refactor(lean): remove Float from FixedPoint core, implement integer-only sqrt/log2/expNeg

Core FixedPoint.lean is now fully Float-free: - Q16_16.sqrt: integer Newton method (intSqrt, 64-step fuel) - Q16_16.log2: bit-position extraction + linear interpolation - Q16_16.expNeg: 7-segment piecewise-linear (~0.02 max error) - Q0_16.log2: bit extraction with 1/ln(2) scaling Removed from core: ofFloat, toFloat, ln (Q16_16); toFloat, ofFloat (Q0_16); q0_64ScaleFloat, ofFloat, toFloat (Q0_64). Created Semantics.FixedPointBoundary for I/O boundary Float conversions. 14 downstream files updated to import boundary module. Build: 3573 jobs, 0 errors (lake build) Co-Authored-By: Allaun Silverfox <bigdataiscoming+9i37y6j2@protonmail.com>
2026-08-13 11:40:35 +00:00 · 2026-06-15 02:07:21 +00:00 · 2026-06-15 02:07:21 +00:00 · 8e741199bf
commit 8e741199bf
parent 9e43f50257
18 changed files with 181 additions and 71 deletions
--- a/0-Core-Formalism/lean/Semantics/AGENTS.md
+++ b/0-Core-Formalism/lean/Semantics/AGENTS.md
@ -30,9 +30,11 @@ lake build
  the formal source of truth.
 - Float (`Q16_16.ofFloat`, `Q0_16.ofFloat`, `Q0_64.ofFloat`) is forbidden in
  compute-path code. Use `Q16_16.ofNat`, `Q16_16.ofRatio`, or `Q16_16.ofInt`
-  instead. The historical 5 contamination sites in `BraidCross.lean:49,50,84`
-  and `BraidStrand.lean:57,71` are the canonical fixed-point constructor
-  template.
+  instead. As of 2026-06-15, the core `Semantics.FixedPoint` module is fully
+  Float-free: `ofFloat`/`toFloat` live in `Semantics.FixedPointBoundary` and
+  must only be imported at I/O boundaries. `Q16_16.sqrt`, `Q16_16.log2`,
+  `Q16_16.expNeg`, and `Q0_16.log2` use integer-only algorithms (Newton's
+  method, bit-position extraction, piecewise-linear approximation).
 - Every new compressor theorem pair MUST provide both `eigensolid_convergence`
  and `receipt_invertible`. The convergence theorem proves the crossing loop
  stabilizes; the invertibility theorem proves the receipt bijectively encodes
