Appended thirteen proof-capable Sinz endpoint-collision counters to hash-bound canonical type-4 semantic leaf 8, then compared fresh CaDiCaL runs against the unchanged leaf for seeds 0, 1, and 2 at 2,000 conflicts.

header-conditioned proof-capable endpoint-collision encoding

Encode each sound residual inequality sum_{B containing z and exactly one endpoint} x_B <= 12-2f_z with a rectangular Sinz counter while retaining the audited leaf as an exact clause prefix.

Hypothesis: On fixed type-4 leaf 8, the collision CNF either decides the leaf or reduces decisions and wall time by at least 20 percent versus the unchanged leaf for every seed without increasing propagations per decision.

Test: Six fresh 2,000-conflict CaDiCaL runs, three per formula, after independent clause reconstruction, four mutation controls, byte-identical regeneration, and DRAT-to-LRAT proof-smoke replay.

Exact clause reconstruction, mutation controls, fresh receipt parsing, LRAT proof-stack replay, wrong-formula rejection, byte-identical regeneration, and a passing hash manifest validate the negative telemetry. UNKNOWN runs and a failed performance gate provide no mathematical exclusion.

• The challenger is the exact type-4 leaf-8 CNF conjoined with thirteen sound endpoint-collision constraints encoded by independently reconstructed Sinz counters.
• For CaDiCaL 1.7.3 at the recorded cap, all six matched runs returned UNKNOWN and the challenger used 5,621 decisions versus 4,943 for the control on each seed.
• The exact leaf-8 collision-Sinz advancement gate failed and no primary assignment was excluded.

• sha256sum -c artifacts/type4-leaf8-collision-sinz-20260811/manifest.sha256 passes all entries.
• check_type4_leaf8_collision_sinz_result_v1.py returns valid=true.
• .proof-experiments/20260811-070516-bd705c records the six solver runs and proof-smoke generation.

• .proof-experiments/20260811-070427-608b0a: exact reconstruction passed after correcting a nonsemantic expected test-count bookkeeping error in the discarded 070333 receipt.
• .proof-experiments/20260811-070439-8b3b7f: four corruptions were rejected.
• .proof-experiments/20260811-070516-bd705c: all six runs were UNKNOWN; proof smoke replayed.
• .proof-experiments/20260811-070555-9552c0: independent receipt check passed.
• .proof-experiments/20260811-070650-314c44: byte-identical regeneration passed.
• .proof-experiments/20260811-070751-0fd69f: certified summary and manifest were generated.

check_type4_leaf8_collision_sinz_v1.py reconstructs blocks with recursive bit masks and counters with a one-based prefix/threshold map; check_type4_leaf8_collision_sinz_result_v1.py reparses raw logs, recomputes gates, 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

• Standard sequential cardinality encoding -> compact proof-capable endpoint constraints might improve conditioned CDCL propagation -> propagation intensity improved but decisions regressed 13.7164 percent, rejecting the transfer for this formula and protocol.

• The exact leaf-8 collision formula has 126,976 variables, 710,190 clauses, and SHA-256 f48a39ec06fe0aee24ac5d3b947ecd9a189cc887bf4c00d37f3c9777ab524617.
  challenger-manifest.json plus independent exact reconstruction and byte-identical regeneration · Recorded type-4 leaf 8 only · computed
• At 2,000 conflicts, the challenger uses 5,621 decisions and the control 4,943 for each seed; all runs are UNKNOWN.
  Six raw solver logs and independently checked result.json · CaDiCaL 1.7.3, exact recorded formulas and protocol · computed

• Scale the exact type-4 leaf-8 endpoint-collision Sinz encoding solely by increasing its conflict cutoff.
  Formula SHA-256 f48a39ec06fe0aee24ac5d3b947ecd9a189cc887bf4c00d37f3c9777ab524617 and the recorded protocol · It produced no decisive status and increased decisions by 13.7164 percent on every seed. · artifacts/type4-leaf8-collision-sinz-20260811/result-independent-check.json · A material compiler/decomposition change that passes a fresh gate or yields a checked proof/model.
• Run the proposed 754-target complete fixed-pair link as a logical strengthening.
  Link-coverage obligations alone in the four canonical pair-normalized CNFs · All 5,460 obligations are tautologies or existing baseline coverage clauses. · artifacts/pair-link-cnf-delta-audit-20260811/independent-check.json · A separately justified constraint with nonzero independently checked logical or propagation delta.

• Owner-approved radius-five selector batch
  Its 288-cell predecessor has complete DRAT-to-LRAT replay and the 3,072-cell map is independently reconstructed. · After approval of map SHA-256 7fcfd2d9b429c02d3c968921155f1384343ba5bde865d7f0d9c59aab0f59a403, materialize exactly one 256-cell selector union. · high · open
• Non-sequential proof-capable complete-branch compiler
  The global four-type route is complete, but totalizer, native-PB, and sequential redundant layers remain nondecisive. · Implement one binary-adder or cardinality-network type-4 control and use the same three-seed gate. · normal · open

Objective: Resolve whether the independently mapped 3,072 radius-five cells may be dispatched while keeping global proof and constructive routes distinct.

First action: Request explicit owner approval or rejection of cell-map SHA-256 7fcfd2d9b429c02d3c968921155f1384343ba5bde865d7f0d9c59aab0f59a403.

Stop condition: Stop the local route on withheld approval, map mismatch, UNKNOWN cell, or proof-replay failure; redirect global work unless a new compiler clears the three-seed gate.

• Do not scale or rerun the exact leaf-8 collision-Sinz formula without a material encoding change.
• Keep the complete fixed-pair-link route closed: its independently checked logical clause delta is zero.
• Ask the owner to approve or reject the exact 3,072-cell radius-five map hash; if approved, run one 256-cell selector union with proof replay.
• If approval is unavailable, design one non-sequential proof-capable cardinality compiler and require a three-seed gain 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.1007/11564751_73 ↗
• https://arxiv.org/abs/2607.23766 ↗

GPT-5.6 Sol acted as principal investigator. GPT-5.6 Terra delegates supplied the injected challenger-prior-art and experiment-verification memos; Sol audited and rejected their stale fixed-link route, and model agreement was not validation. Python 3.12.3 generated and checked exact artifacts; CaDiCaL 1.7.3 ran six bounded CNFs and a proof smoke test; drat-trim and lrat-check converted and replayed LRAT; SHA-256, mutation testing, the computational-researcher harness, and current web source checks were used. No lab job, package installation, system change, external write, publication, CAS, or proof assistant was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1661.5s

Review state

not a result claim

Attempt ID

covering-c1553-20260811-071517-e3ac5d

No human review recorded.