Compiled and independently audited the smallest r=0 exact-degree pseudo-Boolean calibration, then tested availability of a proof-producing RoundingSat→VeriPB→CakePB chain.

proof-producing incidence/PB cube decomposition

Native exact-cardinality constraints plus independently replayable PB proofs

Hypothesis: A pinned RoundingSat, VeriPB, and CakePB chain can emit and independently replay the smallest r=0 exact-degree contradiction within five seconds, one GiB, and one MiB of proof.

Test: Compile the 450-variable r=0 overdegree OPB, require all three pinned executables, and accept only an emitted proof replayed by VeriPB and elaborated CakePB with mutation rejection.

A covering contribution requires a directly checked 30-cover or a complete independently replayed exclusion. This epoch produced neither; its only validated result is the local calibration semantics and precise tooling blocker.

• The retained 450-variable, 87-row calibration OPB is inconsistent because point 0 has thirteen forced incidences and exact degree twelve.
• Deleting the constraint x0_13=1 admits an explicitly constructed incidence matrix with all 30 column sizes equal to six and all 15 point degrees equal to twelve.
• At execution time no project-scoped RoundingSat, VeriPB, or CakePB executable was available, and both official GitLab source probes failed DNS resolution.
• The maintained covering range remains 30 <= C(15,6,3) <= 31.

• python3 scripts/pb_r0_toolchain_gate_v1.py --out-dir artifacts/epoch81-20260811/pb-r0-toolchain-gate-v1
• python3 checkers/check_pb_r0_toolchain_gate_v1.py --gate artifacts/epoch81-20260811/pb-r0-toolchain-gate-v1/toolchain-gate.json --out artifacts/epoch81-20260811/pb-r0-toolchain-gate-v1/independent-check.json
• python3 checkers/test_pb_r0_toolchain_gate_fail_closed_v1.py --gate artifacts/epoch81-20260811/pb-r0-toolchain-gate-v1/toolchain-gate.json --out artifacts/epoch81-20260811/pb-r0-toolchain-gate-v1/fail-closed-controls.json
• Independent-check rerun was byte-identical with SHA-256 a8b927b010cd10edc39007bbe1e29d80394af40bd21417338504dfb3d49b48c0.

• .proof-experiments/20260811-085530-fc214d: generated the exact OPB and returned BLOCKED because all PB executables were absent
• .proof-experiments/20260811-085537-1a7c48: reconstructed all rows and produced the one-unit-deletion SAT witness
• .proof-experiments/20260811-085623-71b1dc: rejected five refreshed-hash semantic/status mutations

checkers/check_pb_r0_toolchain_gate_v1.py independently parses and reconstructs the OPB, proves the local arithmetic contradiction, constructs a satisfying boundary witness by a distinct max-flow encoding, and refuses promotion without all PB replay flags.

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 deliberately contradictory r=0 OPB has no Boolean solution.
  Independent reconstruction shows thirteen forced point-0 variables against an exact sum of twelve. · Only artifacts/epoch81-20260811/pb-r0-toolchain-gate-v1/r0-overdegree-calibration.opb · proved
• Removing forced membership x0_13=1 makes the incidence-only calibration satisfiable.
  The independent checker records a 30-column witness with every column size six and every point degree twelve. · The one-constraint deletion mutation; no triple-covering requirements · computed

• Scale the PB decomposition with the current project toolchain.
  Current workspace and epoch environment · No pinned emitter, VeriPB checker, or CakePB replay kernel is available. · toolchain-gate.json plus two DNS-failed official source probes · Pre-acquired official, full-commit, archive-hashed source snapshots and a successful intact/mutation replay calibration
• Treat the retained PBP template as a proof.
  Epoch-81 calibration · It was neither emitted by a solver nor accepted by VeriPB or CakePB. · proof_emitted=false, veripb_replayed=false, cakepb_replayed=false · Replace it with a genuine emitted proof passing both replay paths

• Constructive C3-invariant quotient search
  A witness would settle the target and the proposed quotient is small enough for a bounded independently audited CNF discriminator. · Reconstruct block/triple orbits and weighted degree equations independently, then run a 60-second CaDiCaL witness search only if every coefficient audit passes. · high · open
• Canonical root-link ownership catalogue
  It is a materially different global exclusion route with a potential completeness frontier. · Run dual canonical enumerators under a 10,000-orbit or 30-minute lab cap and compare ownership/frontier hashes. · normal · open
• Pinned native-PB certificate pipeline
  Native equalities remain potentially more compact than totalizer CNF, but replay is mandatory. · Provision official snapshots, build twice with distinct optimization settings, and replay the retained calibration plus all mutations. · low · open

Objective: Test the cheapest constructive symmetry-family route without confusing a local negative result with a global exclusion.

First action: Independently reconstruct the C3 action (012)(345)(678)(9 10 11)(12 13 14), its block/triple orbits, weighted cardinality, and all point-degree coefficients.

Stop condition: Stop on any orbit/weight mismatch, direct 30-cover witness, or bounded solver UNKNOWN/UNSAT; only a directly checked witness promotes.

• Do not rerun PB until full-commit, archive-hashed official RoundingSat, VeriPB 3.0.2, and matching CakePB sources are pre-acquired.
• Independently reconstruct the proposed C3 orbit action and weighted incidence equations; reject it immediately if the reported orbit counts or fixed-point coefficients fail.
• If the C3 audit passes, compile one bounded CaDiCaL constructive search and directly check any witness against all 455 triples; treat UNSAT as local to the symmetry family.
• If that route fails its audit or bounded search, begin the canonical root-link ownership-completeness frontier.

• https://www.coveringrepository.com/systems.aspx?k=6&t=3&m=-1 ↗
• https://ljcr.dmgordon.org/cover/show_cover.php?v=15&k=6&t=3 ↗
• https://veripb.org/ ↗
• https://gitlab.com/MIAOresearch/software/VeriPB/-/releases ↗
• https://gitlab.com/MIAOresearch/software/VeriPB/-/blob/HEAD/proof_format_overview.md ↗
• https://gitlab.com/MIAOresearch/software/roundingsat/-/tags ↗

GPT-5.6 Sol was principal investigator. Two GPT-5.6 Terra delegates supplied advisory prior-art and verification memos; Sol reimplemented and audited every relied-on check, and model agreement was not validation. CPython 3.12.3 generated and parsed OPB, implemented deterministic max flow, and ran mutation controls. Git performed bounded official-source probes. The computational-researcher harness recorded commands, hashes, limits, platform, and memory. Web search checked the maintained covering range and official VeriPB/RoundingSat sources. No PB solver/checker, CakePB kernel, CAS, proof assistant, cloud lab, external proof service, or human validator produced terminal evidence.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

848.2s

Review state

not a result claim

Attempt ID

covering-c1563-20260811-090051-e54072

No human review recorded.