Delete exactly the 13,650 reverse triple-support implications from the pinned normalized r=0 incidence CNF, then compare matched CaDiCaL preprocessing dimensions.

projection-equivalent incidence SAT compression

Retain y(T,c)->x(p,c) for all p in T and OR_c y(T,c), while deleting only AND_{p in T}x(p,c)->y(T,c); independently reconstruct the stream and apply a frozen two-dimension preprocessing gate.

Hypothesis: Deleting exactly 13,650 reverse triple-support clauses reduces both active variables and active clauses by at least 5% after one pinned CaDiCaL 1.7.3 preprocessing round.

Test: Run sequential control and variant CaDiCaL 1.7.3 -P1 -c 0 passes; continue only if control/variant ratios for both active variables and active clauses are at least 1.05.

The deterministic artifacts establish a reusable encoding lemma and decisively close this exact optimization under the frozen protocol. UNKNOWN preprocessing supplies no SAT or UNSAT evidence, so only scoped tactical progress is recorded.

• The pinned r=0 CNF minus exactly 13,650 reverse triple-support clauses has the same projected incidence-matrix models as the base formula.
• The variant has 33,162 variables, 142,742 clauses, and SHA-256 ee755169a47cdd8904c386043ec5261c5d5dd18a747911d31f4052b140ba76b2.
• Pinned preprocessing leaves 19,035 variables and 96,517 clauses for the variant versus 18,988 variables and 105,189 clauses for the control.
• The joint 5% preprocessing gate fails, and no covering-number conclusion follows.

• python3 scripts/one_direction_triple_preprocess_v1.py --out-dir artifacts/epoch91-20260811/one-direction-triples-v1/run --base artifacts/epoch9-20260808/incidence-orbit-pilot-v1/incidence-orbit-r0.cnf --cadical /usr/bin/cadical
• python3 checkers/check_one_direction_triple_preprocess_v1.py --base artifacts/epoch9-20260808/incidence-orbit-pilot-v1/incidence-orbit-r0.cnf --variant artifacts/epoch91-20260811/one-direction-triples-v1/run/incidence-r0-one-direction-triples.cnf --run-receipt artifacts/epoch91-20260811/one-direction-triples-v1/run/run-receipt.json --archival-cover artifacts/epoch2-20260808/archival_31_cover.txt --output artifacts/epoch91-20260811/one-direction-triples-v1/independent-check.json
• sha256sum -c artifacts/epoch91-20260811/SHA256SUMS
• python3 checkers/verify_cover_v1.py artifacts/epoch2-20260808/archival_31_cover.txt --expected-blocks 31

• .proof-experiments/20260811-161145-cfd781: producer and paired preprocessing completed in 2.753 seconds; joint gate false.
• .proof-experiments/20260811-161212-64bbb5: independent reconstruction and controls completed in 2.005 seconds; checker PASS and gate independently false.

checkers/check_one_direction_triple_preprocess_v1.py uses a separate text parser, invokes the pre-existing clean-room mathematical base reconstructor, compares the retained stream byte-for-byte, truth-tables all 16 gadget assignments, reparses simplified formulas and logs, checks all 455 archival coverage rows, and rejects five mutations.

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

• One-direction Tseitin witnesses -> existential projection should survive reverse-clause deletion -> semantics passed, but preprocessing variable elimination worsened.
• Binary support indices from finite-domain SAT encodings -> replacing one-hot witnesses should target the observed active-variable bottleneck -> not yet tested.
• Certified root-link decomposition from C(12,6,4) -> forced degree types may provide complete structural cases -> only type (8,4^13) is currently audited through depth four.

• The one-direction triple-support encoding is projection-equivalent to the pinned exact-support encoding.
  Elementary two-way extension proof, 16-assignment gadget truth table, 455-triple archival-cover control, and byte-exact clause audit. · Pinned normalized r=0 incidence formula with unchanged pair supports and coverage rows. · proved
