Prove error bounds on formally-verified natural logarithm

.github/workflows/ln-formal.yml

@@ -53,12 +53,6 @@ jobs:
         env:
           FOUNDRY_SOLC_VERSION: 0.8.34
 
-      - name: Check floor-specification witness and helper mirror
-        run: python3 -W error -m formal.python.ln.check_ln_counterexample
-
-      - name: Check monotonicity certificate
-        run: python3 -W error -m formal.python.ln.check_ln_monotone
-
       - name: Generate Lean model from Ln.sol via Yul IR
         run: |
           forge inspect src/wrappers/LnWrapper.sol:LnWrapper ir | \
@@ -69,6 +63,19 @@ jobs:
       - name: Generate certificate coefficient literals
         run: python3 -W error formal/python/ln/gen_cert_literals.py
 
+      - name: Generate floor cert cell covers and bias cap numerator
+        working-directory: formal/ln/LnProof
+        run: |
+          lake build LnProof.FloorCertLit LnProof.KroneckerShift LnProof.FloorConsts
+          lake env lean GenCover.lean
+          lake env lean GenErr1.lean
+
+      - name: Generate error-bound cert literals and cell covers
+        working-directory: formal/ln/LnProof
+        run: |
+          lake build LnProof.ErrorBoundCore
+          lake env lean GenErrLit.lean
+
       - name: Build Ln proof and model evaluator
         working-directory: formal/ln/LnProof
         run: lake build && lake build ln-model

formal/ln/LnProof/.gitignore

@@ -10,3 +10,23 @@
 # Auto-generated; rebuild with:
 #   python3 formal/python/ln/gen_cert_literals.py
 /LnProof/FloorCertLit.lean
+
+# Auto-generated error-bound cert literals + cell covers; rebuild with:
+#   lake build LnProof.ErrorBoundCore && lake env lean GenErrLit.lean
+/LnProof/ErrCertLtLit.lean
+/LnProof/ErrCertGeLit.lean
+/LnProof/ErrCertLt.lean
+/LnProof/ErrCertGe.lean
+/LnProof/ErrCertLtC*.lean
+/LnProof/ErrCertGeC*.lean
+
+# Auto-generated floor cert cell covers; rebuild with:
+#   lake build LnProof.FloorCertLit LnProof.KroneckerShift && lake env lean GenCover.lean
+/LnProof/FloorCertGeUpC*.lean
+/LnProof/FloorCertLtUpC*.lean
+/LnProof/FloorCertGeLoC*.lean
+/LnProof/FloorCertLtLoC*.lean
+
+# Auto-generated tight bias-cap numerator; rebuild with:
+#   lake build LnProof.FloorConsts && lake env lean GenErr1.lean
+/LnProof/BiasCapNum.lean

formal/ln/LnProof/GenCover.lean

