Phase 2, decompress part 2b: THE SQUARE-ROOT WALK PROVEN

(sqrt_ratio_i_sq_spec, kernel-audited)

The largest single proof of the decompress chain: for square u/v
(witness x, v nonzero), the extracted sqrt_ratio_i returns choice 1 and
the even-parity root - Bnd r (2^52), r^2 * v = u, r's canonical residue
even. The walk composes every previously certified piece: the
square/mul/pow_p58 candidate chain, sqrt_m1_spec, fe_ct_eq_spec x3 (the
three constant-time residue checks), neg_spec, the Choice bitor, and
fe_cond_assign_spec twice (root flip by sqrt(-1), then sign
normalization via is_negative).

Case analysis: sqrt_core's disjunction (v*r^2 = +/-u) against the check
flags - u = 0 collapses everything to the zero root; u != 0 with
v*r^2 = u kills both flip flags (u = -u forces u = 0 in odd
characteristic; u = -u*i forces u*(1+i) = 0 with 1+i nonzero); with
v*r^2 = -u the flip fires and (i*r)^2 * v = -(-u) = u. Parity: the odd-
prime negation flip (ZMod.neg_val), zero-root edge included. New
helpers: eq_neg_self_iff_zero, one_add_i_ne_zero.

Certificate exact standard three; full button green fresh. Remaining:
from_bytes walk, decompress_of_canonical, replication, pass 4.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

verification/Proofs/DecompressSpec.lean

@@ -238,4 +238,272 @@ theorem sqrt_core (u v x : Fp) (hv : v ≠ 0) (hx : x ^ 2 * v = u) :
     · left; rw [hkey, h, mul_one]
     · right; rw [hkey, h]; ring
 
