Condition the published fixed-root-link completion formula on one deterministic compatible simple 4-regular pair-excess graph, emit and independently replay LRAT, then lift the exclusion through the certified fixed-link automorphism.

fixed-root-link exact pair-excess extension SAT

Exact pair multiplicities collapse one fixed-link completion family to a proof-producing leaf; a certified link automorphism lifts the terminal exclusion to the graph's two-element orbit.

Hypothesis: One deterministic simple 4-regular pair-excess leaf compatible with the published fixed link terminates within 10 CPU-seconds with a directly checked cover or a dual-replayed LRAT no larger than 32 MiB.

Test: Build the un-cubed fixed-link formula with all 91 residual pair equations, run CaDiCaL for 10 seconds, and require full reconstruction plus acceptance by lrat-check and CakeLPR.

The claimed local exclusion follows from exact CNF reconstruction, two independent LRAT kernels, deletion and mutation attacks, and a separately checked automorphism lift. The evidence has no ownership mechanism beyond the two-element orbit, so a broader claim would be invalid.

• No completion of the retained published fixed root link realizes the recorded simple 4-regular pair-excess graph.
• No completion realizes its distinct image under the fixed-link automorphism (4 5).
• The decisive CNF has 12,821 variables and 52,445 clauses.
• The maintained global range remains 30 <= C(15,6,3) <= 31.

• python3 scripts/fixed_link_pair_profile_v1.py --out-dir artifacts/epoch71-20260811/fixed-link-pair-profile-v2 --seconds 10
• python3 checkers/check_fixed_link_pair_profile_v1.py --artifact-dir artifacts/epoch71-20260811/fixed-link-pair-profile-v2 --out artifacts/epoch71-20260811/fixed-link-pair-profile-v2/independent-check.json
• python3 checkers/check_fixed_link_pair_profile_orbit_v1.py --artifact-dir artifacts/epoch71-20260811/fixed-link-pair-profile-v2 --out artifacts/epoch71-20260811/fixed-link-pair-profile-v2/orbit-lift-check.json
• sha256sum -c artifacts/epoch71-20260811/SHA256SUMS

• .proof-experiments/20260811-010658-3542c7: superseded replay control; CakeLPR default allocation failed and is not evidence.
• .proof-experiments/20260811-010825-2add88: terminal UNSAT in 0.480351 seconds with dual replay.
• .proof-experiments/20260811-010837-b0e109: independent full-formula and proof audit passed.
• .proof-experiments/20260811-011052-a6c54f: exact two-profile automorphism lift passed.

checkers/check_fixed_link_pair_profile_v1.py independently reconstructs the fixed-link kernel and pair rows using the earlier clean-room checker implementation; checkers/check_fixed_link_pair_profile_orbit_v1.py separately binds the terminal receipt to the independently certified link group.

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

• Certified fixed-link blockers for C(12,6,4) -> predict that exact link plus exact pair structure can yield compact replayable leaves here -> observed a 0.86 MiB dual-replayed LRAT.

• The selected fixed-link pair-profile formula is UNSAT.
  CNF SHA-256 ff230cf51d5627567e5d981c615cc3c5fd8f43236aed013ff061bf0329ef035f and LRAT SHA-256 1b1b7653beb6cb898bf5992d98a146caac373b9e5e55f3905925c8830387a31d accepted by lrat-check and CakeLPR. · One deterministic labelled excess graph inside one fixed root-link family. · proved
• The fixed-link automorphism orbit of the selected graph has size two and both members are excluded.
  artifacts/epoch71-20260811/fixed-link-pair-profile-v2/orbit-lift-check.json · The full order-two automorphism group of the retained fixed link. · proved
• The formula contains 12,821 variables, 52,445 clauses, and audits all 105 global pair equations.
  Independent clause reconstruction receipt c7ee04a4abe949345a52330c3013e6af424ab1e84ed7ac678ea15679b7cc139d. · The decisive v2 CNF. · computed

• A 30-block completion of the retained fixed link with either selected orbit member as its exact pair-excess graph.
  Exactly two labelled pair-profile families. · Complete dual-replayed UNSAT plus sound automorphism lift. · fixed-link-pair-profile.lrat and orbit-lift-check.json · A concrete defect in link identity, pair-target reconstruction, CNF semantics, LRAT replay, or automorphism binding.
• Treat the selected graph proof as an exclusion of the entire fixed link.
  All other pair-excess profiles for this link. · No exhaustive profile catalogue or ownership union was produced. · The explicit scope limits in run-receipt.json and orbit-lift-check.json. · A complete independently checked compatible-profile frontier whose every leaf is terminally excluded.

• Pair-row UNSAT core extraction
  A compact row core could block many excess graphs at once and converts the fast terminal leaf into bulk elimination. · Compile complementary half-row relaxations and run each for two proof-producing seconds. · high · open
• Exactly-owned 249-profile global proof frontier
  It retains global ownership, unlike the fixed-link graph leaf. · Adopt a materially different proof mechanism or validated assumption binding before another profile run. · normal · open
• Constructive degree-preserving search with a new move family
  A single directly checked 30-block cover would settle the target without exhaustive ownership. · Specify and cheaply calibrate a move family distinct from the closed support-three operator. · low · open

Objective: Generalize the local terminal proof into a replayable class-level pair-profile blocker.

First action: Fork the compiler to accept a manifest of retained pair rows, then build the two complementary 45/46-row relaxations.

Stop condition: Stop or redirect if both relaxations are SAT/UNKNOWN, either proof replay fails, or no surviving core can be expressed as a sound graph-class predicate.

• Instrument each of the 91 exact pair rows as a removable group.
• Run complementary half-row relaxations with two-second proof-producing limits.
• If an UNSAT half survives, continue divide-and-conquer deletion toward a core of at most 16 pair rows.
• Independently characterize the set of excess graphs blocked by any resulting core.

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

GPT-5.6 Sol served as principal investigator. GPT-5.6 Terra delegates supplied advisory prior-art and experiment-verification memos; Sol independently audited every relied-on claim and model agreement was not validation. Deterministic tools were Python 3.12.3, CaDiCaL 1.7.3, GCC, lrat-check, CakeLPR, exact integer/set arithmetic, SHA-256, and the Proof Factory experiment harness. No CAS, proof assistant, PB solver, cloud lab, external proof service, fresh network retrieval, human validator, or publication action was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1157.6s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260811-011720-6b396d

No human review recorded.