Literal twelve-distinct-4-set residual decomposition on nine deterministic quantiles of the 353 coincident-link survivors, with DRAT-to-LRAT replay and exact attachment-fibre binding.

literal residual block decomposition

Replace independent point-capacity inequalities by one exact 4-uniform hypergraph whose twelve blocks jointly realize all forced degrees and unshadowed-pair demands.

Hypothesis: At least one of nine deterministically selected capacity-surviving coincident-mark interfaces has no twelve-distinct-4-set residual realization with the exact forced degrees and all unshadowed pairs covered.

Test: Rank all 353 survivors by the predeclared capacity-slack tuple, solve nine inclusive quantiles at seed 0 and 25000 conflicts, directly check SAT models, and convert and replay every UNSAT proof through LRAT.

Any genuine 54-cover in the scoped branch must supply the declared twelve-block residual hypergraph. LRAT replay proves that none exists for row 414, and the condition is independent of the other triangle placements. The proof therefore removes exactly that interface fibre, while SAT and UNKNOWN outcomes make no stronger claim.

• Marked coincident-link interface row 414 has no valid twelve-distinct-4-set residual realization.
• The literal residual condition strictly strengthens the inherited point-capacity inequalities.
• All 547 rooted [3^5] attachment orbits of interface row 414 are excluded, reducing the scoped frontier from 471270 to 470723.

• Producer experiment 20260812-183120-6ec243 returned SAT, UNKNOWN, UNKNOWN, UNKNOWN, UNKNOWN, UNSAT, UNKNOWN, UNKNOWN, SAT.
• Independent experiment 20260812-183223-79d9ca regenerated all 353 semantics and nine CNFs; row-414 DRAT and LRAT both verified.
• Attachment experiment 20260812-183351-f83edc checked the exact reduction from 471270 to 470723.
• Mutation experiment 20260812-183411-af9889 rejected a malformed triple, deleted SAT block, and truncated DRAT.
• sha256sum -c artifacts/triangle5-residual-4set-pilot-20260812/manifest.sha256 passes.

• .proof-experiments/20260812-183120-6ec243: nine fixed kernels, one UNSAT, two SAT, six UNKNOWN.
• .proof-experiments/20260812-183223-79d9ca: independent formula, model, and proof validation.
• .proof-experiments/20260812-183351-f83edc: exact attachment-fibre binding.
• .proof-experiments/20260812-183411-af9889: three fail-closed mutations rejected.

check_triangle5_residual_4set_pilot_v1.py independently reconstructs the full census and CNFs, checks complete SAT assignments, converts DRAT to LRAT, and replays LRAT. check_triangle5_residual_attachment_elimination_v1.py separately binds the local proof to the prior Burnside-checked fibre.

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

• C(12,6,4) forced-link certificate architecture -> require proof logs for local link exclusions -> row 414 produced a replayed DRAT/LRAT exclusion.
• Hypergraph degree-sequence realization -> replace independent capacity inequalities by one literal 4-uniform realization -> the discriminator rejected row 414.

• Row 414 has no exact residual twelve-block 4-uniform realization.
  CNF SHA-256 01971dd88ae81fa9693423b7284bb7e82c5da9d29c2aaed53a1ab23d8fa83c18 plus replayed DRAT/LRAT hashes in receipt.json. · Marked coincident-link interface row 414. · computed
• The row-414 exclusion removes exactly 547 rooted [3^5] attachment orbits.
  attachment-elimination.json bound to the independently checked prior orbit ledger. · Rooted [3^5] local interface/attachment product. · computed
• Every genuine cover in a coincident-link branch induces the tested residual 4-uniform hypergraph.
  notes/triangle5-residual-4set-lemma-20260812.md; direct degree and coverage derivation. · All hypothetical 54-block covers with the selected excess-one triangle edge. · proved

• Use the inherited point-capacity inequalities as a complete test of local residual feasibility.
  Coincident-link residual interfaces. · Row 414 passes every point-capacity inequality but its exact literal formula is LRAT-UNSAT. · independent-check.json strict_strength_rows=[414]. · None; the implication is falsified by a certified finite instance.
• Scale the same exact-count DFA immediately across all 353 interfaces.
  This seed-0, 25000-conflict encoding protocol. · Six of nine deterministic quantiles remained UNKNOWN. · result.json and independent-check.json. · A materially different encoding or decomposition wins a matched row-343/row-414 proof pilot; a larger arbitrary cap is insufficient.

• Alternative proof-producing residual encoding.
  The literal mechanism already yielded a certified rejection, but the DFA is the current bottleneck. · Compare a sequential, totalizer, or meet-in-the-middle encoding on row 343 and the row-414 control at the identical conflict cap. · high · open
• Constructive coverage-aware 3-for-3 preflight.
  A lower-defect degree-18 family or 54-cover is terminal and materially distinct from local exclusion. · Run two independently implemented candidate counters around the saved defect-nine seed and proceed only if they agree and the candidate count is at most 2^22. · normal · open

Objective: Find a proof-producing encoding that turns the literal residual mechanism into a complete interface classifier.

First action: Build a matched alternative encoding for rows 343 and 414, then run seed 0 at 25000 conflicts with DRAT/LRAT enabled.

Stop condition: Redirect if row 414 is not replayed, row 343 remains UNKNOWN, formula semantics disagree, or proof checking fails.

• Implement one materially different proof-producing encoding for row 343 and the row-414 control while keeping seed 0 and 25000 conflicts fixed.
• If that encoding fails the matched gate, switch to two independent constructive coverage-aware 3-for-3 candidate pre-counts at the defect-nine seed.
• Only after a matched encoding win, classify the remaining 352 coincident-link interfaces and bind every rejection to its attachment fibre.

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

GPT-5.6 Sol was principal investigator. Two injected GPT-5.6 Terra delegates supplied advisory reconnaissance; their agreement was not evidence, and the fixed-pair rerun was rejected after audit. Deterministic work used Python 3.12.3, CaDiCaL 1.7.3, drat-trim, lrat-check, exact integer combinatorics, SHA-256, the computational-researcher experiment harness, and separate Python checkers. A bounded SciPy/HiGHS development pilot informed experiment design but supports no claimed result. No additional subagent was spawned; no CAS, proof assistant, cloud lab, package installation, system change, or external write was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1529.2s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1553-20260812-184217-b66aef

No human review recorded.