Test local feasibility of all five forced root-link degree types using flat native pseudo-Boolean set-selection models and direct witness checking.

root-link local-feasibility classification

Represent each 12-block link using one Boolean selector for each of the 2002 five-subsets, with exact degrees and all 91 pair-covering constraints.

Hypothesis: Each of the five degree multisets forced on a 12-block root link is locally realizable by twelve distinct 5-subsets covering every pair of 14 points.

Test: Run Z3 4.13.0 for 20 seconds on each type and accept only explicit links independently checked for exact degrees, distinctness, and all 91 pairs.

UNKNOWN statuses are neither witnesses nor exclusions. Failure on the known-SAT control removes the encoding's information value under the tested cap, so the epoch records no field progress.

• Under the frozen flat Z3 encoding, seed, and 20-second-per-type cap, all five root-link cases returned UNKNOWN.
• The archived 12-block type-(5^4,4^10) link independently checks all 91 pairs and has labelled degree vector (5,5,4,4,4,4,5,5,4,4,4,4,4,4).
• No root-link type or global covering family was excluded.

• Five-type harness run 20260812-105044-9abd8c completed in 105.609 seconds; each solver call reported timeout.
• Independent audit 20260812-105341-7ddc9f returned PASS_PROTOCOL_NO_CLASSIFICATION and rejected three mutations.
• sha256sum -c artifacts/epoch116-20260812/SHA256SUMS passed for every retained artifact.
• python3 -m py_compile passed for the producer and checker.

• .proof-experiments/20260812-105044-9abd8c: five UNKNOWN timeouts, total solver time 100.052 seconds.
• .proof-experiments/20260812-105341-7ddc9f: independent protocol audit passed, archived control accepted, three mutations rejected.

checkers/check_root_link_five_type_feasibility_v1.py independently derives the partitions of four, verifies witnesses using set and bit-mask coverage, validates the archived positive control, and treats UNKNOWN as no claim.

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 decomposition practice -> operational prediction that a route must pass a known terminal control before scale-up -> flat Z3 failed the known-SAT link control.
• Set-system symmetry -> operational prediction that selector variables remove block-order redundancy -> the exact 12! quotient was obtained but did not create adequate propagation.

• The archived type-(5^4,4^10) link contains twelve distinct 5-subsets, has the recorded labelled degree vector, and covers all 91 pairs.
  artifacts/epoch50-20260810/published-c1452-link.txt plus artifacts/epoch116-20260812/root-link-five-type-independent-check.json · The single maintained C(14,5,2)=12 construction · computed
• All five frozen flat-PB runs returned UNKNOWN under the declared cap.
  artifacts/epoch116-20260812/root-link-five-type-result.json · Z3 4.13.0, seed 0, 20 seconds per type, frozen selector encoding · computed

• Use the flat 2002-selector Z3 native-PB encoding at 20 seconds per type as a root-link classifier.
  All five forced labelled root-link degree targets under the frozen encoding and seed · Every case timed out, including the known-SAT positive control. · artifacts/epoch116-20260812/root-link-five-type-result.json and independent positive-control check · A material encoding or search change that decides the archived control within five seconds and passes independent formula reconstruction.

• SAT-friendly root-link positive-control compilation
  A known witness gives a decisive seconds-scale gate before testing unknown types. · Compile the archived type-(5^4,4^10) instance to CNF, force its twelve source selectors in a control arm, independently reconstruct clauses, and require SAT within five seconds. · high · open
• Complete 62437-profile parent-rich pair-surplus ledger
  This remains the prerequisite for globally aggregatable certified leaves. · After explicit human approval, materialize the exact remaining 38705 profiles and independently reconcile the full ledger. · high · open
• Proof-producing incidence/PB calibration
  A replayable PB chain could generate terminal evidence. · Provision only pinned official RoundingSat, VeriPB, and CakePB artifacts, then run the saved overdegree calibration. · normal · open

Objective: Qualify a root-link search encoding on a known witness before spending compute on unknown types.

First action: Compile the archived type-(5^4,4^10) link instance to SAT-friendly CNF with a forced-model control and an independently reconstructed clause manifest.

Stop condition: Redirect immediately on positive-control timeout, clause mismatch, invalid model, or unreplayed UNSAT.

• Do not lengthen the flat Z3 timeout.
• Build a SAT-friendly CNF positive-control calibration using the archived link and require terminal SAT within five seconds.
• Advance to an unknown root type only if formula reconstruction, positive-control recovery, and mutation checks pass.
• Do not launch the remaining 38705-profile parent materialization without explicit human approval.
• Keep native PB proof search held until pinned RoundingSat, VeriPB, and CakePB pass the saved calibration.

• 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://ljcr.dmgordon.org/cover/show_cover.php?k=6&t=3&v=15 ↗
• https://arxiv.org/abs/math/9502238 ↗
• https://arxiv.org/abs/2607.23766 ↗

GPT-5.6 Sol principal investigator; two GPT-5.6 Terra delegates supplied advisory memos only. Deterministic tools: Python 3.12.3, Z3 4.13.0 native pseudo-Boolean constraints, exact set/bit-mask arithmetic, SHA-256, py_compile, and the computational-researcher experiment harness. No CAS, proof assistant, replayable proof, cloud lab, external validator, or system installation was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1009.4s

Review state

not a result claim

Attempt ID

covering-c1563-20260812-105816-a7b306

No human review recorded.