Merge claude/codex-prove-sqrt-cbrt into dcmt/codex-prove-sqrt-cbrt

Author: duncancmt

formal/cbrt/Cbrt512Proof/Cbrt512Proof.lean

@@ -1,5 +1,6 @@
 -- Root of the Cbrt512Proof library.
 import Cbrt512Proof.GeneratedCbrt512Model
+import Cbrt512Proof.CbrtNumericCerts
 import Cbrt512Proof.Cbrt512Correct
 import Cbrt512Proof.CbrtDenormalization
 import Cbrt512Proof.CbrtNormalization

formal/cbrt/Cbrt512Proof/Cbrt512Proof/CbrtBaseCase.lean

@@ -6,6 +6,7 @@
 -/
 import Cbrt512Proof.GeneratedCbrt512Model
 import Cbrt512Proof.EvmBridge
+import Cbrt512Proof.CbrtNumericCerts
 import CbrtProof.CbrtCorrect
 import CbrtProof.CertifiedChain
 import CbrtProof.FiniteCert
@@ -123,15 +124,18 @@ private theorem icbrt_le_hi_of_pow_lt_cube (w hi : Nat) (k : Nat)
 theorem baseCase_NR_within_1ulp (w : Nat)
     (hw_lo : 2 ^ 251 ≤ w) (hw_hi : w < 2 ^ 254) :
     let m := icbrt w
-    let z := run6From w 22141993662453218394297550
+    let z := run6From w baseCaseSeed
     m ≤ z ∧ z ≤ m + 1 := by
   simp only
   let s : Nat := 22141993662453218394297550
   let m := icbrt w
   have hmlo : m * m * m ≤ w := icbrt_cube_le w
   have hmhi : w < (m + 1) * (m + 1) * (m + 1) := icbrt_lt_succ_cube w
-  have hsPos : 0 < s := by omega
   have hw_pos : 0 < w := by omega
+  have hs_lo : 2 ^ 83 ≤ s := by
+    change 2 ^ 83 ≤ baseCaseSeed
+    exact baseCaseSeed_bounds.1
+  have hsPos : 0 < s := by omega
   -- Lower bound
   have hmz : m ≤ run6From w s := by
     unfold run6From
@@ -142,72 +146,78 @@ theorem baseCase_NR_within_1ulp (w : Nat)
             (cbrtStep_pos w _ hw_pos
               (cbrtStep_pos w _ hw_pos hsPos)))))
       hmlo
-  refine ⟨hmz, ?_⟩
+  have hmz' : m ≤ run6From w baseCaseSeed := by
+    simpa [s, baseCaseSeed] using hmz
+  refine ⟨hmz', ?_⟩
   -- Case split on octave
   by_cases h252 : w < 2 ^ 252
   · -- Octave 251: w ∈ [2^251, 2^252)
