Proof-producing canonical type-2 CNF calibration with all 104 implied pair-multiplicity upper bounds

multiplicity-five pair normalization

Translate the previously effective native pseudo-Boolean pair caps into forward-only balanced unary totalizers and compare against the identical canonical type-2 base under matched CaDiCaL limits.

Hypothesis: On canonical type 2, adding all 104 implied pair bounds in proof-producing CNF form reduces CaDiCaL decisions by at least 30 percent at matched seed-0 25000-conflict caps.

Test: Run fresh base and upper CaDiCaL 1.7.3 processes at seed 0 and 25000 conflicts after independent formula reconstruction; compare decisions and stop if the upper reduction is below 30 percent.

The deterministic matched comparison shows that this specific forward-totalizer translation is materially worse than base. Since no live proof or witness was produced, the evidence supports closing only this encoding and protocol.

• The hash-bound type-2 upper CNF contains 177523 variables, 1010071 clauses, 104 pair-cap rows, and 27170 pair incidences.
• At matched seed-0 25000-conflict CaDiCaL 1.7.3 caps, the upper CNF increased decisions from 54423 to 148779.
• The exact value remains in the maintained range 54 <= C(15,5,3) <= 55.

• python3 scripts/type2_pair_upper_cnf_v1.py on the immutable type-2 base produced upper SHA-256 9eb86085684fcfb67adb70110e99f702b7579e6a51d4ec6bec5d2adf30970e2c
• python3 checkers/check_type2_pair_upper_cnf_v1.py reported valid=true and zero mismatches
• CaDiCaL experiment 20260809-215528-88028a: UNKNOWN, 25001 conflicts, 54423 decisions
• CaDiCaL experiment 20260809-215528-69978f: UNKNOWN, 25002 conflicts, 148779 decisions
• drat-trim and lrat-check accepted only the deliberately contradictory smoke certificate

• .proof-experiments/20260809-215452-fb9ffb — generated the clean 104-row upper CNF
• .proof-experiments/20260809-215504-8255f4 — independently reconstructed the formula with zero mismatches
• .proof-experiments/20260809-215528-88028a — base UNKNOWN with 54423 decisions
• .proof-experiments/20260809-215528-69978f — upper UNKNOWN with 148779 decisions
• .proof-experiments/20260809-215735-ec44e1 — all five mutations rejected
• .proof-experiments/20260809-215735-404f3c — all 258 totalizer cases passed
• .proof-experiments/20260809-215855-268e02 — smoke DRAT verified and converted to LRAT
• .proof-experiments/20260809-215903-a89866 — LRAT checker accepted the smoke certificate

checkers/check_type2_pair_upper_cnf_v1.py independently enumerates the 2717 primary block masks recursively and reconstructs every pair row and totalizer clause without importing producer arrays.

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

• Native pseudo-Boolean propagation -> predicted that redundant pair caps would also help proof-producing CNF -> observed the opposite, with 173.3752 percent more decisions.
• Certified SAT-proof workflow -> predicted the local DRAT/LRAT pipeline could be exercised before any scale-up -> the deliberately contradictory smoke certificate replayed successfully.

• Every pair has multiplicity at most 7 in any hypothetical 54-block cover.
  Triple coverage gives lambda_uv >= 5 and exact point degree 18 gives incident pair-multiplicity sum 72. · All hypothetical 54-block C(15,5,3) covers · proved
• The clean type-2 upper CNF has 177523 variables and 1010071 clauses.
  Producer manifest and independent clause reconstruction · CNF SHA-256 9eb86085684fcfb67adb70110e99f702b7579e6a51d4ec6bec5d2adf30970e2c · computed
• The tested upper CNF used 148779 decisions versus 54423 for base at matched caps.
  Hash-bound experiment receipts and CaDiCaL stdout · CaDiCaL 1.7.3, seed 0, canonical type 2, 25000-conflict protocol · computed

• Scale the forward-only balanced-totalizer type-2 pair-cap CNF under the same CaDiCaL protocol.
  The hash-bound canonical type-2 upper formula and seed-0 CaDiCaL 1.7.3 protocol · It increased decisions by 173.3752 percent and remained UNKNOWN. · artifacts/type2-pair-upper-cnf-20260809/result.json · A materially different proof-producing encoding or measured mechanism-level improvement on the same semantics
• Repeat the complete fixed-pair-link relaxation as a standalone filter.
  The previously frozen 395-signature and 754-target type-4 frontier · The complete prior run retained all 754 targets. · artifacts/type4-complete-pair-link-20260809/independent-check.json · Couple the link to genuinely new labelled skeleton information

• Joint labelled pair-excess-skeleton and residual-coverage orbit census
  It combines the two information sources that individually failed and has a one-orbit zero-pruning stop condition. · Build one skeleton-orbit by residual-triple-orbit capacity table with separately reconstructed maps. · high · open
• Materially different proof-producing cardinality encoding
  The pair-cap lemma is sound, but the tested unary encoding caused the observed regression. · Compare one compact cardinality network or BDD encoding against base at 5000 conflicts before any scale-up. · normal · open
• Constructive exact-degree multi-basin search
  A direct 54-block witness remains a symmetric resolution path and the previous local search covered only one radius-five neighborhood. · Measure exact-degree repair success from several independently generated 55-cover basins without claiming arbitrary-radius exhaustion. · low · open

Objective: Test whether one labelled pair-skeleton/residual-coverage coupling prunes any complete target class.

First action: Freeze one canonical skeleton orbit and one residual-triple orbit, then write the target/capacity protocol before implementing either map.

Stop condition: Stop or redirect if producer/checker maps disagree or every target retains a positive capacity witness.

• Select one canonical pair-excess skeleton orbit and one residual-triple orbit.
• Predeclare the exact target set, capacity observable, and zero-pruning stop condition.
• Build independent producer and checker maps before testing a larger orbit family.
• Do not scale this forward-totalizer CNF without a materially different encoding and a new matched pilot.

• https://ljcr.dmgordon.org/cover/show_cover.php?k=5&t=3&v=15 ↗
• https://www.coveringrepository.com/systems.aspx?k=5&t=3&m=-1 ↗
• https://arxiv.org/abs/math/9502238 ↗
• https://arxiv.org/abs/2603.29548 ↗
• https://github.com/arminbiere/cadical ↗
• https://github.com/marijnheule/drat-trim ↗

GPT-5.6 Sol principal selected the route, implemented the producer/checkers, executed the experiments, audited the evidence, and made the route decision. GPT-5.6 Terra delegates supplied advisory prior-art and verification memos; their agreement was not treated as independent validation. Python 3.12.3, exact combinatorial enumeration, CaDiCaL 1.7.3, drat-trim, lrat-check, SHA-256, and web searches of the maintained repository and arXiv were used. No lab job, system installation, external publication, or host-configuration change occurred.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1278.9s

Review state

not a result claim

Attempt ID

covering-c1553-20260809-220614-99d89c

No human review recorded.