@@ -0,0 +1,100 @@
+import LnProof.FloorCertLit
+import LnProof.KroneckerShift
+
+/-!
+# Cover generator (committed tool)
+
+Greedily walks `[lo, hi]` for a certificate polynomial, computing at each anchor
+`a` the largest cell width `w` with `0 ≤ (hornerIv (kShiftWitness kB C a) 0 w).1`
+— exactly the predicate the in-kernel `checkCoverK` decides, so the emitted
+covers are guaranteed `decide`-acceptable.  Writes one `…C<NN>.lean` cell file
+per sub-cell and prints the `_nonneg` ladder + import block to splice into the
+cover module.
+
+Run with `lake env lean GenCover.lean` (after `lake build LnProof.FloorCertLit`).
+-/
+
+open LnPoly LnFloorCert
+
+namespace GenCover
+
+/-- Largest `w ∈ [0, hiW]` with `0 ≤ (hornerIv S 0 w).1` (non-increasing in `w`). -/
+partial def maxW (S : List Int) (hiW : Int) : Int :=
+  let rec bs (lo hi : Int) : Int :=
+    if lo ≥ hi then lo
+    else
+      let mid := (lo + hi + 1) / 2
+      if 0 ≤ (hornerIv S 0 mid).1 then bs mid hi else bs lo (mid - 1)
+  bs 0 hiW
+
+/-- Greedy walk → `(reached?, (anchor, width) list)`. -/
+partial def walk (C : List Int) (lo hi : Int) : Bool × List (Int × Int) :=
+  let rec go (a : Int) (fuel : Nat) (acc : List (Int × Int)) : Bool × List (Int × Int) :=
+    match fuel with
+    | 0 => (false, acc.reverse)
+    | fuel + 1 =>
+      if a > hi then (true, acc.reverse)
+      else
+        let S := kShiftWitness kB C a
+        if 0 ≤ (hornerIv S 0 0).1 then
+          let w := maxW S (hi - a)
+          go (a + w + 1) fuel ((a, w) :: acc)
+        else (false, ((a, -1) :: acc).reverse)
+  go lo 200000 []
+
+def pad2 (i : Nat) : String := (if i < 10 then "0" else "") ++ toString i
+
+/-- Emit cell files `<modPrefix><NN>.lean` and return the ladder text. -/
+def emit (nm litName symName evalEqName modPrefix cellPrefix nonnegName : String)
+    (C : List Int) (lo hi : Int) : IO Unit := do
+  let (ok, cells) := walk C lo hi
+  IO.println s!"-- {nm}: reached={ok} ncells={cells.length}"
+  if ! ok then
+    IO.println s!"-- FAILED tail: {cells.drop (cells.length - 2)}"
+    return
+  -- write one cell file per sub-cell
+  for (aw, i) in cells.zipIdx do
+    let (a, w) := aw
+    let nn := pad2 i
+    let body :=
+      s!"import LnProof.FloorCertLit\nimport LnProof.KroneckerShift\n\nnamespace LnFloorCert\nopen LnPoly\n\nset_option maxRecDepth 100000\n\ntheorem {cellPrefix}{nn} : checkCoverK kB {litName} {a} {a + w}\n    [{w}] = true := by\n  decide +kernel\n\nend LnFloorCert\n"
+    IO.FS.writeFile s!"LnProof/{modPrefix}{nn}.lean" body
+  -- ladder + imports
+  let mut imps := ""
+  for (_, i) in cells.zipIdx do
+    imps := imps ++ s!"import LnProof.{modPrefix}{pad2 i}\n"
+  IO.println "==== IMPORTS ===="
+  IO.println imps
+  IO.println "==== LADDER ===="
+  let lb := "{"
+  let rb := "}"
+  IO.println s!"theorem {nonnegName} {lb}m : Int{rb} (h1 : {lo} ≤ m) (h2 : m ≤ {hi}) :"
+  IO.println s!"    0 ≤ evalPoly {symName} m := by"
+  IO.println s!"  have hev := {evalEqName} m"
+  IO.println "  rw [hev]"
+  let n := cells.length
+  for (aw, i) in cells.zipIdx do
+    let (a, w) := aw
+    if i + 1 < n then
+      IO.println s!"  rcases Int.lt_or_le m ({a + w} + 1) with h | h"
+      IO.println s!"  · exact checkCoverK_sound _ _ _ _ _ {cellPrefix}{pad2 i} m (by omega) (by omega)"
+    else
+      IO.println s!"  exact checkCoverK_sound _ _ _ _ _ {cellPrefix}{pad2 i} m (by omega) h2"
+
+end GenCover
+
+open GenCover
+
+def loLT : Int := 39614081257132168796771975168          -- 2^95
+def hiLT : Int := 56022770974786139918731938181          -- Sc - 46
+def loGE : Int := 56022770974786139918731938273          -- Sc + 46
+def hiGE : Int := 79228162514264337593543950335          -- 2^96 - 1
+
+-- Regenerate the never-overshoot covers (the +form certs at EUN=3382).
+-- All four floor cert covers (never-overshoot +form GeUp/LtUp, not-too-low
+-- −form GeLo/LtLo). The cover modules keep their hand-written eval_eq; only the
+-- cell files + the _nonneg ladder are generated.
+#eval emit "certGeUp" "certGeUpLit" "certGeUp" "geUp_eval_eq" "FloorCertGeUpC" "geUp_cell" "geUp_nonneg" certGeUpLit loGE hiGE
+#eval emit "certLtUp" "certLtUpLit" "certLtUp" "ltUp_eval_eq" "FloorCertLtUpC" "ltUp_cell" "ltUp_nonneg" certLtUpLit loLT hiLT
+#eval emit "certGeLo" "certGeLoLit" "certGeLo" "geLo_eval_eq" "FloorCertGeLoC" "geLo_cell" "geLo_nonneg" certGeLoLit loGE hiGE
+#eval emit "certLtLo" "certLtLoLit" "certLtLo" "ltLo_eval_eq" "FloorCertLtLoC" "ltLo_cell" "ltLo_nonneg" certLtLoLit loLT hiLT

