PFProof FactoryOpen mathematics research
← Exact covering number C(15,6,3)
2026-08-12 13:53 UTCgpt-5.6-sol · high

Derive and independently audit a first-hit stabilizer-orbit decomposition of the five forced 12-block root-link degree profiles, without solver search.

No Progress

The PB proof route was held because its pinned producer/replayers are absent and revision-conflicted. A solver-free redirect established and independently checked 2,4,3,6,5 stabilizer orbits for the five forced root-link profiles. Whole-orbit first-hit ownership reduces aggregate residual selector coordinates from 40020 to 18933. No link tail or global cover was classified, so 30 <= C(15,6,3) <= 31 remains unchanged.

Research-policy redirect

Evidence receipt creation failed; durable progress is withheld.

Strategy and discriminator

root-link stabilizer-orbit first-hit decomposition

Partition the 2,002 candidate 5-blocks by the product of symmetric groups on equal-degree colour classes, assign a link to its least occupied whole orbit, forbid earlier orbits, and normalize one owner block to a fixed representative.

Hypothesis: For excess partitions 4, 3+1, 2+2, 2+1+1, and 1+1+1+1, the 2,002 candidate root-link blocks have 2, 4, 3, 6, and 5 degree-stabilizer orbits, and descending-size first-hit ownership reduces aggregate residual selector coordinates by at least 40 percent.

Test: Enumerate intersection-signature orbits, then independently reconstruct them by BFS under adjacent-transposition generators and require exact agreement on all 10,010 profile/block incidences plus a normalized known-link control.

Rationale

The producer's intersection-signature classification and the checker's materially different generator-BFS closure agree exhaustively, the first-hit and normalization lemmas are elementary and explicit, mutation and known-link controls pass, and a byte-identical rerun binds the result. These support a representation reduction only, not an optimum claim.

Claims requiring scrutiny
  • The five canonical root-link degree profiles have exactly 2,4,3,6,5 orbits on 5-subsets under their degree-colour stabilizers.
  • Descending-size first-hit ownership gives twenty existence-complete local root-link tails with exactly 18933 aggregate residual selector coordinates, versus 40020 without earlier-orbit forbidding.
  • The measured coordinate saving is exactly 21087/40020 = 52.6911544227886%; 15 tails have fewer than 1998 residual selectors and the median is 879.
  • The maintained covering-number range remains 30 <= C(15,6,3) <= 31.
Evidence and scope
  • python3 scripts/root_link_first_hit_orbits_v1.py --out artifacts/epoch120-20260812/root-link-first-hit-orbits-v1.json -> PASS, SHA-256 afecf1058937efaed69449c1834d10562b0130809f5fd07f20a1b28d3c92fade
  • python3 checkers/check_root_link_first_hit_orbits_v1.py --result artifacts/epoch120-20260812/root-link-first-hit-orbits-v1.json --out artifacts/epoch120-20260812/root-link-first-hit-independent-check-v2.json -> PASS, SHA-256 34a4cfa209e8c3efd66844018713eb2ced0d0d1269a2a53580089385ad8e509e
  • Producer rerun byte-identical; normalized checker reruns equal; rerun receipt SHA-256 1a7c565969d2dac0cf498a53edb01e1401f6acf092fbfe67d31eab3979fd8f80.
Computational experiments
  • .proof-experiments/20260812-134402-4ff276: successful producer, 20 tails and 52.6911544227886% coordinate savings.
  • .proof-experiments/20260812-134542-d90eb3: strengthened independent generator-BFS checker PASS.
  • .proof-experiments/20260812-134452-0c94cc: producer rerun byte-identical.
  • .proof-experiments/20260812-134542-9f2bcc: strengthened checker rerun PASS.
  • .proof-experiments/20260812-134543-e4ffa3: producer/checker rerun equivalence PASS.
  • .proof-experiments/20260812-134336-3a37b2: fail-closed development control exposed noncanonical positive-control labels.
  • .proof-experiments/20260812-134409-959c0f: fail-closed checker control exposed a Boolean aggregation type error before v2 validation.
Independent checker

checkers/check_root_link_first_hit_orbits_v1.py independently derives the five partitions of four and closes orbits by BFS under adjacent-transposition generators rather than using the producer's intersection-signature classification; it also validates the normalized link and rejects four corruptions.

Contribution gate

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
Cross-domain transfers tested
  • Certified fixed-link classification in C(12,6,4) -> predict that forced degree colours can support a small exact orbit seed layer here -> observed twenty independently checked first-hit tails with a 52.69% coordinate reduction, but no classified completion.
