Construct and independently reconstruct the complete sparse OPB semantics of the certified partition-[15], root-mask-31 leaf, with hash-rebound target, variable, and orientation mutation controls.

proof-producing OPB leaf solving

A tuple-scanning generator emits canonical sparse OPB and incidence artifacts; a different recursive-mask checker scatters block incidences and compares every variable map, row, relation, target, and equality-expansion count.

Hypothesis: The selected exact-pair leaf has a deterministic 3002-variable sparse OPB representation with 550 written rows and 655 equality-expanded proof axioms that an independently implemented checker reconstructs exactly while rejecting target, variable-map, and orientation mutations.

Test: Generate the full leaf without a solver, compare every semantic field against a different incidence construction, then rebind each deliberate mutation's hash and require rejection at row comparison.

Agreement of materially different incidence constructions plus semantic mutation rejection establishes that the OPB artifact represents the intended selected leaf. With no solver result or certificate, this supports infrastructure progress only.

• The hash-bound selected-leaf OPB has 3002 variables and 550 written constraints representing 445 coverage inequalities and 105 exact pair equalities.
• Under the documented VeriPB convention, those rows load as 655 proof axioms.
• The independent checker reconstructs all 59390 incidence terms and rejects hash-rebound target, variable, and orientation mutations.
• No assignment, profile, or cube was eliminated; the range remains 54 <= C(15,5,3) <= 55.

• python3 checkers/check_opb_leaf_semantic_v1.py returned valid=true with all predeclared counts.
• python3 checkers/test_opb_leaf_mutations_v1.py rejected orientation and variable changes at row 1 and a target change at row 446 after hash rebinding.
• sha256sum -c artifacts/opb-leaf-semantic-audit-20260808/manifest.sha256 returned OK for every listed artifact.

• .proof-experiments/20260808-212337-da2ac9: generated the canonical incidence manifest and OPB in 1.155 seconds.
• .proof-experiments/20260808-212347-b48fa8: independent reconstruction accepted all exact counts in 0.293 seconds.
• .proof-experiments/20260808-212431-cfb002: three hash-rebound semantic mutations were rejected in 1.244 seconds.

check_opb_leaf_semantic_v1.py does not import the generator and replaces tuple scanning with recursive mask generation plus sparse incidence scattering; test_opb_leaf_mutations_v1.py exercises target, variable, and orientation failures after bypassing the provenance hash guard.

not_requested

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

Original model outcome

progress

Public classification

progress

• Certified pseudo-Boolean proof logging -> predicted that input equalities must appear in the proof formula-size contract -> observed 105 equalities raise the selected leaf from 550 written rows to 655 proof axioms.
• Adversarial software testing -> predicted that semantic mutations would identify checker coverage -> observed the initial hash-only rejection was insufficient, while hash-rebound controls reached and falsified exact row semantics.

• The canonical selected-leaf OPB contains 3002 variables, 445 coverage inequalities, 105 exact pair equalities, 550 written constraints, and 59390 incidence terms; the equalities expand the proof input to 655 axioms.
  Independent-check.json, canonical artifacts, and the primary VeriPB/CakePB documentation. · Partition [15], root mask 31, source manifest SHA-256 6d64b96e4017784262a995fabbed56ca2849f67cb9c86329666e4825c834ffa8. · computed

• Count only the 550 written OPB rows in a future VeriPB formula-size assertion.
  The selected OPB under the documented VeriPB equality convention. · Each of 105 equalities counts as two input inequalities, so the correct count is 445 + 2*105 = 655. · VeriPB/CakePB documentation and independent-check.json. · A different proof checker with a separately documented input-count convention.
• Treat a mutation rejected only by the OPB hash guard as evidence that row semantics are checked.
  Negative controls for this semantic checker. · The initial control did not reach row comparison; only the hash-rebound rerun exercised the target, variable, and relation checks. · mutation-controls.json records hash_rebound_before_check=true and row-specific failures. · Not applicable; retain the strengthened control.

• End-to-end proof-producing OPB calibration on tiny C(5,3,2) controls.
  It is the cheapest test of solver proof emission, VeriPB input binding, CakePB elaboration, and direct SAT-model checking before a selected-leaf run. · Build pinned project-scoped revisions and run bounds 3, 4, and 5 with fail-closed replay and model requirements. · high · open
• A stronger outside-triple structural refinement.
  A proved inequality could eliminate profiles or cubes without relying on solver proof production. · Derive one explicit outside-triple inequality and test it against all 20 stored root-flow witnesses. · normal · open

Objective: Establish a fail-closed project-scoped proof-producing OPB toolchain.

First action: Retrieve pinned CP 2025 RoundingSat, VeriPB, and CakePB revisions, record source/compiler/binary hashes, and generate the three C(5,3,2) controls.

Stop condition: Redirect before the selected leaf on any pin mismatch, unsupported or absent proof, VeriPB rejection, CakePB rejection, invalid SAT model, or timeout.

• Acquire pinned CP 2025 RoundingSat, VeriPB, and CakePB revisions in a project-scoped cache and record source and binary hashes.
• Generate deterministic C(5,3,2) bound-3, bound-4, and bound-5 controls; require VeriPB and CakePB replay for bound 3 and direct model checking for bounds 4 and 5.
• Only after all controls pass, run one short proof-producing solve on the exact selected leaf and treat any result as local to one of 2145 cubes.

• 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/entities/document/10.4230/LIPIcs.CP.2025.21 ↗

OpenAI Codex/GPT-5 acted as the Sol principal. Two GPT-5.6 Terra delegates supplied advisory reconnaissance only; their claims were independently audited and promoted into main-workspace artifacts with provenance. Python 3.12.3 and run_experiment.py generated and checked exact artifacts. Web search rechecked status and proof-format documentation. No SAT/PB solver, CAS, proof assistant, or new subagent was run in this epoch.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

958.0s

Review state

not a result claim

Attempt ID

covering-c1553-20260808-213153-c28ac5

No human review recorded.