+/-- In 𝔽_p (p odd), an element equal to its own negative is zero. -/
+theorem eq_neg_self_iff_zero (a : Fp) : a = -a ↔ a = 0 := by
+  constructor
+  · intro h
+    have h2 : (2 : Fp) * a = 0 := by linear_combination h
+    rcases mul_eq_zero.mp h2 with h' | h'
+    · exact absurd h' two_ne_zero_Fp
+    · exact h'
+  · intro h; rw [h]; ring
+
+/-- 1 + √−1 does not vanish (else −1 = 1, contradicting p odd). -/
+theorem one_add_i_ne_zero {i : Fp} (hi : i * i = -1) : (1 : Fp) + i ≠ 0 := by
+  intro h
+  have him : i = -1 := by linear_combination h
+  rw [him] at hi
+  have : (2 : Fp) = 0 := by linear_combination hi
+  exact two_ne_zero_Fp this
+
+/-- **THE SQUARE-ROOT WALK** (success case): if u/v is a square (witness x,
+    v ≠ 0), `sqrt_ratio_i` returns choice 1 and the even-parity root:
+    r² · v = u with r's canonical residue even. -/
+theorem sqrt_ratio_i_sq_spec (u v : Fe) (hbu : Bnd u (2^54)) (hbv : Bnd v (2^54))
+    (hvne : ⟪v⟫ ≠ 0) (x : Fp) (hx : x ^ 2 * ⟪v⟫ = ⟪u⟫) :
+    field.FieldElement51.sqrt_ratio_i u v ⦃ cr =>
+      cr.1.val = 1 ∧ Bnd cr.2 (2^52) ∧
+      ⟪cr.2⟫ ^ 2 * ⟪v⟫ = ⟪u⟫ ∧ (⟪cr.2⟫).val % 2 = 0 ⦄ := by
+  haveI : NeZero P := ⟨by unfold P; norm_num⟩
+  unfold field.FieldElement51.sqrt_ratio_i
+  -- the arithmetic chain: v³, v⁷, u·v³, u·v⁷, (u·v⁷)^((p−5)/8), r, r², check
+  let* ⟨ fe, hbfe, hfe ⟩ ← square_spec' by bnd
+  let* ⟨ v3, hbv3, hv3 ⟩ ← mul_spec' by bnd
+  let* ⟨ fe1, hbfe1, hfe1 ⟩ ← square_spec' by bnd
+  let* ⟨ v7, hbv7, hv7 ⟩ ← mul_spec' by bnd
+  let* ⟨ fe2, hbfe2, hfe2 ⟩ ← mul_spec' by bnd
+  let* ⟨ fe3, hbfe3, hfe3 ⟩ ← mul_spec' by bnd
+  let* ⟨ fe4, hbfe4, hfe4 ⟩ ← pow_p58_spec by bnd
+  let* ⟨ r, hbr, hr ⟩ ← mul_spec' by bnd
+  let* ⟨ fe5, hbfe5, hfe5 ⟩ ← square_spec' by bnd
+  let* ⟨ check, hbcheck, hcheck ⟩ ← mul_spec' by bnd
+  -- √−1
+  step with sqrt_m1_spec as ⟨im, hbim, him⟩
+  -- the three constant-time checks
+  step with (fe_ct_eq_spec check u) as ⟨correct, hc01, hciff⟩
+  -- −u (needs u's limbs)
+  obtain ⟨u0, u1, u2, u3, u4, hul⟩ := Fe.exists_limbs u
+  unfold Shared0FieldElement51.Insts.CoreOpsArithNegFieldElement51.neg
+  step with (neg_spec u u0 u1 u2 u3 u4 hul (by bnd)) as ⟨fe6, hbfe6, hfe6⟩
+  step with (fe_ct_eq_spec check fe6) as ⟨flipped, hf01, hfiff⟩
+  let* ⟨ fe7, hbfe7, hfe7 ⟩ ← mul_spec' by bnd
+  step with (fe_ct_eq_spec check fe7) as ⟨flipped_i, hfi01, hfiiff⟩
+  -- r′ = √−1 · r
+  let* ⟨ r_prime, hbrp, hrp ⟩ ← mul_spec' by bnd
+  -- the flip choice and the root flip
+  simp only [subtle.Choice.Insts.CoreOpsBitBitOrChoiceChoice.bitor, bind_tc_ok]
+  obtain ⟨rr0, rr1, rr2, rr3, rr4, hrl⟩ := Fe.exists_limbs r
+  obtain ⟨rp0, rp1, rp2, rp3, rp4, hrpl⟩ := Fe.exists_limbs r_prime
+  step with (fe_cond_assign_spec r r_prime _ rr0 rr1 rr2 rr3 rr4 rp0 rp1 rp2 rp3 rp4 hrl hrpl)
+    as ⟨r1, hr1l⟩
+  -- sign normalization
+  step with (is_negative_spec r1) as ⟨rneg, hrneg⟩
+  obtain ⟨q0, q1, q2, q3, q4, hq⟩ := Fe.exists_limbs r1
+  -- Bnd r1 (2^52): its list is one of the two bounded lists
+  have hbr1 : Bnd r1 (2^52) := by
+    have hb1 : Bnd r (2^52) := Bnd.mono hbr (by norm_num)
+    have hb2 : Bnd r_prime (2^52) := Bnd.mono hbrp (by norm_num)
+    split at hr1l
+    · rw [Bnd_eq r1 rr0 rr1 rr2 rr3 rr4 _ (by rw [hr1l])]
+      rw [Bnd_eq r rr0 rr1 rr2 rr3 rr4 _ hrl] at hb1
+      exact hb1
+    · rw [Bnd_eq r1 rp0 rp1 rp2 rp3 rp4 _ (by rw [hr1l])]
+      rw [Bnd_eq r_prime rp0 rp1 rp2 rp3 rp4 _ hrpl] at hb2
+      exact hb2
+  -- −r1 and the parity select
+  step with (neg_spec r1 q0 q1 q2 q3 q4 hq (Bnd.mono hbr1 (by norm_num)))
+    as ⟨r_neg, hbrn, hrn⟩
+  obtain ⟨n0, n1, n2, n3, n4, hnl⟩ := Fe.exists_limbs r_neg
+  step with (fe_cond_assign_spec r1 r_neg _ q0 q1 q2 q3 q4 n0 n1 n2 n3 n4 hq hnl)
+    as ⟨r2, hr2l⟩
+  try simp only [spec_ok]
+  -- ── interpreted values ───────────────────────────────────────────────────
+  have hfe2v : ⟪fe2⟫ = ⟪u⟫ * ⟪v⟫^3 := by rw [hfe2, hv3, hfe]; ring
+  have hfe3v : ⟪fe3⟫ = ⟪u⟫ * ⟪v⟫^7 := by rw [hfe3, hv7, hfe1, hv3, hfe]; ring
+  have hrval : ⟪r⟫ = ⟪u⟫ * ⟪v⟫^3 * (⟪u⟫ * ⟪v⟫^7)^(2^252-3) := by
+    rw [hr, hfe2v, hfe4, hfe3v]
+  have hcheckv : ⟪check⟫ = ⟪v⟫ * ⟪r⟫^2 := by rw [hcheck, hfe5]; ring
+  have hcore := sqrt_core ⟪u⟫ ⟪v⟫ x hvne hx
+  rw [← hrval] at hcore
+  have hrpv : ⟪r_prime⟫ = ⟪im⟫ * ⟪r⟫ := hrp
+  -- denote transfer along the two selects
+  have hr1d : (flipped ||| flipped_i).val = 0 ∧ ⟪r1⟫ = ⟪r⟫ ∨
+      (flipped ||| flipped_i).val ≠ 0 ∧ ⟪r1⟫ = ⟪r_prime⟫ := by
+    split at hr1l
+    · left
+      refine ⟨by assumption, ?_⟩
+      unfold denote
+      rw [feVal_eq r1 rr0 rr1 rr2 rr3 rr4 (by rw [hr1l]),
+          feVal_eq r rr0 rr1 rr2 rr3 rr4 hrl]
+    · right
+      refine ⟨by assumption, ?_⟩
+      unfold denote
+      rw [feVal_eq r1 rp0 rp1 rp2 rp3 rp4 (by rw [hr1l]),
+          feVal_eq r_prime rp0 rp1 rp2 rp3 rp4 hrpl]
+  have hr2d : rneg.val = 0 ∧ ⟪r2⟫ = ⟪r1⟫ ∨ rneg.val ≠ 0 ∧ ⟪r2⟫ = ⟪r_neg⟫ := by
+    split at hr2l
+    · left
+      refine ⟨by assumption, ?_⟩
+      unfold denote
+      rw [feVal_eq r2 q0 q1 q2 q3 q4 (by rw [hr2l]),
+          feVal_eq r1 q0 q1 q2 q3 q4 hq]
+    · right
+      refine ⟨by assumption, ?_⟩
+      unfold denote
+      rw [feVal_eq r2 n0 n1 n2 n3 n4 (by rw [hr2l]),
+          feVal_eq r_neg n0 n1 n2 n3 n4 hnl]
+  -- ── choice values from the three checks ──────────────────────────────────
+  -- the value equation carried by r1 in every case: ⟪r1⟫²·⟪v⟫ = ⟪u⟫ and the
+  -- flip choice consistent with the branch taken
+  have hval1 : ⟪r1⟫ ^ 2 * ⟪v⟫ = ⟪u⟫ ∧ (correct ||| flipped).val = 1 := by
+    haveI : Fact (Nat.Prime P) := ⟨P_prime⟩
+    have hc01' := hc01
+    have hf01' := hf01
+    have hfi01' := hfi01
+    by_cases hu0 : ⟪u⟫ = 0
+    · -- u = 0: check = v·r² = ±0 = 0; every flag fires; r1 = im·r with r-part 0
+      have hchk0 : ⟪check⟫ = 0 := by
+        rcases hcore with h | h <;> rw [hcheckv]
+        · rw [show ⟪v⟫ * ⟪r⟫^2 = ⟪v⟫ * (⟪u⟫ * ⟪v⟫^3 * (⟪u⟫*⟪v⟫^7)^(2^252-3))^2 from by rw [hrval]]
+          rw [hrval] at h
+          rw [h, hu0]
+        · rw [hrval] at h ⊢
+          rw [h, hu0]
+          ring
+      have hr0 : ⟪v⟫ * ⟪r⟫^2 = 0 := by rw [← hcheckv]; exact hchk0
+      have hrz : ⟪r⟫ = 0 := by
+        rcases mul_eq_zero.mp hr0 with h | h
+        · exact absurd h hvne
+        · exact pow_eq_zero_iff (n := 2) (by norm_num) |>.mp h
+      have hcv : correct.val = 1 := hciff.mpr (by rw [hchk0, hu0])
+      have hor1 : (correct ||| flipped).val = 1 := by
+        rcases hf01 with h0 | h1
+        · have : flipped = 0#u8 := UScalar.eq_of_val_eq (by simp [h0])
+          rw [this]
+          have : correct = 1#u8 := UScalar.eq_of_val_eq (by simp [hcv])
+          rw [this]
+          rfl
+        · have : flipped = 1#u8 := UScalar.eq_of_val_eq (by simp [h1])
+          rw [this]
+          have : correct = 1#u8 := UScalar.eq_of_val_eq (by simp [hcv])
+          rw [this]
+          rfl
+      refine ⟨?_, hor1⟩
+      rcases hr1d with ⟨-, hd⟩ | ⟨-, hd⟩
+      · rw [hd, hrz, hu0]; ring
+      · rw [hd, hrpv, hrz, hu0]; ring
+    · -- u ≠ 0: the disjunct decides everything
+      rcases hcore with hA | hB
+      · -- v·r² = u: no flip, correct = 1
+        have hcv : correct.val = 1 := hciff.mpr (by rw [hcheckv]; exact hA)
+        have hfv : flipped.val = 0 := by
+          rcases hf01 with h | h
+          · exact h
+          · exfalso
+            have := hfiff.mp h
+            rw [hcheckv, hfe6] at this
+            rw [hA] at this
+            exact hu0 ((eq_neg_self_iff_zero ⟪u⟫).mp this)
+        have hfiv : flipped_i.val = 0 := by
+          rcases hfi01 with h | h
+          · exact h
+          · exfalso
+            have := hfiiff.mp h
+            rw [hcheckv, hfe7, hfe6] at this
+            rw [hA] at this
+            have hfac : ⟪u⟫ * (1 + ⟪im⟫) = 0 := by linear_combination this
+            rcases mul_eq_zero.mp hfac with h' | h'
+            · exact hu0 h'
+            · exact one_add_i_ne_zero (by rw [← sq]; rw [sq]; exact him) h'
+        have hflip0 : (flipped ||| flipped_i).val = 0 := by
+          have h1 : flipped = 0#u8 := UScalar.eq_of_val_eq (by simp [hfv])
+          have h2 : flipped_i = 0#u8 := UScalar.eq_of_val_eq (by simp [hfiv])
+          rw [h1, h2]
+          rfl
+        refine ⟨?_, ?_⟩
+        · rcases hr1d with ⟨-, hd⟩ | ⟨hne, -⟩
+          · rw [hd]; linear_combination hA
+          · exact absurd hflip0 hne
+        · have h1 : correct = 1#u8 := UScalar.eq_of_val_eq (by simp [hcv])
+          have h2 : flipped = 0#u8 := UScalar.eq_of_val_eq (by simp [hfv])
+          rw [h1, h2]
+          rfl
+      · -- v·r² = −u: flip fires, r1 = im·r
+        have hfv : flipped.val = 1 := hfiff.mpr (by rw [hcheckv, hfe6]; exact hB)
+        have hflip1 : (flipped ||| flipped_i).val ≠ 0 := by
+          have h1 : flipped = 1#u8 := UScalar.eq_of_val_eq (by simp [hfv])
+          rw [h1]
+          rcases hfi01 with h | h
+          · have h2 : flipped_i = 0#u8 := UScalar.eq_of_val_eq (by simp [h])
+            rw [h2]
+            decide
+          · have h2 : flipped_i = 1#u8 := UScalar.eq_of_val_eq (by simp [h])
+            rw [h2]
+            decide
+        refine ⟨?_, ?_⟩
+        · rcases hr1d with ⟨h0, -⟩ | ⟨-, hd⟩
+          · exact absurd h0 hflip1
+          · rw [hd, hrpv]
+            have him2 : ⟪im⟫ ^ 2 = -1 := by rw [sq]; exact him
+            have : (⟪im⟫ * ⟪r⟫) ^ 2 * ⟪v⟫ = ⟪im⟫^2 * (⟪v⟫ * ⟪r⟫^2) := by ring
+            rw [this, him2, hB]
+            ring
+        · have h2 : flipped = 1#u8 := UScalar.eq_of_val_eq (by simp [hfv])
+          rw [h2]
+          rcases hc01 with h | h
+          · have h1 : correct = 0#u8 := UScalar.eq_of_val_eq (by simp [h])
+            rw [h1]
+            rfl
+          · have h1 : correct = 1#u8 := UScalar.eq_of_val_eq (by simp [h])
+            rw [h1]
+            rfl
+  obtain ⟨hval1', hwas⟩ := hval1
+  -- ── parity normalization and the final post ─────────────────────────────
+  haveI : NeZero P := ⟨by unfold P; norm_num⟩
+  have hrnegv : rneg.val = (⟪r1⟫).val % 2 := by
+    rw [hrneg]
+    unfold denote
+    rw [ZMod.val_natCast]
+  have hbr2 : Bnd r2 (2^52) := by
+    split at hr2l
+    · rw [Bnd_eq r2 q0 q1 q2 q3 q4 _ (by rw [hr2l])]
+      rw [Bnd_eq r1 q0 q1 q2 q3 q4 _ hq] at hbr1
+      exact hbr1
+    · have hb3 : Bnd r_neg (2^52) := hbrn
+      rw [Bnd_eq r2 n0 n1 n2 n3 n4 _ (by rw [hr2l])]
+      rw [Bnd_eq r_neg n0 n1 n2 n3 n4 _ hnl] at hb3
+      exact hb3
+  refine ⟨hwas, hbr2, ?_, ?_⟩
+  · -- the square equation survives the sign normalization
+    rcases hr2d with ⟨-, hd⟩ | ⟨-, hd⟩
+    · rw [hd]; exact hval1'
+    · rw [hd, hrn]
+      have : (-⟪r1⟫) ^ 2 * ⟪v⟫ = ⟪r1⟫ ^ 2 * ⟪v⟫ := by ring
+      rw [this]
+      exact hval1'
+  · -- even parity
+    rcases hr2d with ⟨h0, hd⟩ | ⟨hne, hd⟩
+    · rw [hd]
+      rw [hrnegv] at h0
+      exact h0
+    · rw [hd, hrn]
+      have hodd : rneg.val = 1 := by
+        have := hrnegv
+        omega
+      rw [hrnegv] at hodd
+      have hr1nz : ⟪r1⟫ ≠ 0 := by
+        intro hz
+        rw [hz] at hodd
+        simp at hodd
+      have hnegval : (-⟪r1⟫).val = P - (⟪r1⟫).val := by
+        rw [ZMod.neg_val, if_neg hr1nz]
+      rw [hnegval]
+      have hlt := ZMod.val_lt ⟪r1⟫
+      have hpodd : P % 2 = 1 := by unfold P; norm_num
+      have hpos : 0 < (⟪r1⟫).val := by
+        rcases Nat.eq_zero_or_pos (⟪r1⟫).val with h | h
+        · exact absurd ((ZMod.val_eq_zero _).mp h) hr1nz
+        · exact h
+      omega
+
 end CurveFieldProofs

verification/check.sh

@@ -99,6 +99,7 @@ CERTS=(
   CurveFieldProofs.pow_p58_spec
   CurveFieldProofs.fe_ct_eq_spec
   CurveFieldProofs.sqrt_core
+  CurveFieldProofs.sqrt_ratio_i_sq_spec
 )
 # Imports needed so every certificate in CERTS is in scope for the audit.
 AUDIT_IMPORTS=(