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

Assemble the validated 91-class degree-18 defect-10 local corpus, compute nine fixed count-only signatures, select one predictor on 16 saved classes, and test it on a disjoint 24-class exact-mobility holdout.

No Progress

An exact, independently checked 91-class local corpus was produced and its predeclared count-only mobility predictor was falsified. The covering range remains 54 <= C(15,5,3) <= 55.

Research-policy redirect

Evidence receipt creation failed; durable progress is withheld.

Strategy and discriminator

defect-plateau structural-signature census

Point-isomorphism quotienting and a frozen train/holdout test determine whether cheap unlabeled structure predicts defect-preserving 2-for-2 mobility.

Hypothesis: One of nine predeclared structural counts, selected only on 16 saved classes, has the same correlation sign and absolute Spearman correlation at least 0.35 with exact defect-preserving 2-for-2 mobility on the disjoint 24-class holdout.

Test: Stream both complete move ledgers, select the maximum-absolute-correlation nonconstant feature on the training classes using a fixed tie rule, and evaluate only that feature on the held-out classes.

Rationale

Frozen source hashes, a pre-response protocol, complete local ledgers, an independent reconstruction, and fail-closed mutations support the local negative result. Its limited scope supports closing this route but no global exclusion.

Claims requiring scrutiny
  • The frozen source union has exactly 91 distinct upstream point-isomorphism signatures represented by checked degree-18 defect-10 families.
  • The response ledgers contain 115 training and 142 held-out defect-10 move occurrences among 1,564,129 legal rows.
  • Point-signature diversity has training Spearman -0.3706698379628954 and held-out Spearman -0.23066052349487706.
  • The predeclared absolute held-out gate 0.35 failed.
  • No 54-block cover or global branch exclusion was obtained.
Evidence and scope
  • python3 scripts/degree18_defect10_signature_census_v1.py --protocol protocols/degree18-defect10-signature-census-v1.json --output-dir artifacts/degree18-defect10-signature-census-20260812-corrected
  • python3 checkers/check_degree18_defect10_signature_census_v1.py --protocol protocols/degree18-defect10-signature-census-v1.json --artifact-dir artifacts/degree18-defect10-signature-census-20260812-corrected --output /tmp/check.json
  • python3 scripts/test_degree18_defect10_signature_census_mutations_v1.py --checker checkers/check_degree18_defect10_signature_census_v1.py --protocol protocols/degree18-defect10-signature-census-v1.json --artifact-dir artifacts/degree18-defect10-signature-census-20260812-corrected --output /tmp/mutations.json
  • sha256sum -c artifacts/degree18-defect10-signature-census-20260812-corrected/manifest.sha256
Computational experiments
  • .proof-experiments/20260812-072758-20b375: rejected audit control; zero-degree points were omitted from one audit-only histogram
  • .proof-experiments/20260812-072842-a4c5da: corrected producer; held-out gate failed at -0.23066052349487706
  • .proof-experiments/20260812-073018-838abc: independent checker passed
  • .proof-experiments/20260812-073017-51abb3: all six mutations were rejected
Independent checker

checkers/check_degree18_defect10_signature_census_v1.py is a separate implementation that reconstructs source selection, hashes, degrees, defect, all nine features, both complete response ledgers, correlations, and the gate decision.

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
  • Local-search landscape analysis -> cheap signatures should predict mobility -> the sign transferred but magnitude failed the frozen holdout gate.
  • Certified covering campaigns -> slack-zero rigidity should feed complete symmetry branches and proof replay -> retained as a next-route requirement, not established this epoch.
Established facts
  • The joined corpus has 91 representatives with 91 distinct upstream point-isomorphism signatures.
    independent-check-v2.json: passed=true and representatives_checked=91 · The frozen source union only · computed
  • Every representative has 54 distinct blocks, point degree 18, and defect 10.
    Independent reconstruction of all 91 families · The selected representatives · computed
  • Point-signature diversity's held-out Spearman correlation is -0.23066052349487706.
    independent-check-v2.json after complete response rescan · The 24 held-out classes · computed
Ruled out in this epoch
  • Use the current nine-feature count-only screen to prioritize the 51 unexpanded classes.
    Selection on 16 classes and validation on the disjoint 24-class frontier · Absolute held-out Spearman 0.23066052349487706 was below 0.35. · result.json and independent-check-v2.json · A theorem-derived or independently motivated labelled feature plus a fresh frozen holdout
  • Rerun the complete fixed-pair link as a new discriminator.
    All 395 signatures and 754 existing targets · The existing independently checked gate retained every target and has zero new semantic delta. · artifacts/type4-complete-pair-link-gate-20260809/independent-check.json · Genuinely new labelled information beyond the complete fixed-pair link
Open leads
  • Four-type native-PB pair-upper matched gate
    An existing 5,000-conflict pilot showed a large auxiliary-free resource reduction and the route covers the global four-type normalization. · After approval, run four types times two encodings times two seeds and audit formulas and telemetry. · high · open
  • Literal outside-subset realization
    Restores labelled subset identities absent from failed aggregate routes. · Run one saved root-orbit-107 control if native-PB regresses. · normal · open
  • Proof-producing pseudo-Boolean encoding
    Would align the useful pair rows with the negative certificate contract. · Compile one canonical type to pinned OPB and require semantic reconstruction plus proof smoke. · normal · open
Continuation checkpoint

Objective: Obtain exact-scope approval for the four-type, two-seed native-PB pair-upper gate.

First action: Approve or revise the fixed matrix: types 1-4, base/upper, seeds 0/1553, Z3 4.13.0, 25,000 conflicts, 1 GB, fresh sequential processes.

Stop condition: Do not dispatch without approval; afterward redirect on validation mismatch, per-type regression, mutation survival, skipped run, or failure of the every-pair telemetry gate.

Next moves
  • Obtain human approval for the exact 16-run successor protocol before dispatching compute.
  • If approved, run types 1-4 times base/upper times seeds 0/1553 using Z3 4.13.0, 25,000 conflicts, 1 GB, and fresh sequential processes.
  • Accept a mathematical advance only for a directly checked cover or an independently replayed proof.
  • Redirect on any per-type regression, skipped run, version drift, hash mismatch, or failed mutation.
Tool disclosure

GPT-5.6 Sol was principal investigator and designed, implemented, executed, audited, and interpreted the epoch. Two injected GPT-5.6 Terra delegates supplied advisory reconnaissance only; Sol independently audited their claims and did not count model agreement as validation. Python 3.12.3 standard-library programs performed exact enumeration, SHA-256 hashing, tied-rank Spearman calculations, independent reconstruction, and mutation tests. Web search checked status and prior art. No subagents, CAS, SAT solve, proof assistant, cloud lab, package installation, external write, publication, or system change was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration
1382.3s
Review state
evidence receipt failure; not durable progress
Attempt ID
covering-c1553-20260812-074018-83add0
Human review ledger

No human review recorded.