Conditioned the fixed-link incidence CNF on two extreme canonical first blocks, independently replayed terminal evidence, then extracted and checked a lexicographic-degree lemma that eliminates first blocks containing points 1 or 2.

fixed-link incidence SAT with lex-degree prefix reduction

Exact residual row degrees interact with the membership-bit lexicographic column orbitope to force leading zero bits in the first residual column, eliminating whole first-column cubes before SAT.

Hypothesis: At least one of the least and greatest canonical first-column cubes for the fixed published link produces terminal SAT or UNSAT evidence within ten CPU-seconds.

Test: Materialize fourteen first-column units for the two extreme representatives, run proof-producing CaDiCaL 1.7.3 for ten seconds per arm, reconstruct both CNFs independently, and require dual LRAT replay for UNSAT.

Exact degree equations and lex ordering give a short proof of the forced prefix. Complete independent orbit reconstruction confirms the exact 672 count. Dual proof replay supports the scoped UNSAT leaf, but its inclusion in the bulk-eliminated class prevents using it as evidence of general tractability.

• For the fixed source link, every lex-sorted eighteen-column completion has a first residual block omitting points 1 and 2.
• Exactly 672 of the 2211 canonical first-column cubes survive this restriction.
• The fixed-link cube with first residual block {1,2,3,4,5,6} is UNSAT.
• No global covering bound changed: 30 <= C(15,6,3) <= 31.

• sha256sum -c artifacts/epoch52-20260810/SHA256SUMS passed for every listed artifact.
• CaDiCaL 1.7.3 returned UNSAT for the greatest cube; fresh lrat-check and CakeLPR builds both accepted LRAT e74c37e7b58de40d75d549f686b9045205da12742104d992d46289601ff48c79.
• The independent checker reconstructed two 6725-variable, 28566-clause conditioned formulas exactly.
• Independent enumeration recovered 3003 labelled blocks, 2211 prior orbits, and 672 surviving orbits.
• The valid v4 mutation harness rejected changed ownership, false status, changed formula hash, and terminal-line deletion.

• .proof-experiments/20260810-115158-6e21e6: repaired two-arm pilot; greatest cube dual-replayed UNSAT and least cube UNKNOWN.
• .proof-experiments/20260810-115229-0606e7: independent clause reconstruction and proof replay passed.
• .proof-experiments/20260810-115439-32db67: path-rebound mutation controls all rejected.
• .proof-experiments/20260810-115709-cc08b2: producer retained exactly 672 lex-degree-compatible orbit representatives.
• .proof-experiments/20260810-115720-937641: independent enumeration reproduced the 672 count.

check_fixed_link_extreme_pilot_v1.py reconstructs every CNF clause using the earlier independent encoding and freshly replays proofs; check_fixed_link_lex_degree_prefix_v1.py separately enumerates all blocks and orbits and verifies the degree-prefix proof.

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

• Lexicographic orbitopes plus exact row sums -> predict forced leading zero bits -> observed two forced zeros and an exact 2211-to-672 local reduction.
• Fixed-link residual degrees 7,7 among 18 columns -> predict the same mechanism for fixed-first residual degrees 11,11 among 29 columns -> theorem-level argument appears to transfer, but preprocessing impact is not yet measured.
• Extreme-cube SAT calibration -> predict terminal behavior signals tractability -> observed a trivial boundary UNSAT, falsifying that interpretation.

• The first residual block omits points 1 and 2 in every lex-sorted completion of the fixed link.
  Exact degree argument and independent checker receipt ccae010b47fb1cd5eb038a845c88fcb41dfb44be3ef519cfb7e2a79d087ee66c. · Fixed link SHA-256 fa875193588a0313e7f87e7f38f95fef596177cf7842c6ba0d335c90604560bc. · proved
• Exactly 672 canonical first-column cubes survive the forced-prefix restriction.
  Complete enumeration and closed-form count (924+420)/2=672. · First residual blocks for the fixed-link family under automorphism (4 5). · computed