formal/ln/LnProof/GenErr1.lean

@@ -0,0 +1,15 @@
+import LnProof.FloorConsts
+
+/-! Generate `BiasCapNum.lean`: the tight bias-cap numerator
+`biasCapNum = ⌊expNum 130 (BIASc·2²⁷) QS · 10⁶⁰ / (130!·QS¹³⁰)⌋`, the sharp lower
+cap on `e^(BIASc·2²⁷/QS)` used by `capBLtight` and the error weights. Computed
+from the committed inputs (BIASc), so it tracks any bias change. Run with
+`lake env lean GenErr1.lean` (after `lake build LnProof.FloorConsts`). -/
+
+open LnExp LnFloor LnGeneratedModel
+
+#eval do
+  let bcap := (LnExp.expNum 130 (BIASc * 2 ^ 27) QS * (10 ^ 18 * 10 ^ 42)) / (LnExp.fact 130 * QS ^ 130)
+  IO.FS.writeFile "LnProof/BiasCapNum.lean"
+    s!"/-! Generated by GenErr1 (lake env lean GenErr1.lean): the tight bias-cap\nnumerator BIASCAPNUM, the sharp lower cap on e^(BIASc·2^27/QS) used by\ncapBLtight and the error weights. -/\nnamespace LnFloorCert\n\ndef biasCapNum : Nat := {bcap}\n\nend LnFloorCert\n"
+  IO.println s!"BiasCapNum written: {bcap}"

formal/ln/LnProof/GenErrLit.lean