@ -107,7 +109,7 @@ lake build
 ```

 Compiler surface baseline: **3313 jobs, 0 errors** (`lake build Compiler`, commit `859d8726`, reverified 2026-05-28).
-Full workspace: **3572 jobs, 0 errors** (`lake build`, reverified 2026-06-15).
+Full workspace: **3573 jobs, 0 errors** (`lake build`, reverified 2026-06-15).
 PistSimulation: **3309 jobs, 0 errors** (`lake build Semantics.PistSimulation`, commit `778b78d3`, reverified 2026-05-27).
 EmergencyBoot: **3302 jobs, 0 errors** (`lake build Semantics.Hardware.EmergencyBootTypes Semantics.Hardware.EmergencyBootState Semantics.Hardware.EmergencyBootShell`, reverified 2026-05-27).

--- a/0-Core-Formalism/lean/Semantics/ExtensionScaffold/Compression/SignalPolicy.lean
+++ b/0-Core-Formalism/lean/Semantics/ExtensionScaffold/Compression/SignalPolicy.lean
@ -1,4 +1,5 @@
 import ExtensionScaffold.Compression.CellCore
+import Semantics.FixedPointBoundary

 set_option linter.dupNamespace false

--- a/0-Core-Formalism/lean/Semantics/Semantics/Autobalance.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/Autobalance.lean
@ -1,4 +1,5 @@
 import Semantics.FixedPoint
+import Semantics.FixedPointBoundary
 import Semantics.Bind

 namespace Semantics.Autobalance
--- a/0-Core-Formalism/lean/Semantics/Semantics/CGAVersorAddress.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/CGAVersorAddress.lean
@ -1,5 +1,6 @@
 import Semantics.FAMM
 import Semantics.FixedPoint
+import Semantics.FixedPointBoundary

 open Semantics
 open Semantics.FixedPoint (Q16_16)
--- a/0-Core-Formalism/lean/Semantics/Semantics/EfficiencyAnalysis.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/EfficiencyAnalysis.lean
@ -1,4 +1,5 @@
 import Semantics.FixedPoint
+import Semantics.FixedPointBoundary
 import Lean.Data.Json

 namespace Semantics.EfficiencyAnalysis
--- a/0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean
@ -22,6 +22,35 @@ This removes the old proof debt caused by proving signed arithmetic facts direct
 against modular UInt32/UInt64 overflow behavior.
 -/

+-- ═══════════════════════════════════════════════════════════════════════════
+-- Shared integer helpers (Float-free)
+-- ═══════════════════════════════════════════════════════════════════════════
+
+/-- Floor of log₂ for natural numbers. Returns 0 for n = 0. -/
+private def natLog2 (n : Nat) : Nat :=
+  if n = 0 then 0
+  else
+    let rec loop (x : Nat) (acc : Nat) (fuel : Nat) : Nat :=
+      match fuel with
+      | 0 => acc
+      | f + 1 =>
+        match x with
+        | 0 => acc
+        | _ => loop (x >>> 1) (acc + 1) f
+    loop (n >>> 1) 0 64
+
+/-- Integer square root via Newton's method. Returns floor(√n). -/
+private def intSqrt (n : Int) : Int :=
+  if n ≤ 0 then 0
+  else
+    let rec loop (x : Int) (fuel : Nat) : Int :=
+      match fuel with
+      | 0     => x
+      | f + 1 =>
+        let x' := (x + n / x) / 2
+        if x' ≥ x then x else loop x' f
+    loop (n / 2 + 1) 64
+
 -- ═══════════════════════════════════════════════════════════════════════════
 -- Q0.16 signed normalized fraction
 -- ═══════════════════════════════════════════════════════════════════════════
@ -97,23 +126,14 @@ def le (a b : Q0_16) : Bool := a.toInt ≤ b.toInt
 def gt (a b : Q0_16) : Bool := b.toInt < a.toInt
 def ge (a b : Q0_16) : Bool := b.toInt ≤ a.toInt

-def toFloat (q : Q0_16) : Float :=
-  Float.ofInt q.toInt / 32767.0
-
-def ofFloat (f : Float) : Q0_16 :=
-  if f.isNaN then zero
-  else if f ≥ 1.0 then one
-  else if f ≤ -1.0 then neg one
-  else if f < 0.0 then
-    ofRawInt (-(Int.ofNat ((-f * 32767.0).round.toUInt16.toNat)))
-  else
-    ofRawInt (Int.ofNat ((f * 32767.0).round.toUInt16.toNat))
-
 def log2 (q : Q0_16) : Q0_16 :=
-  if q.toInt = 0 then zero
+  if q.toInt ≤ 0 then zero
  else
-    let f := toFloat q
-    if f ≤ 0.0 then zero else ofFloat (Float.log2 f)
+    let rawNat := q.toInt.toNat
+    let k := natLog2 rawNat
+    let mQ16 : Int := (q.toInt * 32767) / ((1 : Int) <<< k)
+    let fracPart := ((mQ16 - 32767) * 47274) / 32767
+    ofRawInt ((k : Int) * 32767 - 15 * 32767 + fracPart)

 def min (a b : Q0_16) : Q0_16 :=
  if a.toInt ≤ b.toInt then a else b
@ -288,45 +308,44 @@ def neg (q : Q16_16) : Q16_16 := ofRawInt (-q.toInt)
@[inline]
 def abs (q : Q16_16) : Q16_16 := if q.toInt < 0 then neg q else q

-@[inline]
-def ofFloat (f : Float) : Q16_16 :=
-  if f.isNaN || f ≥ 32768.0 then infinity
-  else if f ≤ -32768.0 then minVal
-  else if f < 0.0 then
-    ofRawInt (-(Int.ofNat ((-f * 65536.0).floor.toUInt32.toNat)))
-  else
-    ofRawInt (Int.ofNat ((f * 65536.0).floor.toUInt32.toNat))
-
-@[inline]
-def toFloat (q : Q16_16) : Float :=
-  Float.ofInt q.toInt / 65536.0
-
+/-- Q16.16 square root via integer Newton's method.
+    Computes floor(√(q.raw × 65536)) which is the Q16.16
+    representation of √(q.raw/65536). -/
@[inline]
 def sqrt (q : Q16_16) : Q16_16 :=
-  if q.toInt = 0 then zero
-  else
-    let f := toFloat q
-    if f ≤ 0.0 then zero else ofFloat (Float.sqrt f)
-
-/-- Natural logarithm approximation around 1.0. -/
-def ln (q : Q16_16) : Q16_16 :=
-  let x := q.toInt
-  if x ≤ 0 then zero
-  else
-    let y := x - q16Scale
-    let y2 := (y * y) / q16Scale
-    let y3 := (y * y2) / q16Scale
-    ofRawInt (y - y2 / 2 + y3 / 3)
+  if q.toInt ≤ 0 then zero
+  else ofRawInt (intSqrt (q.toInt * q16Scale))

+/-- Q16.16 log₂ via bit extraction + linear interpolation.
+    log2(q.raw/65536) = log2(q.raw) − 16.
+    Integer part from bit position; fractional part approximated
+    via (m−1)/ln(2) where m = q.raw/2^k ∈ [1,2). -/
 def log2 (q : Q16_16) : Q16_16 :=
-  let ln2 : Q16_16 := ofRawInt 45426
-  div (ln q) ln2
+  if q.toInt ≤ 0 then zero
+  else
+    let rawNat := q.toInt.toNat
+    let k := natLog2 rawNat
+    let mQ16 : Int := (q.toInt * q16Scale) / ((1 : Int) <<< k)
+    let fracPart := ((mQ16 - q16Scale) * 94548) / q16Scale
+    ofRawInt ((k : Int) * q16Scale - 16 * q16Scale + fracPart)

+/-- Piecewise-linear approximation to exp(−x) for x ≥ 0 in Q16.16.
+    7-segment linear interpolation. Maximum error ~0.02. -/
 def expNeg (x : Q16_16) : Q16_16 :=
-  if x.toInt ≥ 0x00030000 then zero
-  else if x.toInt ≥ 0x00020000 then ofRawInt 0x00004D29
-  else if x.toInt ≥ 0x00010000 then ofRawInt 0x0000C5C0
-  else ofRawInt 0x0001C5C0
+  if x.toInt ≤ 0 then one
+  else if x.toInt ≥ 3 * q16Scale then zero
+  else
+    let rawX := x.toInt
+    if rawX < q16Scale / 2 then
+      ofRawInt (q16Scale - (rawX * 51595) / q16Scale)
+    else if rawX < q16Scale then
+      ofRawInt (44067 - (rawX * 32768) / q16Scale)
+    else if rawX < 3 * q16Scale / 2 then
+      ofRawInt (26690 - (rawX * 15401) / q16Scale)
+    else if rawX < 2 * q16Scale then
+      ofRawInt (16515 - (rawX * 8585) / q16Scale)
+    else
+      ofRawInt (9699 - (rawX * 4129) / q16Scale)

 instance : Add Q16_16 := ⟨add⟩
 instance : Sub Q16_16 := ⟨sub⟩
@ -811,8 +830,6 @@ def q0_64MinRaw : Int := -9223372036854775808
 def q0_64MaxRaw : Int := 9223372036854775807
 def q0_64ScaleNat : Nat := 9223372036854775808

-def q0_64ScaleFloat : Float := 9223372036854775808.0
-
 /--
 Q0.64 pure fraction representation.
 The canonical proof model stores the signed raw integer in the Int64 range.
@ -877,17 +894,6 @@ def div (a b : Q0_64) : Q0_64 :=
  else ofRawInt ((a.toInt * Int.ofNat q0_64ScaleNat) / b.toInt)
 def abs (x : Q0_64) : Q0_64 := if x.toInt < 0 then neg x else x

-def ofFloat (f : Float) : Q0_64 :=
-  if f.isNaN || f ≥ 1.0 then one
-  else if f ≤ -1.0 then ofRawInt q0_64MinRaw
-  else if f < 0.0 then
-    ofRawInt (-(Int.ofNat ((-f * q0_64ScaleFloat).floor.toUInt64.toNat)))
-  else
-    ofRawInt (Int.ofNat ((f * q0_64ScaleFloat).floor.toUInt64.toNat))
-
-def toFloat (q : Q0_64) : Float :=
-  Float.ofInt q.toInt / q0_64ScaleFloat
-
 instance : Add Q0_64 := ⟨add⟩
 instance : Sub Q0_64 := ⟨sub⟩
 instance : Mul Q0_64 := ⟨mul⟩
@ -930,9 +936,7 @@ theorem piPandigitalCorrect : (piPandigital.toInt - piDirect.toInt).natAbs ≤ 1
 def spaceAnalysis : String :=
  "Pandigital pi: 6 bytes packed vs 4 bytes direct Q16.16 (trade-off for mathematical elegance)"

-#eval piPandigital.toFloat
-#eval piDirect.toFloat
-#eval (piPandigital.toInt - piDirect.toInt).natAbs
+#eval (piPandigital.toInt - piDirect.toInt).natAbs  -- expect: 0

 end PandigitalPi

@ -943,7 +947,7 @@ namespace Semantics
  namespace Q16_16
    export FixedPoint.Q16_16
      (zero one negOne epsilon two infinity maxVal minVal ofNat satFromNat ofRatio toInt
-       ofRawInt ofBits toBits ofFloat toFloat scale ofInt add sub mul div abs neg sqrt ln log2
+       ofRawInt ofBits toBits scale ofInt add sub mul div abs neg sqrt log2
       expNeg sat01 max min le ge gt lt recip ofRaw clip isNeg zero_mul mul_zero one_mul
       mul_one zero_add add_zero sub_self zero_toInt one_toInt epsilon_toInt
       epsilon_toInt_pos toInt_eq_zero_iff epsilon_add_pos zero_div mul_self_nonneg
@ -951,10 +955,10 @@ namespace Semantics
       toInt_nonneg_le_maxVal add_pos_of_pos)
  end Q16_16
  namespace Q0_16
-    export FixedPoint.Q0_16 (zero one half neg add sub mul div abs lt le gt ge toFloat ofFloat log2 min)
+    export FixedPoint.Q0_16 (zero one half neg add sub mul div abs lt le gt ge log2 min)
  end Q0_16
  namespace Q0_64
-    export FixedPoint.Q0_64 (one zero ofRatio half neg add sub mul div abs toInt ofFloat toFloat)
+    export FixedPoint.Q0_64 (one zero ofRatio half neg add sub mul div abs toInt)
  end Q0_64
  namespace PandigitalPi
    export FixedPoint.PandigitalPi (highTerm lowTerm piPandigital piDirect piPandigitalCorrect spaceAnalysis)
--- a/0-Core-Formalism/lean/Semantics/Semantics/FixedPointBoundary.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/FixedPointBoundary.lean
@ -0,0 +1,89 @@
+import Semantics.FixedPoint
+
+/-!
+# FixedPointBoundary — Float ↔ Q16_16 / Q0_16 / Q0_64 conversion
+
+These functions are **only** for the I/O boundary: parsing JSON, reading sensor
+data, or displaying values in `#eval` witnesses. They must NOT be used in any
+compute-path definition that feeds into a receipt, score, or gate.
+
+The core `Semantics.FixedPoint` module is Float-free by design.
+-/
+
+namespace Semantics.FixedPoint
+
+-- ═══════════════════════════════════════════════════════════════════════════
+-- Q0.16 Float boundary
+-- ═══════════════════════════════════════════════════════════════════════════
+
+namespace Q0_16
+
+def toFloat (q : Q0_16) : Float :=
+  Float.ofInt q.toInt / 32767.0
+
+def ofFloat (f : Float) : Q0_16 :=
+  if f.isNaN then zero
+  else if f ≥ 1.0 then one
+  else if f ≤ -1.0 then neg one
+  else if f < 0.0 then
+    ofRawInt (-(Int.ofNat ((-f * 32767.0).round.toUInt16.toNat)))
+  else
+    ofRawInt (Int.ofNat ((f * 32767.0).round.toUInt16.toNat))
+
+end Q0_16
+
+-- ═══════════════════════════════════════════════════════════════════════════
+-- Q16.16 Float boundary
+-- ═══════════════════════════════════════════════════════════════════════════
+
+namespace Q16_16
+
+@[inline]
+def ofFloat (f : Float) : Q16_16 :=
+  if f.isNaN || f ≥ 32768.0 then infinity
+  else if f ≤ -32768.0 then minVal
+  else if f < 0.0 then
+    ofRawInt (-(Int.ofNat ((-f * 65536.0).floor.toUInt32.toNat)))
+  else
+    ofRawInt (Int.ofNat ((f * 65536.0).floor.toUInt32.toNat))
+
+@[inline]
+def toFloat (q : Q16_16) : Float :=
+  Float.ofInt q.toInt / 65536.0
+
+end Q16_16
+
+-- ═══════════════════════════════════════════════════════════════════════════
+-- Q0.64 Float boundary
+-- ═══════════════════════════════════════════════════════════════════════════
+
+def q0_64ScaleFloat : Float := 9223372036854775808.0
+
+namespace Q0_64
+
+def ofFloat (f : Float) : Q0_64 :=
+  if f.isNaN || f ≥ 1.0 then one
+  else if f ≤ -1.0 then ofRawInt q0_64MinRaw
+  else if f < 0.0 then
+    ofRawInt (-(Int.ofNat ((-f * q0_64ScaleFloat).floor.toUInt64.toNat)))
+  else
+    ofRawInt (Int.ofNat ((f * q0_64ScaleFloat).floor.toUInt64.toNat))
+
+def toFloat (q : Q0_64) : Float :=
+  Float.ofInt q.toInt / q0_64ScaleFloat
+
+end Q0_64
+
+end Semantics.FixedPoint
+
+namespace Semantics
+  namespace Q16_16
+    export FixedPoint.Q16_16 (ofFloat toFloat)
+  end Q16_16
+  namespace Q0_16
+    export FixedPoint.Q0_16 (toFloat ofFloat)
+  end Q0_16
+  namespace Q0_64
+    export FixedPoint.Q0_64 (ofFloat toFloat)
+  end Q0_64
+end Semantics
--- a/0-Core-Formalism/lean/Semantics/Semantics/Functions/BracketedCalculus.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/Functions/BracketedCalculus.lean
@ -3,6 +3,7 @@
 -/

 import Semantics.FixedPoint
