Transferred the fixed-link lex-degree prefix lemma to the complete fixed-first 249-profile incidence model, then tested its preprocessing value.

profile-owned lex-prefix incidence preprocessing

Exact residual row degrees and lexicographically sorted columns force two leading zero literals.

Hypothesis: Materializing globally implied units -x(0,1) and -x(1,1) reduces both active variables and clauses after one pinned CaDiCaL preprocessing round by at least 5%.

Test: Append exactly units -16 and -17 to the pinned shared CNF, run CaDiCaL 1.7.3 with -P1 -c 0 on control and treatment, and independently reconstruct the implication, formulas, and final dimensions.

The structural claim follows from exact degree 12 and independently audited lex semantics. Matched pinned preprocessing and separate parsing establish that the units have negligible solver impact. UNKNOWN preprocessing supplies no SAT or UNSAT evidence.

• Every fixed-first lex-normalized 30-block incidence model has x(0,1)=x(1,1)=0.
• The possible first residual block coordinate is reduced from 5004 to C(13,6)=1716 types.
• Explicit units -16 and -17 fail the predeclared 5% preprocessing gate.
• The maintained range remains 30 <= C(15,6,3) <= 31.

• Corrected producer receipt measured 21349/121882 versus 21334/121833.
• The independent checker reproduced the implication, augmentation, dimensions, and decision.
• sha256sum -c artifacts/epoch53-20260810/SHA256SUMS passed.
• The initial failed run and superseded v1 metric were preserved rather than overwritten.

• .proof-experiments/20260810-123207-86a8b0: failed closed before solver invocation because obsolete dimensions were pinned.
• .proof-experiments/20260810-123243-62eec8: v1 completed but its active-variable metric was superseded.
• .proof-experiments/20260810-123418-e672ce: corrected producer run.
• .proof-experiments/20260810-123438-5b2986: independent validation passed.

checkers/check_global_lex_prefix_preprocess_v1.py uses a separate parser and clean-room degree/lex argument and does not import the producer.

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

• Fixed-link degree/lex lemma -> predict two forced zeros globally -> independently proved.
• Large first-coordinate reduction -> predict at least 5% preprocessing savings -> falsified.

• If m lex-sorted binary columns have first-row degree d0<m and second-row degree d1<m-d0, the first column begins with two zero bits.
  Direct prefix-segment proof reconstructed by the independent checker. · Binary columns sorted lexicographically with 0<1. · proved
• The first residual block omits points 0 and 1.
  Instantiate m=29 and d0=d1=11. · Every simple fixed-first model in the complete 249-profile frontier. · proved
• Explicit units preprocess to 21334 active variables and 121833 clauses versus 21349 and 121882.
  Pinned CaDiCaL logs and independent parser. · CaDiCaL 1.7.3 with -P1 -c 0 on the hash-pinned shared CNF. · computed

• Use explicit units -16 and -17 as a material preprocessing improvement.
  One pinned CaDiCaL preprocessing round on the shared global formula. · Both 5% gates failed by two orders of magnitude. · Corrected v2 receipt and independent check. · A materially different encoding with at least 5% improvement in both dimensions or terminal evidence attributable to the units.
• Treat the simplified DIMACS maximum identifier as the active-variable count.
  CaDiCaL preprocessing receipts. · The header retains maximum identifiers after variables become inactive. · v1 supersession record and final progress rows. · None; parse active-variable progress or independently compact the formula.

• Canonical full pair-excess multigraph frontier
  Every putative cover has a loopless 4-regular pair-excess multigraph, giving a potentially global structural owner. · Generate at most 10000 canonical graphs with exactly-once ownership and independent reconstruction. · high · open
• Constructive witness search with a materially different global heuristic
  A 30-block witness remains the cheapest terminal certificate, but current C5 and local-shell routes are capped. · Test a new global move or packed pair-excess prune with positive controls. · normal · open

Objective: Determine whether full pair-excess multigraph canonicalization provides a tractable exactly-once global decomposition.

First action: Implement a canonical-augmentation generator and separate ownership checker, then run with a 10000-leaf or 30-minute cap.

Stop condition: Stop on ownership failure, cap saturation without useful compression, predominantly trivial stabilizers, or reliance on uncheckable PB evidence.

• Implement canonical augmentation for complete loopless 4-regular multigraphs on 15 vertices.
• Write a separate symmetry, row-sum, reconstruction, and exactly-once ownership checker.
• Cap the discriminator at 10000 leaves or 30 minutes.
• Do not launch PB leaves without a pinned independent PB proof replayer.

• 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://arxiv.org/abs/2607.23766 ↗
• https://zenodo.org/records/19735294 ↗
• https://doi.org/10.1002/jcd.3180030404 ↗

GPT-5.6 Sol was principal investigator. Two GPT-5.6 Terra delegates supplied advisory memos only; model agreement was not validation and no delegate artifact is decisive evidence. Python 3.12.3 generated the augmented CNF and ran a separately written checker. CaDiCaL 1.7.3 performed preprocessing only. SHA-256 and the computational-researcher harness recorded artifacts. The web connector returned no extract, so the pre-acquired source audit was retained. No CAS, proof assistant, PB replayer, cloud lab, external proof service, or human validator was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1286.6s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260810-124313-a02e3e

No human review recorded.