@@ -0,0 +1,102 @@
+import LnProof.ErrorBoundCore
+import LnProof.KroneckerShift
+
+/-! Regenerate the error-bound cert literals (ErrCertLtLit / ErrCertGeLit) and
+their covers for the new BIASc + boundNum.  Computes `certErrLt`/`certErrGe`
+inline (mirroring the ErrCert*Bridge constructions) so it does not depend on the
+bridges building, then walks the `checkCoverK` covers (literal signature, as the
+committed `errLt_nonneg`/`errGe_nonneg` use). -/
+
+open LnPoly LnFloorCert LnExp LnFloor LnGeneratedModel
+
+namespace GenErrLit
+
+-- All derived from the committed inputs (BIASc in the model, boundNum in
+-- ErrorBoundCert), so regenerating tracks any change to those automatically.
+def biasCapNum : Nat :=
+  (LnExp.expNum 130 (BIASc * 2 ^ 27) QS * (10 ^ 18 * 10 ^ 42)) / (LnExp.fact 130 * QS ^ 130)
+def errLtK : Int := (10 ^ 31 * (10 ^ 18 * 10 ^ 42) * lnErrQ * (10 ^ 40 + 160) : Nat)
+def errGeK : Int := errLtK
+def errLtW : Nat := biasCapNum * (lnErrQ + minPosAvail) * wadRayStrictDen * 10 ^ 40
+def errGeW : Nat := biasCapNum * (lnErrQ + (692115493 * 2 ^ 99 + 2 ^ 27 * 10 ^ 9)) * wadRayStrictDen * 10 ^ 40
+
+def cLt : List Int :=
+  polyAdd (polyScale ((errLtW : Int) * (fact 23 : Int)) (polyPow ltTDLit 23))
+    (polyScale (-errLtK) (polyMul [1, 1]
+      (polyAdd (polyScale 23 (polyMul (expPolyNum ltTNLit ltTDLit 22) ltTDLit))
+        (polyScale 2 (polyPow ltTNLit 23)))))
+
+def cGe : List Int :=
+  expMarginPoly 22 geTN2bLit geTD2bLit (polyScale errGeK [1, 1]) errGeW
+
+/-- Drop trailing zero coefficients (mirror gen_cert_literals.ptrim). -/
+def ptrim (a : List Int) : List Int :=
+  let r := (a.reverse.dropWhile (· == 0)).reverse
+  if r.isEmpty then [0] else r
+
+partial def maxW (S : List Int) (hiW : Int) : Int :=
+  let rec bs (lo hi : Int) : Int :=
+    if lo ≥ hi then lo
+    else let mid := (lo + hi + 1) / 2
+         if 0 ≤ (hornerIv S 0 mid).1 then bs mid hi else bs lo (mid - 1)
+  bs 0 hiW
+partial def walk (C : List Int) (lo hi : Int) : Bool × List (Int × Int) :=
+  let rec go (a : Int) (fuel : Nat) (acc : List (Int × Int)) : Bool × List (Int × Int) :=
+    match fuel with
+    | 0 => (false, acc.reverse)
+    | fuel + 1 =>
+      if a > hi then (true, acc.reverse)
+      else
+        let S := kShiftWitness kB C a
+        if 0 ≤ (hornerIv S 0 0).1 then
+          let w := maxW S (hi - a)
+          go (a + w + 1) fuel ((a, w) :: acc)
+        else (false, ((a, -1) :: acc).reverse)
+  go lo 200000 []
+
+def pad2 (i : Nat) : String := (if i < 10 then "0" else "") ++ toString i
+
+/-- Walk `[lo,hi]`, write one cell file per sub-cell, and write the complete
+cover module `coverMod` (cell imports + the literal-signature `nonnegName`
+ladder). The error covers carry no hand-written content, so they are fully
+generated. -/
+def emit (litFile litName coverMod modPrefix cellPrefix nonnegName : String) (C : List Int) (lo hi : Int) : IO Unit := do
+  let (ok, cells) := walk C lo hi
+  IO.println s!"-- {coverMod}: reached={ok} ncells={cells.length}"
+  if ! ok then IO.println s!"-- FAILED tail: {cells.drop (cells.length-2)}"; return
+  for (aw, i) in cells.zipIdx do
+    let (a, w) := aw
+    IO.FS.writeFile s!"LnProof/{modPrefix}{pad2 i}.lean"
+      s!"import LnProof.{litFile}\nimport LnProof.KroneckerShift\n\nnamespace LnFloorCert\nopen LnPoly\n\nset_option maxRecDepth 100000\n\ntheorem {cellPrefix}{pad2 i} : checkCoverK kB {litName} {a} {a + w}\n    [{w}] = true := by\n  decide +kernel\n\nend LnFloorCert\n"
+  let lb := "{"; let rb := "}"
+  let mut s := ""
+  for (_, i) in cells.zipIdx do s := s ++ s!"import LnProof.{modPrefix}{pad2 i}\n"
+  s := s ++ s!"\nnamespace LnFloorCert\nopen LnPoly\n\nset_option maxRecDepth 100000\n\n"
+  s := s ++ s!"theorem {nonnegName} {lb}m : Int{rb} (h1 : {lo} ≤ m) (h2 : m ≤ {hi}) :\n    0 ≤ evalPoly {litName} m := by\n"
+  let n := cells.length
+  for (aw, i) in cells.zipIdx do
+    let (a, w) := aw
+    if i + 1 < n then
+      s := s ++ s!"  rcases Int.lt_or_le m ({a + w} + 1) with h | h\n  · exact checkCoverK_sound _ _ _ _ _ {cellPrefix}{pad2 i} m (by omega) (by omega)\n"
+    else
+      s := s ++ s!"  exact checkCoverK_sound _ _ _ _ _ {cellPrefix}{pad2 i} m (by omega) h2\n"
+  s := s ++ "\nend LnFloorCert\n"
+  IO.FS.writeFile s!"LnProof/{coverMod}.lean" s
+
+def litText (name : String) (c : List Int) : String :=
+  "namespace LnFloorCert\n\ndef " ++ name ++ " : List Int := [\n  " ++
+  String.intercalate ",\n  " (c.map toString) ++ "]\n\nend LnFloorCert\n"
+
+end GenErrLit
+open GenErrLit
+def loLT : Int := 39614081257132168796771975168
+def hiLT : Int := 56022770974786139918731938181
+def loGE : Int := 56022770974786139918731938273
+def hiGE : Int := 79228162514264337593543950335
+
+#eval do
+  IO.FS.writeFile "LnProof/ErrCertLtLit.lean" (litText "certErrLtLit" (ptrim cLt))
+  IO.FS.writeFile "LnProof/ErrCertGeLit.lean" (litText "certErrGeLit" (ptrim cGe))
+  IO.println "literals written"
+  emit "ErrCertLtLit" "certErrLtLit" "ErrCertLt" "ErrCertLtC" "errLt_cell" "errLt_nonneg" (ptrim cLt) loLT hiLT
+  emit "ErrCertGeLit" "certErrGeLit" "ErrCertGe" "ErrCertGeC" "errGe_cell" "errGe_nonneg" (ptrim cGe) loGE hiGE

