Materialized exactly-owned fixed-first profile-129 and ran one bounded proof-producing CaDiCaL ASCII-LRAT discriminator with independent ownership and result audits.

proof-producing fixed-first incidence profile frontier

Select one leaf from the independently checked 249-profile partition, materialize its ten unary-counter units, and require either a directly checked 30-cover or dual-replayed ASCII LRAT.

Hypothesis: Previously uncalibrated profile-129, with intersection profile (1,0,24,0,2,2), terminates as SAT or independently replayable UNSAT within 60 solver seconds and a 64 MiB ASCII-LRAT cap.

Test: Run CPU-pinned CaDiCaL 1.7.3 with seed 0, P0 preprocessing, 60 solver seconds, 75 wall seconds, and a 64 MiB proof cap; accept only a cover checked by independent Python and C programs or an LRAT accepted by lrat-check and CakeLPR.

The verification contract accepts only a directly checked 30-cover or complete independently replayed UNSAT evidence. The run produced neither, so the exact range remains unchanged.

• The materialized profile-129 CNF has 34210 variables and 174202 clauses and is exactly the shared fixed-first formula plus ten profile units.
• The retained necessary fixed-first frontier contains 249 profiles with exactly-one ownership; profile-129 occurs once.
• The seed-0 P0 run on profile-129 returned UNKNOWN after 59.96 process seconds.
• Both qualified LRAT replay tools reject the exact 15948931-byte incomplete proof prefix.
• No 30-cover or valid profile-129 exclusion was produced.

• python3 checkers/check_fixed_first_profile_manifest_v1.py --manifest artifacts/epoch44-20260810/fixed-first-profile-manifest-v3/profile-manifest.json --out artifacts/epoch69-20260810/profile129-lrat-v1/fresh-parent-frontier-check.json: PASS
• python3 checkers/check_profile129_materialization_v1.py --artifact-dir artifacts/epoch69-20260810/profile129-lrat-v1 --out artifacts/epoch69-20260810/profile129-lrat-v1/pre-solve-check-v2.json: PASS with four rejected mutations
• python3 scripts/run_profile129_lrat_v1.py --design artifacts/epoch69-20260810/profile129-efficiency-design.json: UNKNOWN, exit 0, 59.96 process seconds
• python3 checkers/check_profile129_result_v1.py --artifact-dir artifacts/epoch69-20260810/profile129-lrat-v1 --out artifacts/epoch69-20260810/profile129-lrat-v1/independent-result-check-v2.json: PASS, independently resolved UNKNOWN
• sha256sum -c artifacts/epoch69-20260810/SHA256SUMS: all entries OK

• .proof-experiments/20260810-234029-02ce3e: materialized profile-129 successfully
• .proof-experiments/20260810-234101-c395ae: freshly reconstructed the 249-profile exactly-once frontier
• .proof-experiments/20260810-234943-b3ea6a: independently reconstructed profile-129 and rejected unit/profile/hash mutations
• .proof-experiments/20260810-234118-104977: CaDiCaL returned UNKNOWN after 59.96 process seconds
• .proof-experiments/20260810-234346-229362: failed control exposed an incorrect assumption about CakeLPR rejection exit status
• .proof-experiments/20260810-234421-e30755: corrected independent audit confirmed UNKNOWN and dual rejection of the incomplete proof

checkers/check_profile129_materialization_v1.py independently reconstructs ownership and formula materialization; checkers/check_profile129_result_v1.py reparses the solver output and uses freshly compiled lrat-check and CakeLPR binaries to reject the incomplete proof.

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.

• Profile-129 is an unresolved necessary profile with vector (1,0,24,0,2,2), r=0, q=11, and ten reconstructed assumptions.
  Fresh parent-frontier and profile-specific check receipts. · Hash-bound fixed-first 249-profile manifest. · computed
• The bounded profile-129 run is nonterminal.
  CaDiCaL log and independently parsed solver receipt show exit 0, no SAT/UNSAT line, and 59.96 process seconds. · Exact CNF SHA-256 7ddd4fd2801eadded09b78b9ca2eb0b893b024e766b0e5985406ae3c09ab77b3, seed 0, P0, 60-second limit. · computed
