Built and independently audited exact-cardinality C(5,3,2) OPB controls, then tested availability of the first required pinned proof-producing solver source.

proof-producing OPB leaf solving

A tuple-based producer emits exact-cardinality OPBs; an independent recursive-mask parser exhaustively evaluates every assignment, while a source preflight gates all real-leaf work.

Hypothesis: The exact-cardinality C(5,3,2) bounds 3, 4, and 5 controls have 11 written rows, 12 equality-expanded proof axioms, and respectively 0, 10, and 72 satisfying selections; pinned source acquisition either enables proof-stack calibration or triggers a fail-closed stop.

Test: Independently parse and exhaustively evaluate all 1024 assignments for each OPB, reject rebound-hash semantic mutations, require byte-identical regeneration, and probe the first required pinned RoundingSat source.

The independent checker and controls establish only the saved formulas and model counts. The failed source gate satisfies the predeclared stop condition, so no inference about a real leaf or the exact covering number is admissible.

• The saved exact-cardinality C(5,3,2) bounds 3, 4, and 5 formulas each contain 10 variables, 11 written constraints, and 12 equality-expanded axioms.
• Their complete satisfying-selection counts are respectively 0, 10, and 72.
• No C(15,5,3) profile or cube was excluded, and the exact range remains 54 <= C(15,5,3) <= 55.

• python3 checkers/check_opb_c532_calibration_v1.py --artifact-dir artifacts/opb-c532-calibration-20260809 --result-output artifacts/opb-c532-calibration-20260809/independent-check.json
• python3 checkers/test_opb_c532_calibration_mutations_v1.py --artifact-dir artifacts/opb-c532-calibration-20260809 --checker checkers/check_opb_c532_calibration_v1.py --result-output artifacts/opb-c532-calibration-20260809/mutation-controls-final.json
• python3 checkers/check_opb_c532_regeneration_v1.py --artifact-dir artifacts/opb-c532-calibration-20260809 --generator scripts/opb_c532_calibration_v1.py --result-output artifacts/opb-c532-calibration-20260809/regeneration-check.json
• sha256sum -c artifacts/opb-c532-calibration-20260809/manifest.sha256

• .proof-experiments/20260809-014610-76ee02: generated three OPBs and reported model counts 0/10/72.
• .proof-experiments/20260809-014610-13537f and 20260809-014709-f7d4c4: retained failed checker-development controls involving model ordering and a checker-only diagnostic; neither supports a formula claim.
• .proof-experiments/20260809-014742-3637c9: final independent checker accepted all three formulas.
• .proof-experiments/20260809-015440-65462d: all three rebound-hash semantic mutations were rejected.
• .proof-experiments/20260809-014953-d24c73: four canonical packet files regenerated byte-identically.
• .proof-experiments/20260809-015441-d9a358: expected failure; RoundingSat source preflight exited 2 after git reported unresolved gitlab.com.

checkers/check_opb_c532_calibration_v1.py reconstructs blocks and pairs recursively as masks, parses OPB text independently, and evaluates all 1024 assignments per formula rather than using the producer's fixed-cardinality tuple enumeration.

not_requested

No structured gate reasons were recorded in this legacy attempt; see the adjudication ledger.

Original model outcome

progress

Public classification

progress

• Certified PB workflow documentation -> exact equalities must count as two proof axioms -> the controls correctly distinguish 11 written rows from 12 loaded axioms.
• Fail-closed certificate campaigns -> source and revision availability must precede real search -> the first acquisition failure stopped all leaf work.

• The saved C(5,3,2) exact-cardinality controls have model counts 0, 10, and 72 at bounds 3, 4, and 5.
  artifacts/opb-c532-calibration-20260809/independent-check.json · All 1024 assignments for each saved formula. · computed
• The canonical OPB packet regenerates byte-identically.
  artifacts/opb-c532-calibration-20260809/regeneration-check.json · The three OPBs and manifest under the recorded Python generator. · computed

• Run the selected C(15,5,3) leaf with the current proof-producing OPB stack.
  Current environment and CP-2025 pinned-tool verification contract. · The first required RoundingSat source could not be resolved or acquired. · artifacts/opb-c532-calibration-20260809/source-preflight-final.json · Provide a hash-identified local bundle matching all required revisions and pass the saved proof/model controls.
• Treat offline formula validation as proof-producing toolchain validation.
  The C(5,3,2) calibration packet. · No RoundingSat proof, VeriPB replay, CakePB elaboration, or solver model was produced. · artifacts/opb-c532-calibration-20260809/independent-check.json · Complete bound-3 dual replay and direct bound-4 and bound-5 model checking.

• Literal outside-subset realization of one minimum-survivor root profile.
  It directly restores subset identities and compatibility information discarded by the exhausted aggregate relaxation. · Generate one deterministic instance and independently decode exact outside point degrees, pair degrees, and triple coverage. · high · open
• Complete proof-producing OPB calibration after pinned bundle provisioning.
  A successful dual-replay gate would make future negative leaf results admissible. · Run the saved bound-3/4/5 packet with exact CP-2025 revisions. · normal · open

Objective: Test literal outside-subset realizability for one minimum-survivor root profile.

First action: Identify the minimum-survivor stored profile, freeze its exact count vector, and emit one deterministic instance plus separate decoder.

Stop condition: Stop after one profile unless it eliminates a complete hash-bound family or supplies a directly checked realization.

• Select the minimum-survivor stored root profile and freeze its exact count vector.
• Emit one deterministic literal outside-subset realization instance and a materially different decoder.
• Reopen OPB calibration only when a hash-identified bundle matching the required RoundingSat, VeriPB, and CakePB revisions is locally available.

• 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://satcompetition.github.io/2025/downloads/checkers/veripb.pdf ↗
• https://drops.dagstuhl.de/storage/00lipics/lipics-vol340-cp2025/html/LIPIcs.CP.2025.21/LIPIcs.CP.2025.21.html ↗
• https://gitlab.com/MIAOresearch/software/roundingsat/-/tags ↗

GPT-5.6 Sol served as principal investigator. Supplied GPT-5.6 Terra challenger and verification memos were advisory design inputs and were not counted as validation. Deterministic computation used Python 3.12.3, Git source preflight, SHA-256, and the computational-researcher experiment harness. No SAT/PB solver, VeriPB, CakePB, CAS, proof assistant, cloud lab, or external solver service was run.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1072.3s

Review state

not a result claim

Attempt ID

covering-c1553-20260809-015713-6f2e0e

No human review recorded.