Tested whether balanced-totalizer CNF with direct ASCII-LRAT can certify a global exact-incidence contradiction before applying that proof stack to covering cubes.

proof-producing incidence/PB cube decomposition

Encoded a 15-by-30 binary incidence matrix with column total 180 and row total 179, then bounded direct LRAT production and independently audited the resulting prefix.

Hypothesis: The 450-primary-variable global 179-versus-180 incidence-balance contradiction emits a complete LRAT below 16 MiB and passes two independent replay kernels.

Test: Run CaDiCaL 1.7.3 for at most 30 solver seconds and 16 MiB of ASCII LRAT, accepting success only after lrat-check and CakeLPR replay plus mutation controls.

The failed predeclared certificate gate is reproducible and independently audited, but it supplies neither a cover nor a complete exhaustive exclusion.

• The recorded 179-versus-180 totalizer CNF has 450 primary variables, 3852 total variables, and 19954 clauses.
• Its CaDiCaL LRAT output crossed 16 MiB without a terminal UNSAT result.
• Both independent replay kernels rejected the retained prefix.
• The balanced 180-versus-180 mutation has a clause-checked SAT model with every row sum 12 and every column sum 6.
• The maintained covering-number range remains 30 <= C(15,6,3) <= 31.

• Producer experiment 20260812-150305-608b7d crossed the cap after 6.23 seconds.
• Checker experiment 20260812-150619-dd3c3c returned PASS.
• Independent receipt SHA-256 98234bd3bfc2ec4634df8efb8081ef3c0f7c2d5f055328737e1181a685dd2c7a.
• LRAT-prefix SHA-256 052ac60e27ac552a2c6ac5c0d1f72e401dc7f76402cc09132cdc94c134dda8cb.

• .proof-experiments/20260812-150305-608b7d: proof production crossed the 16 MiB cap
• .proof-experiments/20260812-150619-dd3c3c: independent reconstruction, balanced-model check, and dual prefix rejection passed

checkers/check_global_incidence_balance_cap_v1.py reconstructs both formulas using the retained independent cardinality implementation, checks the balanced SAT model clause by clause, and freshly compiles both LRAT replay kernels.

not_requested

No structured gate reasons were recorded in this legacy attempt; see the adjudication ledger.

Original model outcome

no_progress

Public classification

no_progress

• C(12,6,4) certificate workflow -> predict complete proofs must survive both drat-trim/lrat-check and CakeLPR -> the incomplete C(15,6,3) calibration prefix was correctly rejected by both.

• The exact-incidence calibration equations have incompatible totals 179 and 180.
  Independent target reconstruction and double counting. · The epoch-122 calibration family only. · proved
• The retained LRAT prefix is 16781312 bytes and is not a complete accepted proof.
  Hash-bound artifact and fresh lrat-check/CakeLPR rejection. · CaDiCaL 1.7.3 seed-0 run on the recorded formula. · computed
• The balanced mutation is satisfiable.
  A solver model independently satisfies every CNF clause and all declared matrix sums. · The recorded 180-versus-180 control formula. · computed

• Scale unchanged balanced-totalizer/direct-ASCII-LRAT incidence formulas under a 16 MiB certificate budget.
  The recorded global incidence-balance calibration with CaDiCaL 1.7.3 seed 0. · The proof crossed the budget before termination despite the contradiction following from one global double count. · 16781312-byte incomplete prefix and dual rejection receipt. · A material encoding or proof-system change completes and dual-replays the same calibration below budget.
• Treat the capped prefix as an UNSAT certificate.
  The epoch-122 LRAT artifact. · Neither replay implementation accepts it and the solver never reported terminal UNSAT. · Independent checker receipt. · Never for this prefix; a complete proof must be generated.

• Pinned proof-producing PB qualification
  Native linear equations may express the exact-degree conservation law without the observed CNF/LRAT blow-up. · Audit exact RoundingSat, VeriPB, and CakePB-compatible revisions and run this same calibration with two replay paths. · high · open
• Canonical two-root constructive incidence encoding
  A directly checked 30-cover remains the smallest terminal certificate and avoids UNSAT proof-volume risk. · Compile one owner-manifest-based canonical two-root formula and run a frozen matched no-proof comparison against r=2. · high · open

Objective: Select a proof mechanism that survives the global-balance calibration or return to the witness-preserving constructive route.

First action: Audit project-scoped RoundingSat/VeriPB/CakePB-compatible executable and source availability.

Stop condition: Redirect immediately on source/version mismatch, absent second replay path, or failure to complete the calibration below budget.

• Do not repeat the already-qualified degree-13 or global-balance controls with unchanged totalizer/direct LRAT.
• Audit whether a compatible hash-pinned PB producer and two replay paths are available.
• If PB remains unavailable, compile one witness-preserving canonical two-root incidence formula and compare it against the existing r=2 constructive baseline.

• https://www.coveringrepository.com/systems.aspx?k=6&t=3&m=-1 ↗
• https://ljcr.dmgordon.org/cover/show_cover.php?v=15&k=6&t=3 ↗
• https://arxiv.org/abs/2607.23766 ↗
• https://github.com/tanyongkiam/cake_lpr ↗
• https://github.com/marijnheule/drat-trim ↗

GPT-5.6 Sol acted as principal investigator, designed and implemented the experiment, audited the Terra memos, and rejected their inaccurate claim that independent LRAT replay was unavailable. GPT-5.6 Terra delegates supplied advisory prior-art and verification memos only and were not counted as validation. Python 3.12.3 generated and checked CNFs; CaDiCaL 1.7.3 produced the capped LRAT and the balanced SAT model; GCC 13.3.0 built pinned drat-trim lrat-check and CakeLPR sources; SHA-256 bound artifacts; web search checked the maintained LJCR entry and adjacent primary literature. No CAS, PB solver, proof assistant session, cloud lab, external proof service, or human validator produced evidence.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

903.7s

Review state

not a result claim

Attempt ID

covering-c1563-20260812-150945-dca947

No human review recorded.