-    -- lo = 15352400942462240883748044, hi = 19342813113834066795298815
-    let lo : Nat := 15352400942462240883748044
-    have hlo : lo ≤ m := lo_le_icbrt_of_cube_le_pow w lo 251 (by native_decide) hw_lo
-    have hhi : m ≤ 19342813113834066795298815 :=
-      icbrt_le_hi_of_pow_lt_cube w 19342813113834066795298815 251 (by native_decide) h252
-    have hm2 : 2 ≤ m := by omega
-    -- d1 bound
-    have hd1 : cbrtStep w s - m ≤ 1994218922075376856504634 := by
-      have h := cbrt_d1_bound w m s lo 19342813113834066795298815 hsPos hmlo hmhi hlo hhi
-      have : max (s - lo) (19342813113834066795298815 - s) = 6789592719990977510549506 := by
-        native_decide
-      rw [this] at h
-      have : (6789592719990977510549506 * 6789592719990977510549506 *
-          (19342813113834066795298815 + 2 * s) + 3 * 19342813113834066795298815 *
-          (19342813113834066795298815 + 1)) / (3 * (s * s)) =
-          1994218922075376856504634 := by native_decide
-      omega
-    exact chain_6steps_upper w m lo s 1994218922075376856504634
-      hm2 (by omega : 0 < lo) hlo hsPos hmlo hmhi hd1
-      (Nat.le_trans (by native_decide : 2 * 1994218922075376856504634 ≤ lo) hlo)
-      (by native_decide) (by native_decide) (by native_decide) (by native_decide) (by native_decide)
+    have hlo : octave251Lo ≤ m :=
+      lo_le_icbrt_of_cube_le_pow w octave251Lo 251 octave251_bounds.1 hw_lo
+    have hhi : m ≤ octave251Hi :=
+      icbrt_le_hi_of_pow_lt_cube w octave251Hi 251 octave251_bounds.2 h252
+    have hm2 : 2 ≤ m := Nat.le_trans octave251_lo_two_le hlo
+    have hd1 : cbrtStep w s - m ≤ octave251D1 := by
+      have h := cbrt_d1_bound w m s octave251Lo octave251Hi hsPos hmlo hmhi hlo hhi
+      rw [show max (s - octave251Lo) (octave251Hi - s) = octave251Gap by
+        simpa [s, baseCaseSeed] using octave251_gap_eq] at h
+      have hformula :
+          (octave251Gap * octave251Gap * (octave251Hi + 2 * s) +
+            3 * octave251Hi * (octave251Hi + 1)) / (3 * (s * s)) = octave251D1 := by
+        simpa [s, baseCaseSeed] using octave251_d1_formula_eq
+      simpa [hformula] using h
+    obtain ⟨h2d1, h2d2, h2d3, h2d4, h2d5, hd6_le1⟩ := octave251_chain_bounds
+    have hloPos : 0 < octave251Lo := Nat.lt_of_lt_of_le (by omega : 0 < 2) octave251_lo_two_le
+    have hup : run6From w s ≤ m + 1 :=
+      chain_6steps_upper w m octave251Lo s octave251D1
+      hm2 hloPos hlo hsPos hmlo hmhi hd1
+      (Nat.le_trans h2d1 hlo) h2d2 h2d3 h2d4 h2d5 hd6_le1
+    simpa [s, baseCaseSeed] using hup
   · by_cases h253 : w < 2 ^ 253
     · -- Octave 252: w ∈ [2^252, 2^253)
-      let lo : Nat := 19342813113834066795298816
-      have hlo : lo ≤ m := lo_le_icbrt_of_cube_le_pow w lo 252 (by native_decide) (by omega)
-      have hhi : m ≤ 24370417406302138235346347 :=
-        icbrt_le_hi_of_pow_lt_cube w 24370417406302138235346347 252 (by native_decide) h253
-      have hm2 : 2 ≤ m := by omega
-      have hd1 : cbrtStep w s - m ≤ 365742585066387069963242 := by
-        have h := cbrt_d1_bound w m s lo 24370417406302138235346347 hsPos hmlo hmhi hlo hhi
-        have : max (s - lo) (24370417406302138235346347 - s) =
-            2799180548619151598998734 := by native_decide
-        rw [this] at h
-        have : (2799180548619151598998734 * 2799180548619151598998734 *
-            (24370417406302138235346347 + 2 * s) + 3 * 24370417406302138235346347 *
-            (24370417406302138235346347 + 1)) / (3 * (s * s)) =
-            365742585066387069963242 := by native_decide
-        omega
-      exact chain_6steps_upper w m lo s 365742585066387069963242
-        hm2 (by omega : 0 < lo) hlo hsPos hmlo hmhi hd1
-        (Nat.le_trans (by native_decide : 2 * 365742585066387069963242 ≤ lo) hlo)
-        (by native_decide) (by native_decide) (by native_decide) (by native_decide) (by native_decide)
+      have hlo : octave252Lo ≤ m :=
+        lo_le_icbrt_of_cube_le_pow w octave252Lo 252 octave252_bounds.1 (by omega)
+      have hhi : m ≤ octave252Hi :=
+        icbrt_le_hi_of_pow_lt_cube w octave252Hi 252 octave252_bounds.2 h253
+      have hm2 : 2 ≤ m := Nat.le_trans octave252_lo_two_le hlo
+      have hd1 : cbrtStep w s - m ≤ octave252D1 := by
+        have h := cbrt_d1_bound w m s octave252Lo octave252Hi hsPos hmlo hmhi hlo hhi
+        rw [show max (s - octave252Lo) (octave252Hi - s) = octave252Gap by
+          simpa [s, baseCaseSeed] using octave252_gap_eq] at h
+        have hformula :
+            (octave252Gap * octave252Gap * (octave252Hi + 2 * s) +
+              3 * octave252Hi * (octave252Hi + 1)) / (3 * (s * s)) = octave252D1 := by
+          simpa [s, baseCaseSeed] using octave252_d1_formula_eq
+        simpa [hformula] using h
+      obtain ⟨h2d1, h2d2, h2d3, h2d4, h2d5, hd6_le1⟩ := octave252_chain_bounds
+      have hloPos : 0 < octave252Lo := Nat.lt_of_lt_of_le (by omega : 0 < 2) octave252_lo_two_le
+      have hup : run6From w s ≤ m + 1 :=
+        chain_6steps_upper w m octave252Lo s octave252D1
+        hm2 hloPos hlo hsPos hmlo hmhi hd1
+        (Nat.le_trans h2d1 hlo) h2d2 h2d3 h2d4 h2d5 hd6_le1
+      simpa [s, baseCaseSeed] using hup
     · -- Octave 253: w ∈ [2^253, 2^254)
