One hash-bound type-4 leaf coupling an exact labelled pair-excess skeleton, five residual-margin profiles, and the first minimum residual-triple orbit

joint labelled pair-excess skeleton and literal residual coverage

Canonicalize one skeleton under the 10,368-element type-4 stabilizer, then solve a 2,717-variable native-PB formula enforcing 49 residual blocks, all 105 pair multiplicities, 15 point degrees, 25 root margins, and two literal coverage clauses.

Hypothesis: The first hash-bound joint skeleton/profile/coverage leaf is literal-feasible and will produce a checked 49-block residual witness within 90 seconds.

Test: Run Z3 4.13.0 for 90 seconds on the exact leaf; accept SAT only after direct non-Z3 witness checking, and accept UNSAT only after replayable proof validation.

UNKNOWN proves neither feasibility nor infeasibility. The checker validated only that the intended canonical leaf and exact constraint maps were encoded in the recorded experiment scope.

• For the exact recorded native-PB protocol, Z3 4.13.0 returned UNKNOWN after 90.011973 seconds, 1,112,405 conflicts, and 4,922,916 decisions.
• A separate non-Z3 implementation reconstructed the 10,368-element stabilizer, canonical skeleton, all 105 pair targets, 15 point targets, five margin profiles, and the selected two-triple orbit.
• No 54-block cover was found and no leaf was excluded.

• python3 scripts/type4_joint_skeleton_coverage_leaf_v1.py under experiment 20260809-222833-c699c1
• python3 checkers/check_type4_joint_skeleton_coverage_leaf_v1.py under experiment 20260809-223105-4b93af
• sha256sum -c artifacts/type4-joint-skeleton-coverage-leaf-20260809/manifest.sha256

• .proof-experiments/20260809-222833-c699c1: Z3 UNKNOWN after 90.011973 seconds
• .proof-experiments/20260809-223105-4b93af: independent checker PASS_UNKNOWN_SCOPE_ONLY

checkers/check_type4_joint_skeleton_coverage_leaf_v1.py is a separate non-Z3 implementation. It validates the selected orbit and every target map but correctly assigns no mathematical conclusion to UNKNOWN.

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.

• The recorded canonical skeleton has component partition [2,2,2,2,2,2,3] and weighted degree two at every point.
  Independent reconstruction in artifacts/type4-joint-skeleton-coverage-leaf-20260809/independent-check.json · Canonical skeleton SHA-256 3b84decf42771f84b289d8a4c4dde0c7e56ae68bced2fdd58ea94741a2200739 · computed
• The recorded formula represents 2,717 residual block variables with 105 exact pair rows, 15 point rows, 25 root-margin rows, and two coverage rows.
  Producer result and independent target-map reconstruction · SMT formula SHA-256 6bc2a5d6602dcf9430161f522161db1ae1500a38be501228a9621a463d3ab48f · computed
• The native-PB run returned UNKNOWN at its 90-second cap.
  .proof-experiments/20260809-222833-c699c1/experiment.json · Z3 4.13.0, seed 0, exact recorded formula · computed

• Repeat the complete fixed-pair {4,5} link as a standalone challenger.
  The frozen 395-signature, 754-target type-4 frontier · The prior complete 431-cell census retained every target with independently checked witnesses. · artifacts/type4-complete-pair-link-gate-20260809/independent-check.json · Couple it to genuinely new labelled information, as this epoch did.
• Scale the same Z3 native-PB joint-leaf protocol or enlarge its triple orbit.
  The recorded canonical skeleton/profile leaf and Z3 4.13.0 encoding · The smallest predeclared literal test already returned UNKNOWN after more than one million conflicts. · artifacts/type4-joint-skeleton-coverage-leaf-20260809/result.json · A materially different exact encoding with matched-cap improvement or replayable proof production

• Compact proof-producing encoding of the immutable joint leaf
  It cheaply distinguishes semantic hardness from native-PB encoding weakness. · Compile the same 105 pair rows with a BDD or compact cardinality network and run a 5,000-conflict matched pilot. · high · open
• Multi-basin exact-degree constructive repair
  A checked 54-block witness directly settles the problem and the previous radius-five exhaustion covered only one basin. · Generate independently distinct exact-degree seeds and measure bounded repair trajectories before any large search. · normal · open

Objective: Determine whether the joint leaf is intrinsically hard or merely poorly represented by native PB.

First action: Compile artifacts/type4-joint-skeleton-coverage-leaf-20260809/leaf.smt2 semantics into one compact proof-producing CNF and run a seed-0 5,000-conflict pilot.

Stop condition: Redirect on UNKNOWN without material propagation improvement; stop immediately on checked SAT or replay-verified UNSAT.

• Compile the same immutable leaf using one compact proof-producing cardinality or BDD encoding.
• Run a matched 5,000-conflict pilot and retain it only for SAT, replay-verified UNSAT, or a material propagation reduction.
• If the compact pilot fails its gate, redirect campaign compute to multi-basin exact-degree constructive repair.

• 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://arxiv.org/abs/math/9502238 ↗
• https://arxiv.org/abs/2607.23766 ↗

GPT-5.6 Sol principal audited the prior artifacts, selected and implemented the discriminator, ran the experiments, interpreted UNKNOWN conservatively, and wrote the durable checkpoint. GPT-5.6 Terra delegates supplied bounded advisory prior-art and verification memos; their agreement was not validation, and their relied-on guidance was promoted with provenance. Python 3.12.3, Z3 4.13.0, exact combinatorial enumeration, SHA-256, the project run_experiment harness, a separate non-Z3 checker, maintained-source inspection, and bounded web/literature searches were used. No lab job, package installation, system modification, external publication, or external write occurred.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1095.7s

Review state

not a result claim

Attempt ID

covering-c1553-20260809-223623-40568f

No human review recorded.