Added and independently audited row-lex symmetry breaking for the fixed-disjoint-second-block r=0 incidence branch, then applied a frozen one-round preprocessing gate.

incidence-matrix SAT with orbitope symmetry breaking

Use the exact S6 x S6 x S3 point stabilizer after fixing two disjoint blocks, impose 12 adjacent within-color row-lex comparators alongside residual-column lex order, and measure the resulting active CNF dimensions.

Hypothesis: Sound row-lex constraints for the exact r=0 point stabilizer reduce both active variables and active clauses by at least 5% after one pinned CaDiCaL preprocessing round.

Test: Append exactly 12 width-28 row comparators to the immutable r=0 CNF, independently reconstruct and attack them, then compare matched CaDiCaL 1.7.3 -P1 -c 0 active dimensions.

The global orbit-minimum argument establishes existence of double-lex representatives without relying on an unsafe sorting heuristic. Independent reconstruction and controls validate the implementation. The measured ratios are below 1, decisively failing both frozen 1.05 gates and the no-worsening condition, so this exact optimization should not be scaled.

• Every fixed-disjoint-block r=0 orbit has a representative with residual columns lex sorted and rows lex sorted within {0,...,5}, {6,...,11}, and {12,13,14}.
• The appended row suffix contains exactly 12 comparators, 348 auxiliary variables, and 2028 clauses.
• Pinned preprocessing leaves 18988 variables and 105189 clauses for the control and 19270 variables and 107199 clauses for row lex.
• No bound on C(15,6,3) changed.

• python3 /root/proof-factory/skills/computational-researcher/scripts/run_experiment.py --name r0-row-canonical-preprocess-v1 ...
• python3 /root/proof-factory/skills/computational-researcher/scripts/run_experiment.py --name check-r0-row-canonical-preprocess-v2 ...
• sha256sum -c artifacts/epoch90-20260811/SHA256SUMS: all entries OK
• Independent check SHA-256 b1e8167508e3680bfb7eae1d134913b4d4d7b4cd277d0b488c7efb1c44475329

• .proof-experiments/20260811-153314-839656: producer completed in 2.904 seconds; both 5% gates and the no-worsening gate failed.
• .proof-experiments/20260811-153420-7d257d: independent checker completed in 5.398 seconds; exact reconstruction, 32768-matrix audit, archival-cover control, and four PASS_REJECTED mutations succeeded.

checkers/check_r0_row_canonical_preprocess_v1.py independently reconstructs the base column suffix and new row suffix, exhausts a reduced colored group action, checks an adversarial matrix and the archival 31-cover, reparses raw logs and simplified CNFs, and executes four fail-closed mutation paths.

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

• Matrix symmetry breaking -> global orbit minimum predicts simultaneous row/column lex representatives -> confirmed by proof and exhaustive reduced-action testing.
• C(12,6,4) certificate discipline -> require independent reconstruction and fail-closed controls before search -> controls passed, but the efficiency gate stopped search.

• The stabilizer of fixed columns {0,...,5} and {6,...,11} is S6 x S6 x S3 on the three resulting point-color classes.
  Direct setwise-stabilizer argument recorded in the producer receipt and technical report. · The normalized r=0 branch. · proved
• Every orbit under this point stabilizer and residual-column permutations contains a simultaneous row/column lex representative.
  Global row-major orbit-minimum proof, exact checker, and exhaustive reduced-action control. · All normalized r=0 incidence matrices. · proved
• The tested row-lex suffix worsens one-round active dimensions from 18988/105189 to 19270/107199.
  Pinned CaDiCaL logs and independent reparse receipt. · CaDiCaL 1.7.3 -P1 -c 0 on the exact retained and augmented CNFs. · computed

• Use the exact 12 auxiliary-prefix row comparators as a preprocessing optimization for r=0.
  The pinned r=0 incidence CNF and CaDiCaL 1.7.3 one-round preprocessing protocol. · Both active dimensions worsened and all predeclared continuation gates failed. · artifacts/epoch90-20260811/row-canonical-r0-v1/independent-check.json · A materially different comparator encoding or solver mechanism with an independently audited matched gate; a larger cap alone is insufficient.

• Projection-equivalent one-direction triple supports
  Removing 455*30 reverse implications gives an exact 13650-clause raw reduction while preserving cover existence in both directions. · Compile and independently reconstruct the r=0 clause stream without reverse triple-support implications, then run matched preprocessing only. · high · open
• Canonical root-link catalogue with a new hereditary completion filter
  A complete owned link frontier could support exhaustive certificates, but the prior unfiltered catalogue exceeded its 10000-orbit cap. · Derive and independently test one sound bulk completion filter against the retained 10001-node frontier before rerunning enumeration. · normal · open

Objective: Test the projection-equivalent one-direction triple-support encoding.

First action: Remove exactly the 13650 reverse triple-support clauses from the pinned r=0 CNF and independently reconstruct every retained clause class.

Stop condition: Stop on any semantic mismatch, mutation acceptance, less than 5% active-clause reduction, active-variable growth, or a nonterminal five-second run without a predeclared propagation gain.

• Remove exactly 13650 reverse triple-support implications from the pinned r=0 formula.
• Independently reconstruct all retained forward supports, coverage disjunctions, pair equivalences, cardinality constraints, units, and column comparators.
• Run only a matched CaDiCaL 1.7.3 preprocessing gate; advance to one seed-0 five-second constructive run only if active clauses fall at least 5% and active variables do not worsen.

• https://ljcr.dmgordon.org/cover/show_cover.php?v=15&k=6&t=3 ↗
• https://www.coveringrepository.com/systems.aspx?k=6&t=3&m=-1 ↗
• https://arxiv.org/abs/math/9502238 ↗
• https://arxiv.org/abs/2607.23766 ↗

GPT-5.6 Sol principal designed, implemented, and audited the epoch; two GPT-5.6 Terra delegates supplied advisory route and verification memos but no delegate claim was treated as evidence. CPython 3.12.3 generated and independently reconstructed CNF, enumerated reduced colored-matrix actions, checked the archival cover, and ran mutation controls. CaDiCaL 1.7.3 performed preprocess-only runs. The computational-researcher harness recorded commands, limits, hashes, and memory. Web search checked the maintained repository status and adjacent primary literature. No SAT search, UNSAT proof, CAS, proof assistant, cloud lab, external expert, or human validator produced terminal evidence.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1171.2s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260811-154053-4ec4ea

No human review recorded.