Construct and independently audit an exact CNF for the fixed-first q=5 equality branch E5, then compare it with the retained unrestricted q=5 formula U5 in four alternating proof-producing CaDiCaL runs.

proof-producing incidence/PB cube decomposition

E5 adds pair-multiplicity-at-most-five counters, exact multiplicity-five indicators, and exactly five induced excess edges per block to the retained U5 incidence formula; matched bounded CDCL runs measure whether the additional propagation improves proof search.

Hypothesis: The exact max-q<=5 equality encoding E5 achieves at least a 2x geometric-mean conflict-rate gain over unrestricted U5 at matched seeds.

Test: Run E5/U5 at seed 0 and U5/E5 at seed 1 for five solver seconds each, require a geometric-mean E5/U5 conflict-rate ratio of at least 2.0 with neither seed below 1.5, and independently reconstruct all added clauses and reject incomplete proofs.

The deterministic checker validates the encoding and measurements, but UNKNOWN runs and rejected proof prefixes establish neither existence nor exclusion. The only justified decision is to stop scaling this duplicated-counter implementation.

• The recorded E5 CNF exactly encodes the max-q<=5 equality subbranch inside the retained U5 model.
• In the frozen four-run pilot, E5/U5 conflict-rate ratios were 0.4347581552 and 0.5773736667, with geometric mean 0.5010168762.
• Both fresh LRAT implementations explicitly rejected all four incomplete proofs.
• No covering-number bound changed.

• python3 scripts/equality_branch_calibration_v1.py --out-dir artifacts/epoch55-20260810/equality-branch-calibration-v1 --seconds 5
• python3 checkers/check_equality_branch_calibration_v1.py --receipt artifacts/epoch55-20260810/equality-branch-calibration-v1/calibration-receipt.json --output artifacts/epoch55-20260810/equality-branch-independent-check.json
• Primary receipt SHA-256 9bc1f7cf9bdb8ce18887dc0827b4bc0b20761a2da0d13c4fe7b325be9c6604c1
• Independent check SHA-256 f3210442c9c4efa80ac176db58a55e57bedd35227a2e030afc4f14ada2b4eb8c
• Epoch receipt SHA-256 cb1fab92ff6f5d179ada78c5b7b481f53e82a8651cf3c58b554f4bdf3d312e1

• .proof-experiments/20260810-141253-391798: four UNKNOWN runs; geometric E5/U5 conflict-rate ratio 0.5010168762.
• .proof-experiments/20260810-141354-b88992: independent reconstruction PASS; all partial LRATs explicitly rejected.

checkers/check_equality_branch_calibration_v1.py independently reconstructed all 116895 E5 suffix clauses without importing the producer, checked inherited support semantics and mutations, reparsed logs, and rebuilt two LRAT implementations.

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

• Proof-producing exhaustive covering campaigns -> predict that a globally constrained equality branch will improve CDCL propagation -> observed a 0.501x geometric conflict-rate ratio, falsifying this duplicated-counter implementation.
• Slack-zero excess-graph structure -> partition existence into E5 and H6 anchor branches -> E5 was encoded exactly, while H6 remains the cheaper complementary test.

• E5 exactly represents the fixed-first q=5 max-q<=5 equality branch inside U5.
  Independent byte-for-clause reconstruction, support-equivalence audit, and counter boundary controls. · The immutable U5 and E5 CNFs recorded in epoch 55. · proved
• E5 achieved geometric-mean conflict throughput 0.5010168762 times U5.
  Four raw CaDiCaL logs independently reparsed under the frozen schedule. · CaDiCaL 1.7.3, seeds 0 and 1, five-second proof-producing runs on the recorded CPU. · computed
• All four recorded LRAT files are incomplete and rejected by both retained implementations.
  Fresh builds of lrat-check and CakeLPR produced the required explicit rejection markers. · The four epoch-55 LRAT prefixes only. · computed

• Scale the unchanged duplicated-counter E5 encoding.
  The exact immutable E5 CNF and matched five-second CaDiCaL 1.7.3 protocol. · It failed both matched throughput comparisons and the geometric 2x gate while increasing size and memory. · Independent-check comparison ratios 0.4347581552, 0.5773736667, and 0.5010168762 geometric mean. · Remove all 105 duplicated pair counters using a separately checked inherited-output map, project at most 1.35x U5 bytes, and at least match U5 on both bounded runs.
• Interpret the recorded UNKNOWN proof prefixes as an exclusion.
  All four epoch-55 runs. · Neither proof derives the empty clause; both replay implementations explicitly reject every prefix. · artifacts/epoch55-20260810/equality-branch-independent-check.json · A complete proof accepted by both replay implementations.

• Complementary q>=6 constructive anchor
  Together with E5 it is existence-complete, requires only one one-sided threshold, and may directly produce a 30-cover. · Build H6 from the hash-bound fixed-first base, independently reconstruct it, then run two five-second proof-producing seeds. · high · open
• Compressed E5 using inherited pair-totalizer outputs
  It can remove 51975 duplicated-counter clauses and 10500 variables exactly. · Derive and independently check the threshold-output variable map before any solver run. · normal · open
• Complete canonical root-link catalogue
  It remains a materially different negative route but needs a compact, independently replayable catalogue frontier. · Resume only after a sound bulk completion filter or two-augmenter ownership proof satisfies the recorded reopen condition. · low · open

Objective: Test the complementary existence-complete q>=6 constructive anchor.

First action: Create scripts/build_high_excess_anchor_v1.py from the epoch-7 fixed-first base and append a one-sided totalizer asserting the 450 internal pair supports sum to at least 66.

Stop condition: Stop or redirect on reconstruction mismatch, invalid proof handling, two UNKNOWN runs without a propagation advantage, or resource growth beyond the frozen gate.

• Generate one proof-compatible H6 formula asserting fixed-first internal pair incidence at least 66.
• Independently reconstruct its one-sided totalizer and boundary semantics.
• Run a two-seed five-second constructive pilot and directly verify any SAT witness against all 455 triples.
• Revisit E5 only after removing all duplicated pair counters through a checked map to inherited totalizer outputs.

• https://www.coveringrepository.com/systems.aspx?k=6&t=3&m=-1 ↗
• https://arxiv.org/abs/math/9502238 ↗
• https://www.dmgordon.org/papers/cover.pdf ↗
• https://arxiv.org/abs/2607.23766 ↗

GPT-5.6 Sol served as principal investigator and selected, implemented, ran, audited, and interpreted the bounded discriminator. GPT-5.6 Terra delegates supplied advisory prior-art and experiment-verification memos; their agreement was not treated as validation, and the relied-on recommendation was promoted with provenance. CPython 3.12.3 generated the CNFs and receipts. CaDiCaL 1.7.3 performed four proof-producing SAT runs. Fresh GCC builds of retained lrat-check and CakeLPR sources checked the proof prefixes. GNU time, exact integer arithmetic, SHA-256, the Proof Factory experiment harness, and web search over primary sources were used. No CAS, proof assistant, cloud lab, external proof service, or human validator produced terminal evidence.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1060.8s

Review state

not a result claim

Attempt ID

covering-c1563-20260810-141949-33a150

No human review recorded.