S9-normalized fixed-second reusable-totalizer encoding and matched proof-producing calibration for exactly-owned profile-129

fixed-second reusable-totalizer SAT

Normalize profile-129's unique disjoint block under S9, encode residual intersection counts (n2,n4,n5)=(24,2,2) with three reusable unary totalizers, and compare against the matched legacy profile formula.

Hypothesis: The S9-normalized profile-129 formula has exactly 33654 variables and 164858 clauses and either terminates or achieves at least 1.25x geometric-mean conflict throughput with no worse LRAT bytes per conflict than the legacy formula.

Test: Clean-room reconstruction of all 84 S9 normalizations and every added clause, followed by four alternating seed/variant five-second CaDiCaL LRAT runs and independent log parsing and dual replay.

The experiment provides trustworthy engineering evidence but neither a 30-block witness nor a replayed UNSAT certificate. The maintained range therefore remains 30 <= C(15,6,3) <= 31.

• All 84 possible unique disjoint blocks in profile-129 lie in one explicitly checked S9 orbit fixing F=012345.
• The fixed-second reusable profile-129 CNF has 33654 variables and 164858 clauses.
• Relative to the legacy profile-129 CNF, this removes 556 variables and 9344 clauses.
• All four five-second CaDiCaL runs were UNKNOWN.
• Both independent LRAT replayers rejected all four incomplete proof prefixes.
• The exact covering range remains 30 <= C(15,6,3) <= 31.

• python3 checkers/check_fixed_second_profile129_reusable_v1.py --artifact-dir artifacts/epoch70-20260811/profile129-reusable-v1 --out artifacts/epoch70-20260811/profile129-reusable-v1/independent-formula-check.json: PASS
• python3 scripts/run_fixed_second_reusable_calibration_v1.py --artifact-dir artifacts/epoch70-20260811/profile129-reusable-v1 --formula-check artifacts/epoch70-20260811/profile129-reusable-v1/independent-formula-check.json --out-dir artifacts/epoch70-20260811/profile129-reusable-calibration-v1 --seconds 5: four UNKNOWN runs
• python3 checkers/check_fixed_second_reusable_calibration_v1.py --run-receipt artifacts/epoch70-20260811/profile129-reusable-calibration-v1/run-receipt.json --out artifacts/epoch70-20260811/profile129-reusable-calibration-v1/independent-result-check.json: PASS, route held
• sha256sum -c artifacts/epoch70-20260811/SHA256SUMS: all entries OK

• .proof-experiments/20260811-002328-cb334f: independent formula audit passed all 84 normalizations and exact byte reconstruction
• .proof-experiments/20260811-002346-8e9fd3: four matched runs completed, all UNKNOWN
• .proof-experiments/20260811-002437-faf358: independent parsing recovered both failed efficiency gates and both replayers rejected every prefix

checkers/check_fixed_second_profile129_reusable_v1.py independently reconstructed the formula and symmetry quotient. checkers/check_fixed_second_reusable_calibration_v1.py independently reparsed the runs and rebuilt lrat-check and CakeLPR; both rejected every incomplete prefix.

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

• Finite group actions -> predict that profile-129's unique disjoint block has an exact 84-to-1 normalization -> all 84 explicit mappings passed.
• Certified C(12,6,4) proof discipline -> predict dual replayers distinguish incomplete proof prefixes -> both tools rejected all four UNKNOWN prefixes.
• Reusable cardinality networks -> predict that smaller formulas improve proof search -> formula size improved, but the matched throughput and proof-efficiency prediction was falsified.

• Profile-129 has an existence-preserving canonical representative with disjoint block 67891011.
  Explicit checked S9 bijections for all 84 complement six-subsets. · Fixed-first profile (1,0,24,0,2,2). · proved
• The reusable profile-129 formula has 33654 variables and 164858 clauses.
  Independent byte reconstruction, formula SHA-256 3a685b9d768761457b9c895b2ab2ce0a004f427db3946609897855663cd2e7f2. · Pinned epoch-9 r=0 source and residual targets (24,2,2). · computed