• Exactly 13,650 reverse clauses were deleted, producing a 33,162-variable, 142,742-clause CNF.
  Ordered deletion digest 21305d28c003d5d58f8a459a78697e35e08d67817b034c44fbb28f18c7590a96 and independent retained-stream reconstruction. · Variant SHA-256 ee755169a47cdd8904c386043ec5261c5d5dd18a747911d31f4052b140ba76b2. · computed
• The variant fails the frozen joint preprocessing gate.
  Independent log reparse: variable ratio 0.9975308641975309 and clause ratio 1.0898494565724173. · CaDiCaL 1.7.3 -P1 -c 0 on the pinned control and exact variant. · computed

• Use reverse-triple-clause deletion alone as the next r=0 preprocessing optimization.
  The exact 13,650-clause one-direction variant under the frozen CaDiCaL 1.7.3 preprocessing gate. · Active variables worsened by 47 and the required variable ratio was below 1.05. · artifacts/epoch91-20260811/one-direction-triples-v1/run/run-receipt.json and independent-check.json · A material witness representation, preprocessing mechanism, or solver change that directly addresses active-variable retention.
• Treat the Terra S6-on-duads sieve as a new global exclusion.
  S6-invariant 30-block families on the 15 duads of K6. · Every S6-invariant family is already A5-invariant, so the sieve is contained in a previously tested family. · artifacts/epoch91-20260811/terra-memos/challenger-prior-art.md · A symmetry family not contained in a previously exhausted invariant family, with independent orbit coverage.

• Five-bit triple support-column indices
  They replace 13,650 one-hot witnesses with 2,275 bits and directly target the measured active-variable failure. · Compile and independently reconstruct the expected 21,787-variable, 143,197-clause r=0 formula, then apply the paired preprocessing gate. · high · open
• Depth-four audit for root-link type (6^2,4^12)
  It is structurally distinct and has the largest target-color stabilizer among the four unaudited degree types. · Adapt the epoch-86 global-orbit-closure producer and an independent child-coverage enumerator with a 10,000-orbit cap. · normal · open
• Proof-producing PB incidence cubes
  Terminal UNSAT evidence would be valuable, but the required pinned emitter and dual-replayer source locks remain absent. · Audit pre-acquired official source snapshots, versions, and hashes before compiling one calibration proof. · low · open

Objective: Test whether binary support-column indices materially reduce both active preprocessing dimensions while preserving exact cover projection.

First action: Implement scripts/binary_index_triple_preprocess_v1.py with dense variable remapping and an independently reconstructed 21,787-variable, 143,197-clause target.

Stop condition: Redirect on any semantic/remapping mismatch, non-UNKNOWN preprocessing status, or either control/variant ratio below 1.05.

• Implement a five-bit support-column index per triple, densely remapping later variables; independently derive the expected 21,787 variables and 143,197 clauses.
• Truth-table the index semantics, forbid codes 30 and 31, reconstruct the entire remapped CNF independently, and rerun the paired 5% gate.
• If the binary-index encoding fails, audit the depth-four root-link frontier for type (6^2,4^12) with independent labelled-child coverage and a 10,000-orbit cap.
• Keep the PB route blocked until pinned emitter/replayer sources, versions, and hashes satisfy its recorded reopen condition.

• 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/math/9502238 ↗
• https://arxiv.org/abs/2607.23766 ↗

GPT-5.6 Sol principal performed route selection, proof audit, implementation, experiment interpretation, and final synthesis. GPT-5.6 Terra delegates supplied advisory experiment-verification and prior-art memos; their agreement was not treated as validation, their relied-on summaries were promoted with provenance, and Sol independently checked or rejected their suggestions. Deterministic Python 3.12.3, CaDiCaL 1.7.3, the computational-researcher reproducibility harness, SHA-256, and web search/retrieval were used. No CAS, PB solver, proof assistant, proof checker, cloud lab, external proof service, or human validator was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1211.8s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260811-162159-d95784

No human review recorded.