Replaced all fifteen exact-degree totalizers in canonical type-4 leaf 8 with a backward-sliced, false-padding-folded Batcher bitonic selection network and ran a matched proof-capable three-seed calibration.

proof-capable selection-network calibration

A descending comparator DAG computes the target and target+1 thresholds for each residual degree row; biconditional AND/OR gates and two output units enforce exact degree.

Hypothesis: On exact type-4 leaf 8, the backward-sliced bitonic network 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 reconstruction of 1,848,728 clauses, 90,112 small semantic cases, six mutations, byte-identical regeneration, and DRAT-to-LRAT smoke replay.

The packet validates an exact negative method comparison and reusable control. It supplies no cover, UNSAT leaf, or primary-space elimination, so it is campaign progress but not field-level progress or a candidate contribution.

• The recorded selection-network CNF has exactly 618,812 variables, 1,848,728 clauses, and SHA-256 1da14e68f1f5fb78cd923ea51af3c22ed8d7a98b8a6143bdb14ca1bd0a907ad7.
• It is primary-semantically equivalent to audited canonical type-4 leaf 8 within the checked encoding contract.
• At 2,000 conflicts every challenger run was UNKNOWN with 5,527 decisions and 28,559,395 propagations versus control UNKNOWN with 4,943 and 4,082,578.
• No primary assignment was excluded and the maintained range remains 54 <= C(15,5,3) <= 55.

• check_type4_leaf8_bitonic_selection_v1.py reconstructed 1,848,728 clauses and 15 rows with valid=true.
• test_type4_leaf8_bitonic_selection_small_v1.py passed 90,112 cases; all six mutations were rejected.
• check_type4_leaf8_bitonic_selection_result_v1.py reparsed six logs, recomputed gate=false, replayed LRAT, and rejected wrong-formula replay.
• check_type4_leaf8_bitonic_selection_regeneration_v1.py reproduced both CNF and manifest byte-for-byte.
• sha256sum -c artifacts/type4-leaf8-bitonic-selection-20260811/manifest.sha256 passed.

• .proof-experiments/20260811-083320-4c5c30: 90,112 small semantic cases passed.
• .proof-experiments/20260811-083338-ca755f: generated 618,812-variable/1,848,728-clause CNF.
• .proof-experiments/20260811-083400-0e0e44: every clause and row reconstructed.
• .proof-experiments/20260811-083416-99b015: six mutations rejected.
• .proof-experiments/20260811-083555-45fc37: all six matched runs UNKNOWN; telemetry gate false; proof smoke replayed.
• .proof-experiments/20260811-083711-5c0979: raw receipt and direct LRAT audit passed.
• .proof-experiments/20260811-083737-e2bbf1: byte-identical regeneration passed.

check_type4_leaf8_bitonic_selection_v1.py rebuilds block incidence with integer masks and independently named min/max topology routines, then matches all clauses; a separate result checker reparses logs and directly 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

• Cardinality/selection networks -> predict stronger monotone propagation at exact low thresholds -> observed 6.25627x worse propagations per decision and 11.8147 percent more decisions, rejecting this exact topology.

• The recorded bitonic leaf formula is exactly 618,812 variables and 1,848,728 clauses.
  manifest, independent full reconstruction, and byte-identical regeneration · Canonical type-4 semantic leaf 8 only · computed
• All three 2,000-conflict challenger runs used 5,527 decisions and 28,559,395 propagations and returned UNKNOWN.
  raw logs plus independent result receipt · CaDiCaL 1.7.3, recorded formula and cap · computed

• Scale the exact backward-sliced bitonic selection formula solely by increasing its conflict limit.
  Formula SHA-256 1da14e68... under the fixed all-seed gate · No leaf was decided; decisions, propagation per decision, and wall time all worsened materially. · artifacts/type4-leaf8-bitonic-selection-20260811/result-independent-check.json · A materially different half-cardinality or decomposition topology that passes a fresh size and telemetry gate, or a checked model/proof.
• Treat backward gate slicing as a mathematical covering-space reduction.
  This compiler calibration · The same 2^2717 primary assignments remain represented and all runs were UNKNOWN. · artifacts/type4-leaf8-bitonic-selection-20260811/independent-check.json · 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, but authorization is a hard gate. · After explicit approval of map SHA-256 7fcfd2d9..., generate exactly stratum 0 as one 256-cell selector union. · high · open
• True half-cardinality network size pilot
  The tested backward-sliced full bitonic topology is not the O(n log^2 k) half-cardinality construction of Asin et al.; a size-only pilot tests whether that material change deserves a solver run. · Implement a topology census for row widths 715/935 and targets 13/16/17; stop unless total clauses are materially below 594,094. · normal · open
• New constructive exact-degree neighborhood
  A hit is terminal, but previous 2-for-2, 3-for-3, and ejection-chain neighborhoods stalled at defect 10. · Design a move family not expressible as the closed neighborhoods and require a below-10 pilot. · low · open

Objective: Resolve the owner gate or cheaply falsify the only materially different compact comparator topology before any solver run.

First action: Request approval of selector map SHA-256 7fcfd2d9b429c02d3c968921155f1384343ba5bde865d7f0d9c59aab0f59a403; if unavailable, implement only an Asin half-cardinality topology census for widths 715/935 and targets 13/16/17.

Stop condition: Stop the compact-network route if its exact clause count is not materially below 594,094; redirect on any semantic mismatch; a checked 54-cover or complete replayed exclusion ends the campaign.

• Do not scale or rerun this exact bitonic formula solely at a larger cutoff.
• Keep the complete fixed-pair-link route closed because its independently audited logical CNF delta is zero.
• Do not dispatch selector stratum 0 until the human owner explicitly approves map SHA-256 7fcfd2d9b429c02d3c968921155f1384343ba5bde865d7f0d9c59aab0f59a403.
• If approval remains unavailable, perform only a formula-size/topology pilot for the true Asin half-cardinality construction and stop unless it is materially smaller than the 594,094-clause totalizer.

• 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://www.cs.upc.edu/~erodri/webpage/papers/sat09-card.pdf ↗
• 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 them, independently confirmed the fixed-link route's zero CNF delta, 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 the smoke proof; drat-trim and lrat-check converted and replayed LRAT; SHA-256, mutation testing, web search, and the computational-researcher harness were used. No subagents, 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

1465.7s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1553-20260811-084545-68f95f

No human review recorded.