-      let lo : Nat := 24370417406302138235346347
-      have hlo : lo ≤ m := lo_le_icbrt_of_cube_le_pow w lo 253 (by native_decide) (by omega)
-      have hhi : m ≤ 30704801884924481767496089 :=
-        icbrt_le_hi_of_pow_lt_cube w 30704801884924481767496089 253 (by native_decide) hw_hi
-      have hm2 : 2 ≤ m := by omega
-      have hd1 : cbrtStep w s - m ≤ 3738299367780524623633435 := by
-        have h := cbrt_d1_bound w m s lo 30704801884924481767496089 hsPos hmlo hmhi hlo hhi
-        have : max (s - lo) (30704801884924481767496089 - s) =
-            8562808222471263373198539 := by native_decide
-        rw [this] at h
-        have : (8562808222471263373198539 * 8562808222471263373198539 *
-            (30704801884924481767496089 + 2 * s) + 3 * 30704801884924481767496089 *
-            (30704801884924481767496089 + 1)) / (3 * (s * s)) =
-            3738299367780524623633435 := by native_decide
-        omega
-      exact chain_6steps_upper w m lo s 3738299367780524623633435
-        hm2 (by omega : 0 < lo) hlo hsPos hmlo hmhi hd1
-        (Nat.le_trans (by native_decide : 2 * 3738299367780524623633435 ≤ lo) hlo)
-        (by native_decide) (by native_decide) (by native_decide) (by native_decide) (by native_decide)
+      have hlo : octave253Lo ≤ m :=
+        lo_le_icbrt_of_cube_le_pow w octave253Lo 253 octave253_lo_cube_le_pow253 (by omega)
+      have hhi : m ≤ M_TOP :=
+        icbrt_le_hi_of_pow_lt_cube w M_TOP 253 m_top_cube_bounds.2 hw_hi
+      have hm2 : 2 ≤ m := Nat.le_trans octave253_lo_two_le hlo
+      have hd1 : cbrtStep w s - m ≤ octave253D1 := by
+        have h := cbrt_d1_bound w m s octave253Lo M_TOP hsPos hmlo hmhi hlo hhi
+        rw [show max (s - octave253Lo) (M_TOP - s) = octave253Gap by
+          simpa [s, baseCaseSeed] using octave253_gap_eq] at h
+        have hformula :
+            (octave253Gap * octave253Gap * (M_TOP + 2 * s) +
+              3 * M_TOP * (M_TOP + 1)) / (3 * (s * s)) = octave253D1 := by
+          simpa [s, baseCaseSeed] using octave253_d1_formula_eq
+        simpa [hformula] using h
+      obtain ⟨h2d1, h2d2, h2d3, h2d4, h2d5, hd6_le1⟩ := octave253_chain_bounds
+      have hloPos : 0 < octave253Lo := Nat.lt_of_lt_of_le (by omega : 0 < 2) octave253_lo_two_le
+      have hup : run6From w s ≤ m + 1 :=
+        chain_6steps_upper w m octave253Lo s octave253D1
+        hm2 hloPos hlo hsPos hmlo hmhi hd1
+        (Nat.le_trans h2d1 hlo) h2d2 h2d3 h2d4 h2d5 hd6_le1
+      simpa [s, baseCaseSeed] using hup
 
 -- ============================================================================
 -- Base case EVM bridge
@@ -264,22 +274,21 @@ theorem model_cbrtBaseCase_evm_correct (x_hi_1 : Nat)
     show x_hi_1 / 4 < 2 ^ 254; unfold WORD_MOD at hx_hi; omega
   have hw_wm : w < WORD_MOD := by show x_hi_1 / 4 < WORD_MOD; unfold WORD_MOD; omega
   have hm_lo : 2 ^ 83 ≤ m :=
-    lo_le_icbrt_of_cube_le_pow w (2 ^ 83) 251 (by native_decide) hw_lo
+    lo_le_icbrt_of_cube_le_pow w (2 ^ 83) 251 pow83_cube_le_pow251 hw_lo
   have hm_hi : m < 2 ^ 85 := by
     show icbrt w < 2 ^ 85
