Replace all fifteen exact-degree totalizers in audited canonical type-4 leaf 8 by an independently reconstructed Wallace carry-save binary-adder CNF and run a matched three-seed proof-capable calibration.

proof-capable cardinality compiler calibration

Truth-table CNF for carry-save full/half adders computes each residual point-degree sum exactly, with target-bit units; the primary map, coverage prefix, and semantic leaf units are preserved.

Hypothesis: On exact type-4 leaf 8, the Wallace compiler either decides the leaf or reduces decisions and wall time by at least 20 percent for seeds 0,1,2 without increasing propagations per decision.

Test: Six isolated CaDiCaL 1.7.3 runs at 2,000 conflicts after exact independent reconstruction, 769 small truth-table cases, six mutation controls, byte-identical regeneration, and DRAT-to-LRAT proof smoke.

The packet is reproducible and materially smaller, so it is validated internal progress. UNKNOWN runs, zero eliminated assignments, and a failed declared decision threshold do not support a cover, exclusion, or candidate contribution.

• The Wallace CNF has 29,681 variables, 215,899 clauses, and SHA-256 a6972fa7b5ccffdd2a5278be44c6c6d065097de545ce9131cba0634fa0d53930.
• It is primary-semantically equivalent to audited type-4 leaf 8 within the exact checked encoding contract.
• At 2,000 conflicts, every challenger run was UNKNOWN with 4,253 decisions and 77,803 propagations versus control UNKNOWN with 4,943 decisions and 4,082,578 propagations.
• No primary assignment was excluded and C(15,5,3) remains in [54,55].

• python3 checkers/check_type4_leaf8_wallace_degree_v1.py ... returns valid=true with 215,899 clauses reconstructed.
• python3 checkers/check_type4_leaf8_wallace_degree_result_v1.py ... returns valid=true and gate_recomputed=false.
• sha256sum -c artifacts/type4-leaf8-wallace-degree-20260811/manifest.sha256 passes after packet finalization.
• .proof-experiments/20260811-075034-e23b38 records six matched runs and proof smoke.

• .proof-experiments/20260811-074809-f61a3c: generated 29,681-variable/215,899-clause CNF.
• .proof-experiments/20260811-074828-38ffd8: exact independent reconstruction passed.
• .proof-experiments/20260811-074838-154166: six mutations were rejected.
• .proof-experiments/20260811-074940-797c9a: 769 small pinned assignments passed.
• .proof-experiments/20260811-075034-e23b38: all six matched runs UNKNOWN; telemetry gate false; proof smoke replayed.
• .proof-experiments/20260811-075215-af13a3: raw receipt and LRAT replay check passed.
• .proof-experiments/20260811-075215-a5dbdb: regeneration byte-identical.

check_type4_leaf8_wallace_degree_v1.py reconstructs blocks as integer masks and uses separately written integer-assignment gate emission and Wallace scheduling; the result checker reparses all raw logs and freshly replays LRAT.

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

• Hardware carry-save compression -> predict linear-size exact-cardinality CNF with much lower propagation cost -> clauses fell 63.66 percent and wall time over 83 percent, but decisions fell only 13.96 percent, falsifying the full advancement prediction.

• The recorded Wallace leaf formula is exactly 29,681 variables and 215,899 clauses.
  challenger manifest, independent full clause reconstruction, and byte-identical regeneration · Canonical type-4 semantic leaf 8 only · computed
• All three 2,000-conflict challenger runs used 4,253 decisions and 77,803 propagations and returned UNKNOWN.
  Six raw logs and independent result receipt · CaDiCaL 1.7.3, recorded formulas and cap · computed

• Scale the exact type-4 leaf-8 Wallace degree compiler solely by increasing its conflict limit.
  Formula SHA-256 a6972fa7... under the predeclared all-seed decision/wall/propagation gate · No leaf was decided and decision reduction was 13.96 percent, below the required 20 percent on every seed. · artifacts/type4-leaf8-wallace-degree-20260811/result-independent-check.json · A material hybrid/decomposition change that passes a fresh gate or yields a checked model/proof.
• Treat formula-size or wall-time reduction as a mathematical space reduction.
  This exact compiler calibration · Existential auxiliary compression preserves the same 2^2717 primary assignment space and all runs were UNKNOWN. · independent semantic equivalence and zero decisive statuses · A checked SAT model or replayed UNSAT proof eliminating a specified primary scope.

• Owner-approved radius-five selector stratum
  A 288-cell predecessor is proof-replayed and the 3,072-cell map is independently hash-bound. · After explicit approval of map SHA-256 7fcfd2d9..., generate only stratum 0 as one 256-cell selector union and require replayed UNSAT or a directly decoded model. · high · open
• Cardinality-network degree compiler
  Wallace compression showed large wall/propagation savings but insufficient decisions; a sorting/selection network has a materially different propagation graph. · Compile the same fifteen rows on the immutable leaf manifest and run the identical three-seed 2,000-conflict gate after exhaustive network semantics. · normal · open
• New constructive exact-degree neighborhood
  A hit remains the cheapest terminal certificate, but prior 2-for-2, 3-for-3, and ejection-chain neighborhoods stalled at defect 10. · Design a new move family and require a below-10 pilot before scale-up. · low · open

Objective: Resolve owner authorization for the hash-bound radius-five tranche while preserving global proof and constructive routes.

First action: Request explicit approval or rejection of map SHA-256 7fcfd2d9b429c02d3c968921155f1384343ba5bde865d7f0d9c59aab0f59a403; if approved, freeze exactly stratum 0 before generation.

Stop condition: Stop on withheld approval, any map/selector mismatch, UNKNOWN, or DRAT/LRAT failure; a checked 54-cover ends all routes.

• Do not scale or rerun the exact Wallace formula solely at a larger cap.
• Keep the complete fixed-pair-link route closed because its checked logical delta is zero.
• Ask the human owner to approve or reject radius-five map SHA-256 7fcfd2d9b429c02d3c968921155f1384343ba5bde865d7f0d9c59aab0f59a403 before dispatching any selector tranche.
• If approval is unavailable, test a genuinely distinct cardinality-network compiler on the same manifest; require the same independent semantics and matched gate.

• 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://doi.org/10.1109/PGEC.1964.263830 ↗
• https://arxiv.org/abs/2607.23766 ↗

GPT-5.6 Sol acted as principal investigator. GPT-5.6 Terra delegates supplied injected prior-art and verification memos; Sol audited their claims, rejected the zero-delta fixed-link route, and did not count model agreement as validation. Python 3.12.3 generated and independently reconstructed CNF; CaDiCaL 1.7.3 ran six bounded formulas and smoke proof; drat-trim and lrat-check converted/replayed LRAT; SHA-256, mutation testing, and the computational-researcher harness were used. No lab job, package installation, system change, external write, CAS, or proof assistant was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1218.0s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1553-20260811-080002-d08b01

No human review recorded.