+import Semantics.FixedPointBoundary

 namespace Semantics.BracketedCalculus

--- a/0-Core-Formalism/lean/Semantics/Semantics/FuzzyAssociation.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/FuzzyAssociation.lean
@ -1,4 +1,5 @@
 import Semantics.FixedPoint
+import Semantics.FixedPointBoundary
 import Semantics.Bind

 namespace Semantics.FuzzyAssociation
--- a/0-Core-Formalism/lean/Semantics/Semantics/LawfulLoss.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/LawfulLoss.lean
@ -16,6 +16,7 @@
 -/

 import Semantics.FixedPoint
+import Semantics.FixedPointBoundary

 namespace Semantics.LawfulLoss

--- a/0-Core-Formalism/lean/Semantics/Semantics/LocalDerivative.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/LocalDerivative.lean
@ -14,6 +14,7 @@
 -/

 import Semantics.FixedPoint
+import Semantics.FixedPointBoundary

 set_option linter.dupNamespace false

--- a/0-Core-Formalism/lean/Semantics/Semantics/NUVMATH.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/NUVMATH.lean
@ -8,6 +8,7 @@ Fixed-point orthogonal projection structure for spectral addressing.
 -/

 import Semantics.FixedPoint
+import Semantics.FixedPointBoundary
 import Semantics.S3C
 import Mathlib.Tactic.Ring