-    have := icbrt_le_hi_of_pow_lt_cube w (2 ^ 85 - 1) 253 (by native_decide) hw_hi
+    have := icbrt_le_hi_of_pow_lt_cube w (2 ^ 85 - 1) 253 pow254_le_succ_pow85_sub_one_cube hw_hi
     omega
   have hm_wm : m < WORD_MOD := by unfold WORD_MOD; omega
   have hm2_le : m * m ≤ (2 ^ 85 - 1) * (2 ^ 85 - 1) :=
     Nat.mul_le_mul (by omega) (by omega)
   have hm2_wm : m * m < WORD_MOD := by
-    have : (2 ^ 85 - 1) * (2 ^ 85 - 1) < WORD_MOD := by unfold WORD_MOD; native_decide
+    have : (2 ^ 85 - 1) * (2 ^ 85 - 1) < WORD_MOD := pow85_sub_one_sq_lt_word
     omega
   have hm3_le : m * m * m ≤ (2 ^ 85 - 1) * (2 ^ 85 - 1) * (2 ^ 85 - 1) :=
     Nat.mul_le_mul hm2_le (by omega)
   have hm3_wm : m * m * m < WORD_MOD := by
-    have : (2 ^ 85 - 1) * (2 ^ 85 - 1) * (2 ^ 85 - 1) < WORD_MOD := by
-      unfold WORD_MOD; native_decide
+    have : (2 ^ 85 - 1) * (2 ^ 85 - 1) * (2 ^ 85 - 1) < WORD_MOD := pow85_sub_one_cube_lt_word
     omega
   have h3m2_wm : 3 * (m * m) < WORD_MOD := by omega
   have h3m2_pos : 3 * (m * m) > 0 := by
@@ -294,8 +303,12 @@ theorem model_cbrtBaseCase_evm_correct (x_hi_1 : Nat)
     push_cast; simp [Int.add_mul, Int.mul_add, Int.mul_one, Int.one_mul]; omega
   -- ======== NR chain: 6 steps ========
   let s := (22141993662453218394297550 : Nat)
-  have hs_lo : 2 ^ 83 ≤ s := by native_decide
-  have hs_hi : s < 2 ^ 88 := by native_decide
+  have hs_lo : 2 ^ 83 ≤ s := by
+    change 2 ^ 83 ≤ baseCaseSeed
+    exact baseCaseSeed_bounds.1
+  have hs_hi : s < 2 ^ 88 := by
+    change baseCaseSeed < 2 ^ 88
+    exact baseCaseSeed_bounds.2
   let z1 := cbrtStep w s
   let z2 := cbrtStep w z1
   let z3 := cbrtStep w z2
@@ -339,7 +352,7 @@ theorem model_cbrtBaseCase_evm_correct (x_hi_1 : Nat)
     unfold WORD_MOD; omega
   -- ======== Shift lemma ========
   have hshift : evmShr (evmAnd (evmAnd 2 255) 255) x_hi_1 = w := by
-    have : evmAnd (evmAnd 2 255) 255 = 2 := by native_decide
+    have : evmAnd (evmAnd 2 255) 255 = 2 := baseCaseShiftMask_eq_two
     rw [this]; exact evmShr_eq' 2 x_hi_1 (by omega) hx_hi
   -- ======== EVM bridge: z6² and z6³ ========
   have hevmMul_z6z6 : evmMul z6 z6 = z6 * z6 := by

formal/cbrt/Cbrt512Proof/Cbrt512Proof/CbrtComposition.lean

@@ -67,7 +67,7 @@ theorem r_qc_properties (x_hi_1 x_lo_1 : Nat)
     exact Nat.not_lt.mp fun h =>
       absurd hsucc_gt
         (Nat.not_lt.mpr (Nat.le_trans (cube_monotone (Nat.le_sub_one_of_lt h)) hB))
-  · -- [3] r_qc³ < WORD_MOD²: r_qc ≤ R_MAX (E1), so r_qc³ ≤ R_MAX³ < WORD_MOD² (native_decide).
+  · -- [3] r_qc³ < WORD_MOD²: r_qc ≤ R_MAX (E1), so r_qc³ ≤ R_MAX³ < WORD_MOD² by certificate.
     exact Nat.lt_of_le_of_lt (cube_monotone hE1) r_max_cube_lt_wm2
   · -- [4] r_qc³ > x_norm → icbrt³ < x_norm: from E2.
     exact hE2