• The emitted LRAT prefix is not an UNSAT certificate.
  Fresh lrat-check returned NOT VERIFIED and CakeLPR reported empty clause not derived. · Proof prefix SHA-256 450ab87570b9ddded759dacee880431de283ac0a470a0cf127d4d7ba3561b9b5. · computed
• The maintained upper and lower bounds remain 31 and 30.
  Maintained LJCR upper and lower tables checked on 2026-08-10. · C(15,6,3) source-status baseline. · computed

• Escalate the unchanged shared-profile/P0 profile-129 formulation solely by lengthening its runtime.
  Exact profile-129 CNF, seed 0, CaDiCaL 1.7.3, P0 proof-producing formulation. · The frozen discriminator was nonterminal and produced no validated mathematical progress. · solver-receipt.json and independent-result-check-v2.json · A material encoding change, independently checked cube split, or proof-prefix method with a qualified replay path.
• Use the six second-block representatives as global ownership cases.
  Global exclusion accounting in this epoch. · No exact-once ownership proof was supplied; the retained disjoint 249-profile frontier was used instead. · fresh-parent-frontier-check.json · An independently checked exact-once ownership rule covering every normalized model.

• Fixed-second reusable-totalizer encoding for profile-129.
  The unique n0 block admits S9 normalization and predicts a 5.36% clause reduction relative to the shared materialization. · Compile targets n2=24,n4=2,n5=2 and independently check predicted dimensions before a five-second preprocessing test. · high · open
• Canonical root-link catalogue.
  It is materially different from global profile SAT and could quotient a substantial completion space. · Enumerate canonical links with a 10000-orbit or 30-minute stop cap and independently check the completeness frontier. · normal · open
• Constructive degree-preserving search with direct cover checking.
  A single 30-block witness would settle the problem without exhaustive negative certification. · Run a fresh bounded operator comparison only after identifying a move family materially different from the closed support-three generator. · normal · open

Objective: Compile and qualify the fixed-second reusable-totalizer encoding of profile-129.

First action: Adapt scripts/build_fixed_second_reusable_profile_v1.py by changing the reusable weights to (2,4,5) and targets to {2:24,4:2,5:2}, then independently reconstruct the stabilizer normalization and clauses.

Stop condition: Redirect on equivalence failure, source/hash mismatch, dimensions other than 33654 variables and 164858 clauses, less than 5% clause reduction, or any terminal output lacking independent validation.

• Adapt scripts/build_fixed_second_reusable_profile_v1.py to profile-129 with weights (2,4,5) and targets (24,2,2).
• Write a separately reconstructed checker for the S9 normalization, exact residual counts, and CNF clauses.
• Require predicted dimensions 33654 variables and 164858 clauses and at least 5% clause reduction before another proof-producing run.
• If the gate fails, redirect to the canonical root-link catalogue instead of lengthening the current run.

• https://www.coveringrepository.com/systems.aspx?k=6&t=3&m=-1 ↗
• https://ljcr.dmgordon.org/cover/table.html ↗
• https://ljcr.dmgordon.org/cover/low_tab.html ↗
• https://arxiv.org/abs/math/9502238 ↗
• https://github.com/dmgordo/LJCR ↗

GPT-5.6 Sol served as principal investigator. Two GPT-5.6 Terra delegates supplied advisory experiment-verification and prior-art memos; Sol independently audited relied-on claims and promoted their provenance. Deterministic tools were Python 3.12.3, CaDiCaL 1.7.3, GCC, retained lrat-check C source, and retained CakeLPR sources. Web search checked the Covering Repository, maintained LJCR tables, GitHub dataset, and arXiv. No CAS, proof assistant, PB solver, cloud lab, external proof service, or human validator was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1623.1s

Review state

not a result claim

Attempt ID

covering-c1563-20260810-235627-61125f

No human review recorded.