Root-normalized SAT feasibility test for the doubled-edge local-link degree profile 7,5^13, followed by independent witness validation.

pair-excess stratification and local-link feasibility

Fix the unique degree-7 point, normalize one of its seven incident blocks to 0123, encode pair coverage and exact degrees with a truncated bidirectional totalizer, solve, decode, and cross-check the model.

Hypothesis: There is no 18-block C(14,4,2) cover with ordered point-degree sequence 7,5^13.

Test: Solve a byte-reproducible rooted CNF; SAT must decode to 18 blocks passing two direct all-pairs checkers and an independent fixed-model Z3 encoding.

SAT is sufficient for the existential local claim because the decoded block list can be checked without trusting the encoding. Both direct checkers found 18 distinct blocks, exact degrees, and coverage of all 91 pairs; Z3 independently accepted all 1001 fixed primary decisions.

• There exists an 18-block C(14,4,2) cover with ordered point-degree sequence 7,5^13.
• The displayed witness contains seven high-point triples of degree profile 1^6 2^6 3 and eleven residual blocks.
• The route attempting to exclude all doubled-edge skeletons through local-link infeasibility is invalid.
• No claim about the existence of a 54-block C(15,5,3) cover follows.

• python3 checkers/check_local_link.py artifacts/local-link-pilot-20260808/live-7-5x13-witness.txt --profile 7,5,5,5,5,5,5,5,5,5,5,5,5,5
• python3 checkers/check_local_link_masks.py artifacts/local-link-pilot-20260808/live-7-5x13-witness.txt --profile 7,5,5,5,5,5,5,5,5,5,5,5,5,5
• Z3 fixed-model experiment 20260808-160043-a0e4e1 returned sat.
• sha256sum -c artifacts/local-link-pilot-20260808/manifest.sha256 passed every entry.

• .proof-experiments/20260808-155337-be1d7a and 20260808-155338-6f5bcd: byte-identical DFA control generation
• .proof-experiments/20260808-155344-6e7e76 and 20260808-155357-1086c8: published CNF control SAT and direct check
• .proof-experiments/20260808-155404-a7865f and 20260808-155451-51ef52: independent Z3 control SAT and direct check
• .proof-experiments/20260808-155946-6c4f05 and 20260808-155946-7a85f3: byte-identical rooted totalizer generation
• .proof-experiments/20260808-155952-a102f2: live SAT in 1.64 seconds
• .proof-experiments/20260808-160008-597381: tuple checker accepted
• .proof-experiments/20260808-160043-a0e4e1: independent fixed-model Z3 encoding accepted
• .proof-experiments/20260808-160044-19c2d9: bit-mask checker accepted
• .proof-experiments/20260808-160648-21d400: final manifest audit passed

checkers/check_local_link.py verifies tuples and all 91 pairs; checkers/check_local_link_masks.py independently uses 14-bit masks; scripts/local_link_z3.py provides a materially different PB encoding with every primary variable fixed.

not_requested

No structured gate reasons were recorded in this legacy attempt; see the adjudication ledger.

Original model outcome

progress

Public classification

progress

• Terra star decomposition -> predict that one high-point block can be normalized safely -> rooted compact SAT produced a checked witness.
• Certified-covering SAT practice -> predict that semantic cross-encoding catches cardinality or variable-map errors -> fixed-model Z3 agreed with both direct checkers.
• Unary cardinality encoding -> predict stronger and smaller propagation than the one-hot DFA -> variables and clauses fell by about half and SAT appeared in 1.64 seconds.

• The displayed 18 blocks cover every pair of 14 points and have ordered degrees 7,5^13.
  Witness SHA-256 936a3ca8e42a106e14f4666f52057f43cec27928d6170046cee33699e6bd6c4e; tuple and bit-mask checker receipts. · The displayed witness only. · computed
• Requiring block 0123 is complete after fixing the unique degree-7 point as 0.
  Every candidate has seven blocks through 0, and S13 acts transitively on their residual triples. · All local links with ordered profile 7,5^13. · proved
• The rooted totalizer CNF regenerated byte-identically.
  Both CNFs have SHA-256 c3aadc55c6910b70e354146202bafa4959110448763f0e04a73dd5173a007650. · The recorded generator, arguments, and environment. · computed

• Prove the 7,5^13 local-link profile impossible to eliminate all doubled-edge skeletons.
  All 18-block C(14,4,2) covers with ordered degrees 7,5^13. · The checked witness realizes the profile. · artifacts/local-link-pilot-20260808/live-7-5x13-witness.txt and three independent validations · None under the same definition.
• Use a solver timeout, missing receipt, or raw process termination as evidence about local feasibility.
  The three failed DFA live runs. · They emitted no status or receipt and therefore have no mathematical content. · Empty run directories 20260808-155514-403ad0, 20260808-155614-930c97, and 20260808-155756-5acf79 · A deterministic rerun returning a checked witness or replayable UNSAT certificate.

• Fixed-link global extension from the checked 7,5^13 seed.
  SAT settles C(15,5,3)=54, and fixing all 18 through-point blocks gives strong propagation. · Generate the 2002-variable residual extension CNF and run a bounded totalizer/CaDiCaL pilot. · high · open
• Root-block-only global constructive SAT.
  It covers all link isomorphism classes and SAT directly settles the target, but is likely harder. · Use exact degree 18 and fixed global block 01234 with the validated totalizer. · normal · open
• Joint skeleton-and-root canonical orbit enumeration.
  This is necessary for a sound complete negative campaign if constructive pilots fail. · Enumerate distinguished-block orbits under each skeleton automorphism group and independently audit orbit coverage. · normal · open

Objective: Determine whether the validated 7,5^13 link extends to a 54-block C(15,5,3) cover.

First action: Implement scripts/fixed_link_extension_cnf.py to generate the 2002-variable residual problem specified in records/attempts/epoch-0002-local-link-20260808.json, then run it through run_experiment.py.

Stop condition: A directly checked 54-block union settles the target at 54; replay-checked UNSAT closes only this fixed seed; timeout or failed controls redirects to the broader root-block constructive calibration.

• Implement the fixed-link residual extension CNF over the 2002 five-subsets avoiding a new global point.
• Require exactly 36 residual blocks, residual degrees 11 at the local degree-7 point and 13 at each other point, and coverage of every triple not already covered by the fixed link.
• Validate any SAT union directly against all 455 triples and all 15 degree equations.
• Treat UNSAT as excluding only this exact fixed link unless a complete local-link orbit census is added.

• 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://ljcr.dmgordon.org/cover/show_cover.php?k=4&t=2&v=14 ↗
• https://arxiv.org/abs/2607.23766 ↗

GPT-5.6 Sol principal designed, implemented, and audited the epoch. GPT-5.6 Terra delegates supplied bounded advisory reconnaissance; the relied-on root-normalization suggestion was promoted with provenance and independently proved and implemented by Sol. Python 3.12.3 generated and checked artifacts. CaDiCaL 1.7.3 found the SAT model. Z3 4.13.0 performed independent PB validation. Web browsing checked current status and prior art. No CAS, proof assistant, external publication, lab job, or additional sub-agent was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1419.5s

Review state

not a result claim

Attempt ID

covering-c1553-20260808-161009-a1d172

No human review recorded.