feat(cont): prove CONT-2 justifiable iff distance is window, square, or pronic

LeanSpec/Forks/Lstar/Slot.lean

@@ -16,8 +16,13 @@ uses the argument order `(finalized, target)`, adopted here. Python asserts
 subtraction truncates instead — callers guarantee the precondition, as
 upstream's assert documents.
 
-Supports the ST-* and CONT-2 propositions from
-`docs/lean4-proof-propositions.md` (no theorems in this file).
+Proves CONT-2 from `docs/lean4-proof-propositions.md`:
+  - CONT-2: `Slot.isJustifiableAfter finalized target` holds iff the slot
+    distance is at most 5, a perfect square, or a pronic number
+    (`justifiable_iff`), via correctness of the hand-rolled `isqrt`.
+
+Also supports the ST-* propositions (the executable judgments are consumed
+by `process_attestations`).
 -/
 
 import LeanSpec.Aliases
@@ -61,4 +66,139 @@ def justifiedIndexAfter (finalized target : Slot) : Option Nat :=
   if target ≤ finalized then none
   else some (target.toNat - finalized.toNat - 1)
 
+/-! ## CONT-2: characterization of justifiability -/
+
+/-- Expand `(k + 1)²` so `omega` can reason with `k * k` as an atom. -/
+private theorem sq_succ (k : Nat) : (k + 1) * (k + 1) = k * k + 2 * k + 1 := by
+  rw [Nat.mul_succ, Nat.succ_mul]
+  omega
+
+/-- Expand an odd square: `(2m + 1)² = 4m² + 4m + 1`. -/
+private theorem odd_sq (m : Nat) :
+    (2 * m + 1) * (2 * m + 1) = 4 * (m * m) + 4 * m + 1 := by
+  rw [sq_succ (2 * m), Nat.mul_mul_mul_comm]
+  omega
+
+/-- `isqrt` lower bound: its square never exceeds the input. -/
+theorem isqrt_le (n : Nat) : isqrt n * isqrt n ≤ n := by
+  induction n using isqrt.induct with
+  | case1 n h =>
+    rw [isqrt, if_pos h]
+    have h01 : n = 0 ∨ n = 1 := by omega
+    cases h01 with
+    | inl h0 => subst h0; exact Nat.le_refl _
+    | inr h1 => subst h1; exact Nat.le_refl _
+  | case2 n h small large hlarge ih =>
+    rw [isqrt, if_neg h]
+    dsimp only
+    split
+    · next h2 => exact h2
+    · next h2 => exact absurd hlarge h2
+  | case3 n h small large hnlarge ih =>
+    rw [isqrt, if_neg h]
+    dsimp only
+    split
+    · next h2 => exact absurd h2 hnlarge
+    · next h2 =>
+      have hexp : (2 * isqrt (n / 4)) * (2 * isqrt (n / 4))
+          = 4 * (isqrt (n / 4) * isqrt (n / 4)) := by
+        rw [Nat.mul_mul_mul_comm]
+      omega
+
+/-- `isqrt` upper bound: the next square is strictly above the input. -/
+theorem isqrt_lt_succ (n : Nat) : n < (isqrt n + 1) * (isqrt n + 1) := by
+  induction n using isqrt.induct with
+  | case1 n h =>
+    rw [isqrt, if_pos h]
+    rw [sq_succ]
+    omega
+  | case2 n h small large hlarge ih =>
+    rw [isqrt, if_neg h]
+    dsimp only
+    split
+    · rw [show 2 * isqrt (n / 4) + 1 + 1 = 2 * (isqrt (n / 4) + 1) from by omega,
+          Nat.mul_mul_mul_comm]
+      omega
+    · next h2 => exact absurd hlarge h2
+  | case3 n h small large hnlarge ih =>
+    rw [isqrt, if_neg h]
+    dsimp only
+    split
+    · next h2 => exact absurd h2 hnlarge
+    · next h2 => exact Nat.lt_of_not_le h2
+
+/-- `isqrt` is the unique value between the bracketing squares. -/
+theorem isqrt_eq (k n : Nat) (h1 : k * k ≤ n) (h2 : n < (k + 1) * (k + 1)) :
+    isqrt n = k := by
+  have hle := isqrt_le n
+  have hlt := isqrt_lt_succ n
+  have h3 : ¬ isqrt n < k := fun hc => by
+    have hstep : (isqrt n + 1) * (isqrt n + 1) ≤ k * k :=
+      Nat.mul_le_mul (Nat.succ_le_of_lt hc) (Nat.succ_le_of_lt hc)
+    omega
+  have h4 : ¬ k < isqrt n := fun hc => by
+    have hstep : (k + 1) * (k + 1) ≤ isqrt n * isqrt n :=
+      Nat.mul_le_mul (Nat.succ_le_of_lt hc) (Nat.succ_le_of_lt hc)
+    omega
+  omega
+
+/-- The pronic discriminant identity: `4k(k+1) + 1 = (2k+1)²`. -/
+private theorem pronic_disc (k : Nat) :
+    4 * (k * (k + 1)) + 1 = (2 * k + 1) * (2 * k + 1) := by
+  rw [Nat.mul_succ, odd_sq]
+  omega
+
+/-- The three-form characterization of `justifiableDelta`: the distance is
+within the immediate window, a perfect square, or a pronic number. -/
+theorem justifiableDelta_iff (δ : Nat) :
+    justifiableDelta δ = true ↔
+      δ ≤ 5 ∨ (∃ k, δ = k * k) ∨ (∃ k, δ = k * (k + 1)) := by
+  unfold justifiableDelta immediateJustificationWindow
+  simp only [Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq, beq_iff_eq]
+  constructor
+  · intro h
+    match h with
+    | .inl (.inl h5) => exact .inl h5
+    | .inl (.inr hsq) => exact .inr (.inl ⟨isqrt δ, hsq.symm⟩)
+    | .inr ⟨hsq, hodd⟩ =>
+      refine .inr (.inr ?_)
+      have hm : isqrt (4 * δ + 1) = 2 * (isqrt (4 * δ + 1) / 2) + 1 := by
+        omega
+      refine ⟨isqrt (4 * δ + 1) / 2, ?_⟩
+      rw [hm, odd_sq] at hsq
+      rw [Nat.mul_succ]
+      omega
+  · intro h
+    match h with
+    | .inl h5 => exact .inl (.inl h5)
+    | .inr (.inl ⟨k, hk⟩) =>
+      refine .inl (.inr ?_)
+      subst hk
+      rw [isqrt_eq k (k * k) (Nat.le_refl _) (by rw [sq_succ k]; omega)]
+    | .inr (.inr ⟨k, hk⟩) =>
+      refine .inr ?_
+      subst hk
+      have hr : isqrt (4 * (k * (k + 1)) + 1) = 2 * k + 1 := by
+        rw [pronic_disc]
+        exact isqrt_eq (2 * k + 1) _ (Nat.le_refl _) (by
+          rw [odd_sq, show 2 * k + 1 + 1 = 2 * (k + 1) from by omega,
+              Nat.mul_mul_mul_comm, sq_succ k]
+          omega)
+      constructor
+      · rw [hr]
+        exact (pronic_disc k).symm
+      · rw [hr]
+        omega
+
+/-- CONT-2: `is_justifiable_after` holds iff the slot distance from the
+finalized slot is at most 5, a perfect square, or a pronic number. The
+`finalized ≤ target` hypothesis mirrors upstream's assert; the
+characterization itself holds for the truncated distance regardless. -/
+theorem justifiable_iff
+    (finalized target : Slot) (_h : finalized ≤ target) :
+    isJustifiableAfter finalized target ↔
+      (let δ := target.toNat - finalized.toNat
+       δ ≤ 5 ∨ (∃ k, δ = k * k) ∨ (∃ k, δ = k * (k + 1))) :=
+  justifiableDelta_iff (target.toNat - finalized.toNat)
+
 end LeanSpec.Slot