--- a/0-Core-Formalism/lean/Semantics/Semantics/ProvenanceSource.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/ProvenanceSource.lean
@ -1,4 +1,5 @@
 import Semantics.Bind
+import Semantics.FixedPointBoundary

 namespace Semantics.ProvenanceSource

--- a/0-Core-Formalism/lean/Semantics/Semantics/Q16_16Numerics.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/Q16_16Numerics.lean
@ -23,6 +23,7 @@ Part of the OTOM TreeDIAT/PIST family.
 -/

 import Semantics.FixedPoint
+import Semantics.FixedPointBoundary

 namespace Semantics.Q16_16Numerics

--- a/0-Core-Formalism/lean/Semantics/Semantics/QFactor.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/QFactor.lean
@ -1,4 +1,5 @@
 import Semantics.FixedPoint
+import Semantics.FixedPointBoundary

 namespace Semantics.QFactor

--- a/0-Core-Formalism/lean/Semantics/Semantics/SLUG3.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/SLUG3.lean
@ -13,6 +13,7 @@ Lean is the source of truth.
 -/

 import Semantics.FixedPoint
+import Semantics.FixedPointBoundary

 namespace Semantics.SLUG3

--- a/0-Core-Formalism/lean/Semantics/Semantics/SubagentOrchestrator.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/SubagentOrchestrator.lean
@ -30,6 +30,7 @@ import Semantics.RcloneIntegration
 import Semantics.GpuDutyAssignment
 import Semantics.DomainModelIntegration
 import Semantics.FixedPoint
+import Semantics.FixedPointBoundary

 namespace Semantics.SubagentOrchestrator

--- a/0-Core-Formalism/lean/Semantics/Semantics/Tape.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/Tape.lean
@ -1,4 +1,5 @@
 import Semantics.FixedPoint
+import Semantics.FixedPointBoundary

 namespace Semantics.Tape