Recompiled one immutable type-4 joint skeleton/profile/coverage leaf as a fully bi-implicational BDD-CNF and ran one proof-producing bounded solve.

joint labelled pair-excess skeleton with proof-producing BDD compilation

Represent each exact pair or retained profile row by a private saturated-count BDD, independently reconstruct every clause, then run CaDiCaL with LRAT enabled.

Hypothesis: The proof-producing BDD-CNF for the immutable joint leaf returns checked SAT or replay-certified LRAT-UNSAT within 60 seconds and 512 MiB.

Test: Generate the exact CNF below 2,000,000 clauses, independently reconstruct it, pass mutation and proof-stack controls, then run CaDiCaL 1.7.3 for 60 seconds with seed 0 and LRAT enabled.

The formula and verification pipeline are independently checkable, but UNKNOWN and a partial LRAT trace have no mathematical force. The exact value therefore remains open.

• The recorded 127-row BDD-CNF is satisfiability-equivalent to the original 148-row semantics for this one leaf.
• CaDiCaL 1.7.3 returned UNKNOWN on that formula at seed 0 after the predeclared 60-second run.
• No claim about feasibility of the leaf or the value of C(15,5,3) follows.

• python3 scripts/type4_joint_bdd_cnf_v1.py generated CNF SHA-256 517f915ccf45cf4ef9e1e55981491d9d96e702b569bb23a6a193b1677b517320
• python3 checkers/check_type4_joint_bdd_cnf_v1.py returned PASS after exact reconstruction and five mutation rejections
• /usr/bin/cadical --seed=0 --lrat=true --binary=false -t 60 artifacts/type4-joint-bdd-cnf-20260809/leaf.cnf artifacts/type4-joint-bdd-cnf-20260809/leaf.lrat returned UNKNOWN
• python3 scripts/proof_stack_c532_control_v1.py verified direct LRAT and rejected the proof against a weaker formula

• .proof-experiments/20260809-235033-591c2b — deterministic CNF build produced 1,028,222 clauses
• .proof-experiments/20260809-235045-5f4a0a — checker stopped on a checker-only NameError before the synthetic control and supplied no evidence
• .proof-experiments/20260809-235126-a34f86 — corrected independent checker passed from scratch
• .proof-experiments/20260809-235159-7a4755 — LRAT smoke and wrong-formula controls passed
• .proof-experiments/20260809-235215-1a8857 — live solver returned UNKNOWN after 60.13 seconds
• .proof-experiments/20260809-235442-8eab40 — fail-closed summary confirmed UNKNOWN and rejected the partial trace as a certificate

checkers/check_type4_joint_bdd_cnf_v1.py independently reconstructs the primary universe, semantic rows, BDD state numbering, every DIMACS clause, row discharges, small-width truth tables, a synthetic 49-block control, and five mutations without importing the producer.

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

• Decision-diagram cardinality encoding -> predicted that a compact proof-producing representation would decide the saved PB leaf within 60 seconds -> the exact CNF remained UNKNOWN, so this transfer failed its discriminator.

• The 127 semantic rows are equivalent to the original 148 semantic rows on this one leaf.
  Algebraic discharge plus exact independent reconstruction in artifacts/type4-joint-bdd-cnf-20260809/independent-check.json · The hash-bound canonical type-4 joint leaf only · proved
• The generated CNF has 2,717 primaries, 257,641 auxiliaries, and 1,028,222 clauses.
  Independent byte reconstruction and CNF SHA-256 517f915ccf45cf4ef9e1e55981491d9d96e702b569bb23a6a193b1677b517320 · The generated leaf.cnf · computed
• The bounded CaDiCaL run returned UNKNOWN after 225,028 conflicts.
  .proof-experiments/20260809-235215-1a8857/experiment.json and stdout.txt · CaDiCaL 1.7.3, seed 0, LRAT enabled, 60-second cap, 512 MiB · computed

• Scale or rerun the same row-local BDD-CNF on this leaf solely by increasing its time cap.
  CNF SHA-256 517f915ccf45cf4ef9e1e55981491d9d96e702b569bb23a6a193b1677b517320 with CaDiCaL 1.7.3, seed 0, LRAT enabled · It reached the predeclared UNKNOWN redirect condition and produced a 415,587,721-byte incomplete proof stream. · artifacts/type4-joint-bdd-cnf-20260809/result.json · A materially different exact encoding with a new bounded discriminator or a checked candidate assignment

• Multi-basin exact-degree constructive repair
  A positive result directly supplies the globally accepted 54-block certificate, while the prior radius-five exhaustion covered only one Iorio basin. · Run deterministic degree-preserving repair from three hash-distinct basins with direct 455-triple checking and a defect-below-10 gate. · high · open
• Global pair-excess cube certificate search
  It remains globally decisive but needs a materially better encoding or decomposition before more proof compute. · Design one complete cube partition with an independently checked union and test one leaf using a different exact encoding. · normal · open
• C3 normalizer refinement
  The restricted family is compact and exactly defined, but prior C3 formulas were UNKNOWN and cannot settle the unrestricted problem. · Reopen only after an independently audited normalizer quotient predicts at least a 20% matched-cap improvement. · low · open

Objective: Determine whether structurally distinct degree-18 constructive basins can improve on the verified defect-10 neighborhood minimum or produce a 54-cover.

First action: Write a hash-bound three-basin protocol defining seed diversity, degree-preserving moves, incremental defect evaluation, direct checking, fixed seeds, and equal per-basin limits.

Stop condition: Stop on a directly checked 54-cover; otherwise redirect after three basins fail to beat verified defect 10 or collapse to the already exhausted Iorio neighborhood.

• Define three independently sourced or generated degree-18 basins and hash-bind their seeds.
• Implement incremental uncovered-triple deltas with degree-preserving moves and a separate direct checker.
• Run one fixed-seed bounded tranche per basin and stop unless a checked cover is found or the verified minimum defect improves below 10.
• Do not increase the cap or rerun this exact BDD-CNF/CaDiCaL configuration.

• 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 ↗

GPT-5.6 Sol principal audited the route, proved the row discharges, implemented and interpreted the experiments, and wrote the checkpoint. GPT-5.6 Terra delegates supplied advisory challenger and verification memos only; their agreement was not validation. Python 3.12.3 generated and independently reconstructed the CNF; CaDiCaL 1.7.3 ran the live search; pinned drat-trim and lrat-check validated only the smoke control; SHA-256 and the project run_experiment harness bound artifacts. No lab job, package installation, system change, external write, or publication occurred.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1055.8s

Review state

not a result claim

Attempt ID

covering-c1553-20260809-235922-ec82c8

No human review recorded.