docs/lean4-proof-propositions.md

@@ -1,6 +1,6 @@
 ---
 title: leanSpec → Lean4 Theorem Proving Proposition Catalog
-last_updated: 2026-07-02
+last_updated: 2026-07-03
 tags:
   - lean4
   - formal-verification
@@ -69,14 +69,14 @@ Format: `<DOMAIN>-<number>`. `DOMAIN` is the abbreviation of the owning area:
 | Domain | Proved | Open | Axiom | Total |
 |---|---:|---:|---:|---:|
 | SSZ | 6 | 0 | 1 | 7 |
-| CONT | 0 | 2 | 0 | 2 |
+| CONT | 1 | 1 | 0 | 2 |
 | ST | 6 | 0 | 0 | 6 |
 | FC | 0 | 5 | 0 | 5 |
 | VAL | 0 | 5 | 0 | 5 |
 | NET | 0 | 2 | 0 | 2 |
 | STOR | 0 | 2 | 0 | 2 |
 | SYNC | 0 | 2 | 0 | 2 |
-| **Total** | **12** | **18** | **1** | **31** |
+| **Total** | **13** | **17** | **1** | **31** |
 
 ## SSZ & primitive types
 
@@ -179,9 +179,10 @@ A **Container** is a composite SSZ type — a struct with named fields (analogou
         c1 < c2 ↔ c1.slot < c2.slot := by sorry
     ```
 
-- [ ] **CONT-2: justifiable holds iff the slot distance is one of three forms**
-  - Source: `is_justifiable_after`
+- [x] **CONT-2: justifiable holds iff the slot distance is one of three forms**
+  - Source: `is_justifiable_after` (`src/lean_spec/spec/forks/lstar/slot.py`)
   - Note: Decides whether the target slot is at a justifiable distance from the finalized-checkpoint slot (LMD-CASPER justification-candidate check).
+  - Proved at: `LeanSpec/Forks/Lstar/Slot.lean` (`Slot.justifiable_iff`, via correctness of the hand-rolled `isqrt`: `isqrt_le` / `isqrt_lt_succ` / `isqrt_eq`)
   - Sample code:
 
     ```lean
@@ -190,6 +191,7 @@ A **Container** is a composite SSZ type — a struct with named fields (analogou
         Slot.isJustifiableAfter finalized target ↔
           let δ := target.toNat - finalized.toNat
           δ ≤ 5 ∨ (∃ k, δ = k * k) ∨ (∃ k, δ = k * (k + 1)) := by sorry
+    -- ✅ proved in LeanSpec/Forks/Lstar/Slot.lean as `Slot.justifiable_iff`
     ```
 
 ## State Transition