• The first-block cube {1,2,3,4,5,6} is UNSAT.
  LRAT SHA-256 e74c37e7b58de40d75d549f686b9045205da12742104d992d46289601ff48c79 accepted by lrat-check and CakeLPR. · One materialized first-column cube for the fixed-link CNF. · proved

• A fixed-link completion may have a first residual block containing point 1 or point 2.
  All 1539 such canonical first-column cubes for the fixed source link. · Exact residual degrees conflict with membership-bit lex ordering. · fixed-link-lex-degree-prefix-audit-v1.json and its independent checker receipt. · Only a demonstrated defect in the exact degree equations, lex-chain semantics, or fixed-link identity.
• Use the greatest cube's fast UNSAT as evidence that the 672 surviving cubes are SAT-easy.
  Fixed-link solver scale-up decision. · The greatest cube lies in the class eliminated directly by the structural lemma, while the sampled surviving cube remained UNKNOWN. · run-receipt.json plus the lex-degree audit. · A terminal proof or witness for a surviving interior cube under the same proof contract.
• Rebuild a complete fixed-first ownership frontier.
  The proposed Terra follow-up. · Epoch 44 already contains an independently checked exactly-once 249-profile frontier. · artifacts/epoch44-20260810/fixed-first-profile-manifest-v3/independent-check.json · A hash or coverage defect in the retained epoch-44 manifest.

• Global fixed-first lex-degree prefix units
  The same proof forces two units in the globally complete 249-profile shared encoding and may improve preprocessing without sacrificing proof production. · Append the two units, independently prove implication, and compare preprocessed dimensions before any solver calibration. · high · open
• Remaining 672 fixed-link cubes
  The local frontier is now 3.29 times smaller, but its global scope is poor and the sampled surviving leaf was nonterminal. · Reopen only with proof-prefix reuse or a terminal surviving-leaf calibration. · low · open
• Constructive witness search with theorem-derived prefix propagation
  The same forced-prefix constraints may cheaply strengthen an incidence witness search without committing to local link classes. · Measure whether the implied units reduce the global incidence preprocessing state before running search. · normal · open

Objective: Transfer the lex-degree prefix lemma to the globally complete fixed-first 249-profile encoding and test whether it materially improves proof-producing preprocessing.

First action: Implement a deterministic transformer adding -x(0,0) and -x(1,0) to artifacts/epoch44-20260810/fixed-first-profile-manifest-v3/fixed-first-profile-shared.cnf, plus a separate implication checker.

Stop condition: Redirect on hash or implication failure, preprocessing reduction below 5%, or an UNKNOWN matched calibration without at least 1.25x conflict-rate gain and no-worse LRAT bytes per conflict.

• Implement and independently prove the analogous two implied first-column units for the global fixed-first 249-profile CNF.
• Measure exact preprocessing reduction and stop if it is below 5%.
• Only after passing that gate, run one matched five-second unresolved-profile proof calibration with the frozen conflict-rate and LRAT-efficiency thresholds.
• Keep the 672 fixed-link leaves on hold unless a surviving interior leaf terminates or validated proof-prefix sharing becomes available.

• https://www.coveringrepository.com/systems.aspx?k=6&t=3&m=-1 ↗
• https://ljcr.dmgordon.org/cover/show_cover.php?k=6&t=3&v=15 ↗
• https://zenodo.org/records/19735294 ↗
• https://doi.org/10.1002/jcd.3180030404 ↗
• https://github.com/tanyongkiam/cake_lpr ↗

GPT-5.6 Sol was principal investigator; two GPT-5.6 Terra delegates supplied advisory prior-art and verification memos only. Python 3.12.3 generated and independently reconstructed CNFs and orbit data. CaDiCaL 1.7.3 performed bounded proof-producing SAT search. GCC 13.3.0 built retained lrat-check and CakeLPR sources; both replayed the terminal LRAT. SHA-256 and the computational-researcher experiment harness recorded artifacts. Web search checked maintained sources. No CAS, proof assistant, cloud lab, external proof service, or human validator was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1442.1s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260810-120516-bfa61c

No human review recorded.