Recursively delete complete automorphism orbits from epoch 72's certified 45-row fixed-link equality cylinder and require independently reconstructed, dual-replayed LRAT evidence.

proof-producing recursive invariant row deletion

Partition the parent's 39 complete (4 5)-orbits into fresh 23- and 22-row child predicates, compile each from the fixed-link base CNF, and test whether either weaker predicate remains UNSAT.

Hypothesis: At least one deterministic invariant 23- or 22-row child is terminal UNSAT within two CaDiCaL CPU seconds and has an ASCII-LRAT proof no larger than 8388608 bytes accepted by lrat-check and CakeLPR.

Test: Compile both children independently and advance only if an intact terminal proof passes both kernels while final-line deletion fails both.

UNSAT of the weaker 22-row formula proves that every completion matching those 22 targets is impossible. The claim is restricted to the exact fixed link and predicate encoded by the reconstructed CNF; no ownership argument supports a broader conclusion.

• The hash-bound 8177-variable, 34190-clause 22-row fixed-link child formula is UNSAT.
• The 45 parent rows form 39 complete certified orbits and are partitioned into children of 23 rows/20 orbits and 22 rows/19 orbits.
• The 23-row sibling was nonterminal under the two-second cap and remains unresolved.
• The maintained range remains 30 <= C(15,6,3) <= 31.

• python3 scripts/recursive_pair_core_probe_v1.py --out-dir artifacts/epoch73-20260811/recursive-pair-core-v1 --seconds 2 --proof-cap-bytes 8388608
• python3 checkers/check_recursive_pair_core_probe_v1.py --artifact-dir artifacts/epoch73-20260811/recursive-pair-core-v1 --out artifacts/epoch73-20260811/recursive-pair-core-v1/independent-check-v3.json
• sha256sum -c artifacts/epoch73-20260811/SHA256SUMS
• Accepted child-1 formula SHA-256 09aa5b9bef9bd2b7ca27833185a92b2203ac83dff67768eff97f4ec7cc2023da
• Accepted child-1 LRAT SHA-256 e75b851010ce308feb217b9dc31a6d36b00095f72d1f552e5900f15bacef8f4a

• .proof-experiments/20260811-022704-f895fb: producer returned UNKNOWN for 23 rows and dual-replayed UNSAT for 22 rows.
• .proof-experiments/20260811-022842-a2ec4f: accepted independent checker reconstructed both formulas, rejected the nonterminal trace, validated the terminal trace, and rejected four content mutations.

checkers/check_recursive_pair_core_probe_v1.py reconstructs the epoch-72 parent split and target graph without importing the epoch-73 producer, rebuilds every clause through the independently maintained checker encoding, replays with lrat-check and CakeLPR, tests final-line deletion, and reruns four corrupted package copies.

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

• Orbit-complete covering computations -> predict that local proof cores must retain explicit ownership and replay semantics -> observed that a 22-row local core is certifiable but still cannot support a global claim without an ownership ledger.

• The explicit 22-row child-1 fixed-link equality cylinder is empty.
  CNF SHA-256 09aa5b9bef9bd2b7ca27833185a92b2203ac83dff67768eff97f4ec7cc2023da; LRAT SHA-256 e75b851010ce308feb217b9dc31a6d36b00095f72d1f552e5900f15bacef8f4a; independent-check-v3 PASS. · One fixed root link and the 22 targets in recursive-cylinder-manifest.json. · proved
• The parent constraint rows are exactly partitioned into invariant children of sizes 23 and 22.
  Independent reconstruction reports 39 parent orbits, child orbit counts 20 and 19, and disjoint exhaustive invariant coverage. · The epoch-72 leaf-1 row set only. · computed

• All 45 epoch-72 equality rows are necessary for the retained local contradiction.
  The certified child-1 target predicate inside the fixed root link. · A subset of 22 rows already yields an independently replayed UNSAT formula. · artifacts/epoch73-20260811/recursive-pair-core-v1/independent-check-v3.json · none; the exact necessity claim is false
• Use the current incidence/PB calibration as accepted mathematical evidence.
  The pinned project environment in this epoch. · Two independently pinnable PB proof replayers were unavailable; ASCII-LRAT checkers do not validate PB traces. · artifacts/epoch73-20260811/delegate-provenance.json and the pre-experiment tool audit · Two official, pinned, independently implemented PB proof replayers and a smallest calibration proof accepted by both

• Recursive 11/11 split of the terminal 22-row cylinder.
  It reaches the at-most-16-row target in one bounded step using an already validated pipeline. · Fork the producer around child-1's 19 orbits and run two fresh two-second proof-producing leaves. · high · open
• Canonical cylinder ownership ledger.
  Local cores become relevant to the exact covering number only when a complete normalized frontier has checked coverage and ownership. · Define canonical pair-profile serialization and test exact membership and overlap on the existing explicit profiles. · normal · open
• Exactly-owned q>=5 fixed-first profile frontier.
  It retains a complete ownership contract and is the fail-safe negative route if recursive local deletion stalls. · Resume its cheapest unresolved proof-producing leaf without extending the UNKNOWN 23-row run. · normal · open

Objective: Determine whether either invariant half of the certified 22-row cylinder remains terminal UNSAT.

First action: Split its 19 complete orbits into two 11-row children with 9 and 10 orbits and invoke the frozen producer/checker protocol.

Stop condition: Stop or redirect if neither child is terminal, any proof exceeds 8 MiB, any reconstruction or replay fails, final-line deletion is accepted, or a content mutation survives.

• Split the terminal 22-row child into two invariant 11-row children containing 9 and 10 complete orbits.
• Apply the same fresh-CNF, two-second, 8 MiB, dual-replay, final-line-deletion, and content-mutation gates.
• If neither child terminates, redirect to the exactly-owned q>=5 fixed-first frontier rather than lengthening the unchanged local run.
• Develop a canonical profile serialization and ownership ledger before aggregating any local cylinders.

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

GPT-5.6 Sol acted as principal investigator. GPT-5.6 Terra delegates supplied advisory reconnaissance and verification-design memos; their agreement was not validation. Deterministic tools used were Python 3.12.3, CaDiCaL 1.7.3, GCC, lrat-check, CakeLPR, exact integer/set arithmetic, SHA-256, and the Proof Factory experiment harness. No CAS, proof assistant, PB solver, cloud lab, external proof service, human validator, or publication action was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

970.0s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260811-023607-ab41a3

No human review recorded.