formal/ln/LnProof/LnProof.lean

@@ -5,3 +5,4 @@ import LnProof.LnMono
 import LnProof.TopMono
 import LnProof.FloorSpec
 import LnProof.ExpLogCutSpec
+import LnProof.ErrorBound

formal/ln/LnProof/LnProof/ErrCertGeBridge.lean

@@ -0,0 +1,113 @@
+import LnProof.ErrCertGe
+import LnProof.FloorCertGeLo
+import LnProof.FactoredCap
+
+/-!
+# Bridge: the ge error cell cover ⇒ the `sumGE` inequality (`hred`)
+
+`errGe_nonneg` proves `0 ≤ evalPoly certErrGeLit m` over the ge domain.  Here we
+identify the literal cert with the symbolic margin
+`certErrGe = expMarginPoly 22 geTN2b geTD2b (errGeK·(m+1)) errGeW`
+(an `evalPoly_ext` identity, exactly as `geLo_eval_eq`), and feed the existing
+`sumGE_of_expMarginPoly` to obtain the `sumGE`-shaped budget inequality that
+`ge_pos_cut_reduced` consumes (`hred`).
+
+The constants are the octave-extracted cell parameters at
+`lnErrorBoundNum = 1692115493`:
+`errGeK = 10^31·(10^18·10^42)·lnErrQ·(10^40+160)`,
+`errGeW = BIASCAPNUM·(lnErrQ+minPosAvail)·wadRayStrictDen·10^40`.
+-/
+
+namespace LnFloorCert
+
+open LnGeneratedModel LnPoly LnExp
+
+set_option maxRecDepth 100000
+
+def errGeK : Int :=
+  63382530011411470074835160268800000001014120480182583521197362564300800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
+
+/-- `errGeW = BIASCAPNUM · (lnErrQ + minPosAvailGe) · wadRayStrictDen · 10^40`,
+where `minPosAvailGe = 692115493·2^99 + 2^27·10^9` is the GE-internal bound
+(1.692115493 ulp) at which the ge cells were generated — tighter than the
+published bound, so the ge branch only tracks the bias here. -/
+def errGeW : Nat :=
+  biasCapNum *
+    (lnErrQ + (692115493 * 2 ^ 99 + 2 ^ 27 * 10 ^ 9)) * wadRayStrictDen * 10 ^ 40
+
+def certErrGe : List Int :=
+  expMarginPoly 22 geTN2b geTD2b (polyScale errGeK [1, 1]) errGeW
+
+theorem errGe_eval_eq : ∀ x : Int, evalPoly certErrGe x = evalPoly certErrGeLit x := by
+  refine evalPoly_ext (B := kB) certErrGe certErrGeLit ?_ ?_ ?_
+  · -- polyL1 bound on the symbolic margin, via the ℓ1 homomorphism lemmas on the
+    -- degree-12 literal bases; the full degree-221 poly is never reduced.
+    show polyL1 certErrGe * 2 < 2 ^ kB
+    have hadd := polyL1_polyAdd
+      (polyScale errGeW (expPolyNum geTN2bLit geTD2bLit 22))
+      (polyNeg (polyScale (fact 22 : Int)
+        (polyMul (polyScale errGeK [1, 1]) (polyPow geTD2bLit 22))))
+    have hneg := polyL1_polyNeg
+      (polyScale (fact 22 : Int)
+        (polyMul (polyScale errGeK [1, 1]) (polyPow geTD2bLit 22)))
+    have hA := polyL1_polyScale errGeW (expPolyNum geTN2bLit geTD2bLit 22)
+    have hAe := polyL1_expPolyNum geTN2bLit geTD2bLit 22
+    have hA2 : (errGeW : Int).natAbs * polyL1 (expPolyNum geTN2bLit geTD2bLit 22) ≤
+        (errGeW : Int).natAbs * expNum 22 (polyL1 geTN2bLit) (polyL1 geTD2bLit) :=
+      Nat.mul_le_mul_left _ hAe
+    have hB := polyL1_polyScale (fact 22 : Int)
+      (polyMul (polyScale errGeK [1, 1]) (polyPow geTD2bLit 22))
+    have hBm := polyL1_polyMul (polyScale errGeK [1, 1]) (polyPow geTD2bLit 22)
+    have hBs := polyL1_polyScale errGeK ([1, 1] : List Int)
+    have hBp := polyL1_polyPow geTD2bLit 22
+    have hBm2 : polyL1 (polyScale errGeK [1, 1]) * polyL1 (polyPow geTD2bLit 22) ≤
+        errGeK.natAbs * polyL1 ([1, 1] : List Int) * polyL1 geTD2bLit ^ 22 :=
+      Nat.mul_le_mul hBs hBp
+    have hB2 : (fact 22 : Int).natAbs *
+        polyL1 (polyMul (polyScale errGeK [1, 1]) (polyPow geTD2bLit 22)) ≤
+        (fact 22 : Int).natAbs *
+          (errGeK.natAbs * polyL1 ([1, 1] : List Int) * polyL1 geTD2bLit ^ 22) :=
+      Nat.mul_le_mul_left _ (Nat.le_trans hBm hBm2)
+    have hfin : ((errGeW : Int).natAbs *
+          expNum 22 (polyL1 geTN2bLit) (polyL1 geTD2bLit) +
+        (fact 22 : Int).natAbs *
+          (errGeK.natAbs * polyL1 ([1, 1] : List Int) * polyL1 geTD2bLit ^ 22)) * 2
+          < 2 ^ kB := by
+      decide +kernel
+    have hAfin := Nat.le_trans hA hA2
+    have hBfin := Nat.le_trans hB hB2
+    rw [hneg] at hadd
+    exact Nat.lt_of_le_of_lt
+      (Nat.mul_le_mul_right 2 (Nat.le_trans hadd (Nat.add_le_add hAfin hBfin))) hfin
+  · show polyL1 certErrGeLit * 2 < 2 ^ kB
+    decide +kernel
+  · show evalPoly certErrGe ((2 : Int) ^ kB) = evalPoly certErrGeLit ((2 : Int) ^ kB)
+    rw [int_two_pow kB]
+    unfold certErrGe expMarginPoly
+    rw [geTN2b_eq_lit, geTD2b_eq_lit]
+    simp only [evalPoly_polySub, evalPoly_polyScale, evalPoly_polyMul,
+      evalPoly_polyPow, evalPoly_expPolyNum, eval01]
+    decide +kernel
+
+/-- The ge cell cover discharges the `sumGE`-shaped budget inequality. -/
+theorem errGe_sumGE {m : Nat} (h1 : Sc + 46 ≤ m) (h2 : m < MHI) :
+    sumGE 22 (evalPoly geTN2b (m : Int)).toNat (evalPoly geTD2b (m : Int)).toNat
+      (evalPoly (polyScale errGeK [1, 1]) (m : Int)).toNat errGeW := by
+  have hge : (56022770974786139918731938273 : Int) ≤ (m : Int) := by
+    simp only [Sc] at h1; omega
+  have hle : (m : Int) ≤ 79228162514264337593543950335 := by
+    simp only [MHI] at h2; omega
+  have hnn : 0 ≤ evalPoly certErrGe (m : Int) := by
+    rw [errGe_eval_eq]; exact errGe_nonneg hge hle
+  have hyp : 0 ≤ evalPoly (polyScale errGeK [1, 1]) (m : Int) := by
+    rw [evalPoly_polyScale]
+    refine Int.mul_nonneg (by unfold errGeK; decide) ?_
+    have hm : (0 : Int) ≤ (m : Int) := Int.ofNat_nonneg m
+    simp only [evalPoly, Int.mul_zero, Int.add_zero, Int.mul_one]
+    omega
+  exact sumGE_of_expMarginPoly hnn
+    (Int.toNat_of_nonneg (geTN2b_nonneg_of_outer h1 h2)).symm
+    (Int.toNat_of_nonneg (Int.le_of_lt (geTD2b_pos_of_outer h1 h2))).symm
+    (Int.toNat_of_nonneg hyp).symm
+
+end LnFloorCert