Transferred the proof-preserving point-degree-cap encoding to canonical multiplicity-five-pair type 2 and compared it with the hash-locked exact-degree CNF.

canonical-pair-branch point-cap compression

Replace fifteen exact residual-degree totalizers by theorem-equivalent forward-only upper caps while preserving all 407 coverage clauses and the 2717-primary type-2 quotient.

Hypothesis: The type-2 cap replacement reduces CaDiCaL seed-0 decisions by at least 20 percent at a matched 25000-conflict limit.

Test: Independently reconstruct and proof-smoke validate the candidate, then compare fresh baseline and candidate CaDiCaL 1.7.3 runs using seed 0 and a 25000-conflict limit.

All semantic and proof controls passed, making the matched telemetry trustworthy. The measured decision regression directly falsifies the predeclared advancement hypothesis, while LIMIT provides no mathematical exclusion.

• Canonical type-2 coverage plus residual caps (13,13,16,16,17x11) is equivalent to coverage plus exact residual degrees.
• The candidate has exactly 71662 variables and 410049 clauses.
• At matched seed-0 limits, decisions regressed by 57.558385%, propagations decreased by 32.264337%, and process time decreased by 47.002398%.
• No cover or UNSAT result was obtained.

• python3 checkers/check_type2_link_cap_cnf_v1.py --cnf artifacts/type2-link-cap-cnf-20260810/candidate.cnf --manifest artifacts/type2-link-cap-cnf-20260810/candidate-manifest.json --output /tmp/check.json
• python3 checkers/check_type2_link_cap_result_v1.py --result artifacts/type2-link-cap-cnf-20260810/result.json --manifest artifacts/type2-link-cap-cnf-20260810/candidate-manifest.json --baseline-run .proof-experiments/20260810-092047-6aa1a9 --candidate-run .proof-experiments/20260810-092047-7ecc49 --output /tmp/result-check.json
• toolchains/drat-trim/lrat-check artifacts/type2-link-cap-cnf-20260810/proof-smoke.cnf artifacts/type2-link-cap-cnf-20260810/proof-smoke.lrat
• Result SHA-256 c95636e04d3bf432ee614916bee8165d8453b37fa3abdb36c5b282b246d15956
• Independent result-check SHA-256 e200157992a5fc63e54245ec3928f7cdc2924957ae37e60a275cf501669d6f57

• .proof-experiments/20260810-092047-6aa1a9: baseline reached LIMIT with 54423 decisions
• .proof-experiments/20260810-092047-7ecc49: candidate reached LIMIT with 85748 decisions
• artifacts/type2-link-cap-cnf-20260810: all semantic, mutation, totalizer, proof-smoke, and result checks passed

checkers/check_type2_link_cap_cnf_v1.py independently reconstructs the complete CNF using bit masks; checkers/check_type2_link_cap_result_v1.py independently parses raw receipts and recomputes every 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

• Globally rooted point-cap CNF -> predicted at least 20% fewer type-2 decisions -> observed 57.558385% more decisions, rejecting the transfer under protocol v1.

• Coverage forces every point degree to be at least 18.
  lambda_xy>=ceil(13/3)=5 and 4r_x=sum_{y!=x}lambda_xy>=70 · Every C(15,5,3) covering · proved
• Canonical type-2 residual caps are exact and imply 49 residual blocks.
  Fixed degrees are (5,5,2,2,1x11); the cap sum is 245. · Canonical multiplicity-five-pair type 2 · proved
• The candidate contains 71662 variables and 410049 clauses and is reconstructed clause-for-clause.
  artifacts/type2-link-cap-cnf-20260810/independent-check.json · type2-link-cap-cnf-v1 · computed
• The matched candidate run used 85748 decisions versus 54423 for the baseline.
  artifacts/type2-link-cap-cnf-20260810/result-independent-check.json · CaDiCaL 1.7.3, seed 0, 25000-conflict protocol · computed

• Advance the forward-only type-2 point-cap replacement under protocol v1.
  Matched CaDiCaL 1.7.3 seed-0 runs at 25000 conflicts · Decisions increased by 57.558385%, failing the required 20% reduction. · artifacts/type2-link-cap-cnf-20260810/result.json and result-independent-check.json · A materially different cardinality encoding, branching mechanism, or proof decomposition with a new matched protocol
• Treat LIMIT as evidence against canonical type 2.
  Both live runs · Neither run produced SAT, UNSAT, or a replayable proof. · Raw solver receipts · A directly checked SAT model or completely replayed UNSAT proof

• Symbolic pair-excess skeleton state DAG
  Could aggregate complete negative cubes without the previously measured 65765700-header explosion. · Count states for the simple 15-cycle skeleton with a 2^20-state stop gate and independent transition reconstruction. · high · open
• Proof-replayed layer-five local frontier
  Its 288-cell predecessor is certified, but the proposed successor is local and authorization-gated. · Run the specified 12-by-256 tranche only after explicit owner approval. · normal · open
• Coverage-aware constructive repair
  A successful result is terminal, but prior 2-for-2, 3-for-3, and length-4-through-7 searches remain at defect 10. · Test a materially new proof-core-weighted move generator and require an independently checked defect below 10. · low · open

Objective: Determine whether pair-excess skeleton constraints admit a compact, provably sufficient symbolic aggregation.

First action: Create a count-only simple-15-cycle state-DAG protocol with an independent transition checker and a 2^20-state stop threshold.

Stop condition: Stop if signature sufficiency cannot be proved, producer/checker counts disagree, or the state census exceeds 2^20.

• Do not increase this protocol's cutoff or merely repeat it on canonical types 1, 3, and 4.
• Predeclare a symbolic pair-excess state-DAG census for the simple 15-cycle skeleton.
• Independently reconstruct state transitions and stop above 2^20 states.
• Keep the 3072-cell layer-five tranche blocked until explicit owner approval.

• 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://arxiv.org/abs/2607.23766 ↗

GPT-5.6 Sol acted as principal investigator. GPT-5.6 Terra delegates supplied bounded advisory reconnaissance and verification design only; their agreement was not treated as validation. Python 3.12.3 generated and independently reconstructed CNFs. CaDiCaL 1.7.3 ran the matched searches and emitted DRAT. Pinned drat-trim verified and converted DRAT to LRAT; pinned lrat-check replayed LRAT and rejected the wrong-formula control. SHA-256 and the computational-researcher experiment harness bound artifacts. No sub-agent or lab job was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1025.3s

Review state

not a result claim

Attempt ID

covering-c1553-20260810-092912-6dbe43

No human review recorded.