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

Fail-closed bounded acquisition audit for the retained CaDiCaL-to-VeriPB/CakePB calibration before any C(15,6,3) target cube

No Progress

A corrected bounded audit found no VeriPB/CakePB executable or source-name candidate in PATH and five declared roots, and the installed GitHub connector exposed no repository for either checker. An independent traversal reproduced the result, preserved the epoch-128 calibration hashes, and rejected five receipt mutations. No target formula or cube ran; 30 <= C(15,6,3) <= 31 is unchanged.

Research-policy redirect

Evidence receipt creation failed; durable progress is withheld.

Strategy and discriminator

proof-producing incidence/PB cube decomposition

Search PATH, five declared project-scoped roots, and connector-visible GitHub repositories for hashable VeriPB/CakePB executables or source-name candidates; authorize only synthetic replay on a positive result.

Hypothesis: A pinned VeriPB or CakePB executable/source-name candidate, or an official mirror visible to the installed GitHub connector, is available through the declared project-scoped channels.

Test: Case-insensitive bounded filesystem scan plus two repository queries, independently reconstructed before replaying the 129-byte retained calibration.

Rationale

The missing external replayers prevent the retained PBP emitter from satisfying the verification contract. Because the scan is environment-bounded, it blocks this route without making any public-source or mathematical nonexistence claim.

Claims requiring scrutiny
  • Within PATH, workspace/tools, /root/proof-factory, /root/.cache, /opt, and /usr/local at the recorded run, there was no executable or case-insensitive source-name candidate matching VeriPB, CakePB, or cake_pb.
  • The two installed GitHub connector repository searches returned zero visible repositories; this does not establish public absence because the official projects are on GitLab.
  • No C(15,6,3) target cube was authorized or executed, so the maintained range remains 30 <= C(15,6,3) <= 31.
Evidence and scope
  • python3 scripts/audit_pbp_replayer_acquisition_v2.py --out artifacts/epoch129-20260812/pbp-replayer-acquisition-gate-v2/receipt.json --connector-record sources/epoch129-pbp-github-mirror-probe.json
  • python3 checkers/check_pbp_replayer_acquisition_v2.py --receipt artifacts/epoch129-20260812/pbp-replayer-acquisition-gate-v2/receipt.json --out artifacts/epoch129-20260812/pbp-replayer-acquisition-gate-v2/independent-check.json
  • python3 checkers/test_pbp_replayer_acquisition_fail_closed_v2.py --receipt artifacts/epoch129-20260812/pbp-replayer-acquisition-gate-v2/receipt.json --out artifacts/epoch129-20260812/pbp-replayer-acquisition-gate-v2/fail-closed-controls.json
  • Experiments 20260812-201653-6c9372, 20260812-201659-2af9ca, and 20260812-202058-c47daf all returned 0.
Computational experiments
  • .proof-experiments/20260812-201653-6c9372: zero executable and source-name candidates; BLOCKED_NO_EXECUTABLE_OR_SOURCE
  • .proof-experiments/20260812-201659-2af9ca: independent rescan returned PASS_BLOCKED_GATE_RECONSTRUCTED
  • .proof-experiments/20260812-202058-c47daf: five receipt mutations were all rejected
Independent checker

checkers/check_pbp_replayer_acquisition_v2.py uses pathlib.rglob rather than the producer's os.walk, rechecks the connector record and retained calibration hashes, and fails unless all target authorization flags remain false. A separate mutation harness rejected five 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
  • GitHub repository connector -> prediction that an official or pinned mirror might bypass blocked GitLab acquisition -> zero visible repositories, so this acquisition transfer was discarded.
Established facts
  • The selected PBP route has no usable binary or source-name candidate in the declared local roots at the recorded epoch.
    V2 receipt SHA-256 812ce3621753997d66265ff236d5b21f83623bf3a3a30e48f2c092fc51a7b818 and independent PASS receipt. · PATH plus workspace/tools, /root/proof-factory, /root/.cache, /opt, and /usr/local on 2026-08-12. · computed
Ruled out in this epoch
  • Repeat PBP replayer acquisition in the unchanged environment.
    The same names, roots, connector visibility, and absent new inputs. · Both corrected and independent scans found zero candidates; repetition has no information value. · V2 receipt and independent check. · A new hash-pinned official VeriPB or CakePB source archive or executable path is supplied.
  • Use CakeLPR as CakePB.
    The retained VeriPB-format PBP calibration. · CakeLPR checks LPR/LRAT and is not a pseudo-Boolean proof checker. · tools/cake_lpr provenance and V2 negative-control classification. · Never under this name and proof format; use the actual pinned CakePB checker.
Open leads
  • Dual external replay of the immutable epoch-128 CaDiCaL calibration.
    It remains the cheapest decisive qualification test once both checker inputs exist. · Run pinned VeriPB and CakePB on the intact PBP, four proof mutations, and the satisfiable base mismatch; run no target cube. · high · open
  • Complete the parent-rich depth-four ownership union.
    It supplies the exhaustive outer frontier required by a global negative certificate and is materially different from another solver-throughput run. · After explicit human approval, materialize exactly 38,705 remaining profiles and independently reconcile all 62,437 profiles and deletion parents. · high · open
Continuation checkpoint

Objective: Unblock one globally certifiable route without repeating closed local or throughput experiments.

First action: Verify a supplied checker archive or binary against its official tag and hash; absent that input, request approval for exactly 38,705 parent-rich profiles before running submit_lab.py.

Stop condition: Stop on source/hash mismatch, any intact-replay failure or mutation acceptance, ownership/count mismatch, or absent explicit scope approval.

Next moves
  • Do not rerun this acquisition scan unless new hash-pinned checker inputs are supplied.
  • If official pinned VeriPB and CakePB inputs arrive, replay only the immutable epoch-128 two-clause calibration and require intact acceptance plus rejection of every declared mutation and mismatched base.
  • Otherwise obtain human approval for materializing exactly the remaining 38,705 parent-rich profiles and independently reconcile the full 62,437-profile union before compiling SAT leaves.
Tool disclosure

GPT-5.6 Sol was principal investigator. The supplied GPT-5.6 Terra challenger-prior-art and experiment-verification delegates provided advisory memos; Sol audited them and did not treat model agreement as validation. Deterministic work used CPython 3.12.3, pathlib/os filesystem traversals, SHA-256, the computational-researcher experiment harness, and the installed read-only GitHub connector. CaDiCaL 1.7.3 artifacts from epoch 128 were hash-checked but CaDiCaL was not run on a target. VeriPB and CakePB were not installed or run; CakeLPR was identified only as a negative control. No CAS, proof assistant, cloud lab, or external proof service produced evidence.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration
1031.7s
Review state
not a result claim
Attempt ID
covering-c1563-20260812-202321-9cce8c
Human review ledger

No human review recorded.