Byte-regenerate and independently reconstruct the globally complete root-block forward-cap CNF, then compare it against the exact-degree root CNF using identical seed-0 CaDiCaL 1.7.3 runs capped at 25000 conflicts.

proof-preserving global root-block link-cap CNF

Triple coverage proves every point degree is at least 18, permitting exact degree equations to be replaced by forward-only at-most-18 totalizers; the experiment tests whether this clause compression also compresses the CDCL search tree.

Hypothesis: The theorem-equivalent global cap CNF retains at least a 20 percent decision advantage over the exact-degree root CNF at 25000 conflicts without increasing process time or peak memory.

Test: Run both hash-bound formulas with the same CaDiCaL binary, seed 0, 25000-conflict limit, 120-second timeout, and 2048 MiB memory limit; validate any decisive result, otherwise compare independently reparsed decisions, time, and memory.

The experiment directly tested the only premise that justified scaling this encoding. Independent parsing confirms that the decisive route metric moved strongly in the wrong direction. Because neither run returned SAT or UNSAT, the evidence supports redirecting the computational strategy but no mathematical exclusion.

• Fresh generation reproduced cap-CNF SHA-256 517e0312dc31a409aecaaa15fb8ec22aac76ea8f23acb9d313d729a6a2695b8b.
• At matched seed-0 25000-conflict limits, baseline decisions were 59078 and candidate decisions were 86075.
• The candidate reduced propagations by 31.305480 percent, process time by 34.192673 percent, and peak memory by 19.600774 percent in this matched run.
• Neither solver run found a cover or produced an UNSAT result.

• artifacts/root-block-link-cap-25k-20260810/independent-check.json accepted complete clause reconstruction and rejected five mutations.
• Experiment 20260810-214946-d64bf2: LIMIT, 59078 decisions, 34083579 propagations, 14.74 process seconds, 149.79 MB.
• Experiment 20260810-215007-58a2ad: LIMIT, 86075 decisions, 23413551 propagations, 9.70 process seconds, 120.43 MB.
• artifacts/root-block-link-cap-25k-20260810/result-independent-check.json accepted and rejected all three result mutations.
• Experiment 20260810-215528-de38a9 replayed the evidence manifest successfully.

• .proof-experiments/20260810-214925-2bcc04: deterministic candidate generation reproduced the prior CNF hash.
• .proof-experiments/20260810-214936-a557db: independent formula reconstruction passed.
• .proof-experiments/20260810-214946-d64bf2: exact-degree baseline reached LIMIT at 25000 conflicts with 59078 decisions.
• .proof-experiments/20260810-215007-58a2ad: cap candidate reached LIMIT at 25000 conflicts with 86075 decisions.
• .proof-experiments/20260810-215214-845b42: independent result parsing and mutation controls passed.
• .proof-experiments/20260810-215528-de38a9: evidence manifest replay passed.

checkers/check_root_block_link_cap_cnf_v1.py independently reconstructs every candidate clause and rejects five semantic mutations. checkers/check_root_block_link_cap_25k_result_v1.py independently parses both experiment logs, recomputes hashes and percentages, verifies the redirect gate, and rejects three mutated results.

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

• Certified C(12,6,4) SAT workflow -> predict that a theorem-equivalent compressed global CNF can serve as a proof-capable base -> semantic and smoke controls passed previously, but this epoch showed that compression alone does not improve the 25000-conflict search tree.

• In every C(15,5,3) cover, each pair lies in at least five blocks and each point lies in at least eighteen blocks.
  A block containing a fixed pair covers three of its thirteen possible extensions, so lambda_xy>=5; summing over fourteen pairs through x gives 4r_x>=70. · All C(15,5,3) covers · proved
• Coverage plus point caps r_x<=18 is equivalent to coverage plus exact point degrees r_x=18.
  The proved lower bound r_x>=18 and the independently reconstructed cap formula. · The complete root-normalized 54-block encoding · proved
• At seed 0 and 25000 CaDiCaL 1.7.3 conflicts, the cap formula made 86075 decisions and the exact-degree formula made 59078.
  Raw experiment logs and independent result checker · The two specified hash-bound formulas and recorded machine run · computed

• Scale the monolithic global cap CNF because its 5000-conflict decision advantage will persist.
  CaDiCaL 1.7.3, seed 0, 25000 conflicts, and the two recorded root formulas · The cap candidate made 26997 more decisions and failed the predeclared advancement gate. · artifacts/root-block-link-cap-25k-20260810/result.json and result-independent-check.json · A materially new symmetry break, proof-replayable cube partition, solver/encoding mechanism, or decisive proof-producing result; a larger arbitrary cutoff is insufficient.
• Rerun the complete fixed-pair-link relaxation as though it were untested.
  All 395 stored signatures and 754 signature/e_45 targets · The prior complete fixed-pair-link relaxation retained every target. · artifacts/type4-complete-pair-link-gate-20260809/independent-check.json · Genuinely new labelled coupling beyond the complete fixed-pair link.

• Reflection normalizer lex-leader for the compact fixed-C6 family.
  It targets the updated search-tree/symmetry bottleneck with a small projected formula addition and an exact local-family acceptance test. · Prove and independently reconstruct the reflection action, generate one lex-leader, and compare against the compact C6 CNF at 25000 conflicts. · high · open
• Literal outside-subset realization control on saved root-orbit 107.
  It restores labelled subset identities within an aggregate survivor and is materially different from the exhausted envelope projections. · Run the saved profile if the C6 normalizer audit or telemetry gate fails. · normal · open

Objective: Test one proved normalizer symmetry break on the compact fixed-C6 family.

First action: Create a protocol proving and independently checking rho=(1 5)(2 4)(7 11)(8 10)(13 14), then reconstruct its induced permutation of the 509 block-orbit variables.

Stop condition: Stop on any normalizer or orbit-map mismatch; validate any SAT/UNSAT result under the full contract; otherwise close the C6 route unless decisions and process time both improve by at least 20 percent at 25000 conflicts.

• Prove directly that rho=(1 5)(2 4)(7 11)(8 10)(13 14) conjugates the fixed C6 generator to its inverse.
• Independently reconstruct rho's induced permutation on all 509 block orbits.
• Add one audited lex-leader to the compact C6 CNF and run a matched 25000-conflict comparison.
• Validate SAT against all 455 triples or replay a complete DRAT/LRAT proof for UNSAT; otherwise close the C6 route unless both decisions and time improve by at least 20 percent.

• https://www.coveringrepository.com/systems.aspx?k=5&t=3&m=-1 ↗
• https://ljcr.dmgordon.org/cover/show_cover.php?k=5&t=3&v=15 ↗
• https://arxiv.org/abs/2607.23766 ↗

GPT-5.6 Sol acted as principal investigator. GPT-5.6 Terra delegates supplied bounded advisory reconnaissance only; the relied-on challenger memo was promoted with provenance and independently audited, and model agreement was not treated as validation. Python 3.12.3 generated CNFs and ran independent checkers; CaDiCaL 1.7.3 performed bounded SAT searches; SHA-256 and the computational-researcher experiment harness bound commands and artifacts. Web search checked maintained status and prior art. No subagents were spawned by Sol, and no CAS, proof assistant, cloud-lab job, external write, publication, or system modification was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

938.8s

Review state

not a result claim

Attempt ID

covering-c1553-20260810-215930-1a7da8

No human review recorded.