• The reusable encoding failed the frozen performance gate.
  Geometric-mean conflict-rate ratio 0.8841950911 and proof-bytes-per-conflict ratio 1.1627292875. · CaDiCaL 1.7.3, seeds 0 and 1, five-second proof-producing runs. · computed
• None of the four emitted prefixes proves UNSAT.
  Fresh lrat-check and CakeLPR builds explicitly rejected every prefix. · The four exact LRAT files listed in the epoch-70 run receipt. · computed

• Scale the unchanged fixed-second reusable-totalizer profile-129 formula with CaDiCaL solely by increasing runtime.
  Exact CNF SHA-256 3a685b9d768761457b9c895b2ab2ce0a004f427db3946609897855663cd2e7f2, CaDiCaL 1.7.3, seeds 0 and 1. · Both throughput and proof-efficiency gates failed and no terminal evidence appeared. · artifacts/epoch70-20260811/profile129-reusable-calibration-v1/independent-result-check.json · A materially different counter encoding or qualified solver, validated proof-prefix reuse, or terminal SAT/dual-replayed UNSAT evidence.
• Treat the profile-local 84-to-1 normalization as a global reduction.
  The full 249-profile uncertainty. · The quotient applies only inside exactly-owned profile-129 and eliminates no profile. · Parent manifest binding and the scope limits in both checker receipts. · An independently checked ownership construction extending an analogous quotient across every live profile.

• Two-layer root-link/extension-blocker architecture
  It is materially distinct from global profile SAT and can produce exact-link blockers with replayable evidence before attempting orbit closure. · Build and independently check one un-cubed epoch-52 fixed-link extension formula with one pair-excess profile. · high · open
• Constructive degree-preserving search with a new move family
  A single checked 30-block witness settles the problem without global UNSAT accounting. · Specify a move family materially different from the closed support-three operator before running a matched pilot. · normal · open
• Alternative qualified proof-producing solver or proof-prefix reuse
  The current bottleneck is proof search and certificate growth rather than formula size. · Run one terminal calibration control only after exact proof-format replay and prefix-binding semantics are independently qualified. · normal · open

Objective: Test whether exact root-link extension blockers can produce replayable local eliminations suitable for later symmetry-complete orbit closure.

First action: Read artifacts/epoch50-20260810/fixed-link-completion-v1/formula-metadata.json and artifacts/epoch52-20260810/fixed-link-lex-degree-prefix-audit-v1.json, then specify exact blocker semantics before generating a formula.

Stop condition: Stop or redirect on semantic reconstruction mismatch, pair-target mutation acceptance, UNKNOWN, proof-budget overflow, replay failure, or orbit-ownership ambiguity.

• Read the epoch-50 fixed-link metadata and epoch-52 lex-degree audit.
• Define exact-link blocker semantics and the ownership boundary before encoding.
• Build one un-cubed residual extension formula with one admissible pair-excess profile.
• Independently reconstruct uncovered-triple clauses and all 105 residual pair equations.
• Treat UNSAT as an exact-link blocker only after complete dual replay; require verified orbit closure before any broader lift.

• https://www.coveringrepository.com/systems.aspx?k=6&t=3&m=-1 ↗
• https://arxiv.org/abs/2607.23766 ↗
• https://arxiv.org/abs/math/9502238 ↗

GPT-5.6 Sol was principal investigator and designed, implemented, executed, and audited this epoch. GPT-5.6 Terra delegates supplied advisory experiment-verification and prior-art memos; Sol promoted them with provenance, independently audited relied-on claims, and did not count model agreement as validation. Deterministic tools were Python 3.12.3, CaDiCaL 1.7.3, GNU time, GCC, retained lrat-check and CakeLPR sources, exact integer arithmetic, SHA-256, and the Proof Factory experiment harness. Web open/search attempted to check the maintained source and arXiv comparator but returned no parseable newer content. No CAS, proof assistant, PB solver, cloud lab, external proof service, or human validator produced terminal evidence.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1079.5s

Review state

not a result claim

Attempt ID

covering-c1563-20260811-003221-2c4008

No human review recorded.