Corrected and independently audited strict residual-lex symmetry breaking for profile (26,0,1,2), then ran a frozen three-seed proof-producing calibration.

incidence-matrix SAT with strict residual orbitope symmetry breaking

Assert false the exact final equality prefix in each of the 27 adjacent residual comparators, then compare baseline and strict formulas under matched CaDiCaL seeds and limits.

Hypothesis: For seeds 0, 1, and 2, every strict/baseline conflict-rate and propagation-rate ratio is at least 0.98 and both geometric means are at least 1.05.

Test: Six CPU-0-pinned five-second LRAT runs in baseline/strict pairs, followed by independent raw-log parsing and dual replay rejection of every UNKNOWN proof prefix.

Neither an accepted witness nor a complete UNSAT certificate exists; the exact target and selected profile remain unresolved.

• Exactly 27 final-prefix units make residual columns 2 through 29 strictly lexicographically increasing in the retained profile formula.
• The three-seed strictness calibration failed its predeclared conflict-and-propagation throughput gate.
• All six solver outcomes were UNKNOWN and both fresh LRAT replayers rejected every incomplete prefix.

• python3 scripts/build_r2_profile_strict_lex_v1.py --out-dir artifacts/epoch37-20260810/strict-lex-v1
• python3 checkers/check_r2_profile_strict_lex_v1.py --artifact-dir artifacts/epoch37-20260810/strict-lex-v1 --receipt artifacts/epoch37-20260810/strict-lex-v1/strict-semantic-check.json
• python3 scripts/run_r2_strict_lex_calibration_v1.py --artifact-dir artifacts/epoch37-20260810/strict-lex-v1 --seconds 5 --cpu 0
• python3 checkers/check_r2_strict_lex_calibration_v1.py --artifact-dir artifacts/epoch37-20260810/strict-lex-v1 --receipt artifacts/epoch37-20260810/strict-lex-v1/calibration-independent-check.json
• sha256sum -c artifacts/epoch37-20260810/SHA256SUMS

• .proof-experiments/20260810-000852-414079: built the 33246-variable, 165674-clause strict formula
• .proof-experiments/20260810-000901-73b894: passed 5460 truth cases and four semantic controls
• .proof-experiments/20260810-001112-7b2a77: six UNKNOWN runs and failed frozen throughput gate
• .proof-experiments/20260810-001208-06077d: independent gate reproduction and twelve proof-prefix rejection outcomes

check_r2_profile_strict_lex_v1.py independently reconstructs comparator clauses and semantics; check_r2_strict_lex_calibration_v1.py independently parses logs and invokes fresh lrat-check and CakeLPR builds.

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

None recorded.

• There are 27 adjacent comparator chains among residual columns 2 through 29, with final prefix variables 32746,32762,...,33162.
  strict-semantic-check.json and clean-room reconstruction · Retained profile (26,0,1,2) incidence formula · computed
• The strict formula has 33246 variables, 165674 clauses, and SHA-256 c63b46d5358cd8a86ecc7a684366d6a2fa1ee83ab8a2fd3b12b0f3cd8abf0355.
  strict-build-manifest.json, strict-semantic-check.json, and SHA256SUMS · Exact retained strict CNF · computed
• The frozen strictness throughput gate failed and all six LRAT prefixes were incomplete.
  calibration-independent-check.json · Seeds 0,1,2, five seconds, CPU 0, CaDiCaL 1.7.3 · computed

• Scale the unchanged strict profile (26,0,1,2) CNF on the strength of short-run throughput.
  The exact baseline/strict formulas and frozen three-seed protocol · The predeclared pairwise and geometric conflict-and-propagation gate failed. · calibration-independent-check.json · A material encoding change, checked cube split, proof-prefix reuse mechanism, or terminal evidence.
• Use the delegate's 28 strict residual-comparator units and 165675-clause prediction.
  Residual columns 2 through 29 · Twenty-eight columns have only twenty-seven adjacent comparator chains. · Independent comparator allocation and strict-semantic-check.json · A separately justified anchor-residual constraint, which would not be a residual adjacent-comparator unit.

• Fixed-point-free C5 one-orbit tail lookup
  It directly targets 888391 measured depth-six failures and may produce a directly checkable witness. · Index unused block orbits by exact residual cycle profile and test coverage-mask containment when one slot remains. · high · open
• Fixed optimal C(14,5,2) root-link completion
  It is materially distinct, with 252 completion-membership variables and 247 residual triple rows. · Bind one published optimal link and run a constructive-only completion calibration with direct witness checking. · normal · open
• Global proof-producing incidence/PB cube decomposition
  It remains the only negative route capable of excluding 30 globally. · Compile and replay one smallest disjoint calibration cube only after a material decomposition or proof-prefix reuse design. · normal · open

Objective: Determine whether exact one-orbit tail completion materially improves the fixed C5 constructive search.

First action: Fork scripts/c5_orbit_dfs_v1.py and replace ordinary branching at slots==1 by exact residual-profile and coverage-mask lookup over unused orbits.

Stop condition: Stop on an independently checked witness; redirect if matched controls do not materially reduce late depth-six failures.

• Implement an exact one-orbit residual-profile and coverage-mask lookup at slots==1 in the fixed C5 DFS.
• Run matched node-capped and wall-capped controls against the epoch-31 baseline.
• Directly validate any 30-block witness against all 455 triples; treat any capped miss as neutral.

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

GPT-5.6 Sol principal; GPT-5.6 Terra advisory experiment-verification and prior-art delegates, with the comparator-count error rejected and no model agreement counted as validation; Python 3.12.3; CaDiCaL 1.7.3; GCC; lrat-check.c; CakeLPR; SHA-256; exact integer and truth-table checks; Proof Factory run_experiment.py; web search. No CAS, proof assistant, cloud lab, or external human validator.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1536.8s

Review state

not a result claim

Attempt ID

covering-c1563-20260810-002517-28fe6c

No human review recorded.