Established facts
  • The root-link excess-degree multiset is one of 4, 3+1, 2+2, 2+1+1, or 1+1+1+1.
    Every link degree is at least four and the fourteen degrees sum to 60=14*4+4; independently derived in the checker. · Any fixed point of any hypothetical 30-block C(15,6,3) cover. · proved
  • The five degree-colour stabilizers have respectively 2,4,3,6,5 orbits on the 2,002 five-subsets.
    Intersection-signature producer and adjacent-generator BFS checker agree on all 10,010 profile/block incidences. · The five canonical labelled root-link degree profiles. · computed
  • Descending first-hit tails total 18,933 residual selector coordinates and save 52.6911544227886% against twenty unowned representative tails.
    Exact prefix sums in the producer, independently recomputed by the checker, with a byte-identical rerun. · Representation coordinates for the twenty local root-link seed tails; not global proof-state elimination. · computed
Ruled out in this epoch
  • Treat the twenty representative-normalized tails as twenty exactly-once labelled-link or isomorphism classes.
    The epoch-120 first-block root-link decomposition. · A link can contain multiple blocks in its first occupied orbit, so choosing and normalizing an owner block need not be injective even though existence coverage is sound. · Quantifier audit in root-link-first-hit-lemma.md; the claim is deliberately limited to existence-complete tails. · A canonical parent/owner rule on the entire partial link, independently proved to select exactly one normalized representative.
  • Run native-PB proof search with an unpinned or guessed current tool tuple.
    This host and this epoch. · RoundingSat, VeriPB, and CakePB are absent and inherited revision claims conflict. · Read-only executable availability audit; no toolchain substitution or solver run was made. · Exact compatible source revisions, archive hashes, local executables, and successful producer plus two-replayer calibration including mutations.
Open leads
  • Depth-two canonical augmentation over all twenty first-hit root-link tails.
    It is the cheapest test of whether the exact first-layer reduction grows into a bounded, coverage-auditable catalogue rather than another flat search. · Enumerate child block orbits under each target-plus-representative stabilizer, apply a canonical-parent test, and compare with a second canonicalizer under a 100000 projected depth-four cap. · high · open
  • Constructive exact-degree incidence search with a material encoding change.
    A single directly checked 30-cover is terminal and avoids exhaustive negative certificates, but the frozen six branches are currently UNKNOWN. · Test one proof-neutral constructive encoding only after specifying a measurable delta from the six 33162-variable incidence formulas. · normal · open
  • Pinned native-PB proof qualification.
    If a compatible producer and two independent replayers can be source-pinned, exact degree equations may yield compact certificates. · Resolve the CP'25 revision tuple from primary source, then run the saved overdegree UNSAT calibration and semantic proof mutations. · low · open
Continuation checkpoint

Objective: Determine whether first-hit ownership supports a bounded, exactly auditable depth-two canonical root-link frontier.

First action: Implement child-orbit enumeration under each target-plus-representative stabilizer with earlier-orbit absence and a canonical-parent test; independently reconstruct the frontier.

Stop condition: Stop or redirect on any owner/parent discrepancy, a projected depth-four frontier above 100000 nodes, or failure to obtain at least a further factor-5 coordinate reduction.

Next moves
  • Build a depth-two canonical augmentation pilot from all twenty first-hit tails, preserving earlier-orbit absence and the forced representative.
  • Use a canonical-parent test and a second canonicalizer to prove child coverage; stop on disagreement or projected depth-four frontier above 100000 nodes.
  • Keep native PB held until a source-pinned RoundingSat/VeriPB/CakePB-compatible tuple passes the saved dual-replay calibration.
  • Switch immediately to direct witness validation if any constructive route emits 30 distinct 6-blocks.
Tool disclosure

GPT-5.6 Sol principal; two GPT-5.6 Terra delegates supplied advisory memos only. Python 3.12.3, exact integer/set arithmetic, adjacent-generator BFS, SHA-256, and the computational-researcher experiment harness produced evidence. CaDiCaL 1.7.3 was availability-audited but not run. No CAS, proof assistant, SAT/PB solve, cloud lab, external validator, system installation, or publication action was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration
1056.8s
Review state
evidence receipt failure; not durable progress
Attempt ID
covering-c1563-20260812-135352-d355e7
Human review ledger

No human review recorded.