diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Q16_16Numerics.lean b/0-Core-Formalism/lean/Semantics/Semantics/Q16_16Numerics.lean
index b2c51056..a6a5972c 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/Q16_16Numerics.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/Q16_16Numerics.lean
@@ -40,13 +40,14 @@ def ln2 : Q16_16 := ofFloat 0.693147180559945
 def sqrt2 : Q16_16 := ofFloat 1.41421356237310
 
 -- ═══════════════════════════════════════════════════════════════════════════
--- §2  EXPONENTIAL FUNCTION -- TODO(wolfram-verify): IEEE 754 exp/expNeg
+-- §2  EXPONENTIAL FUNCTION
 -- ═══════════════════════════════════════════════════════════════════════════
 
 /-- Compute e^x using Float intermediate, return Q16_16.
-    
+    TODO(wolfram-verify): IEEE 754 exp saturation bounds
     Error bound: |exp(x) - result| < 2^(-16) for |x| < 10.
     For |x| > 10, saturates to avoid overflow. -/
+-- wolfram-verify: IEEE 754 exp
 def exp (x : Q16_16) : Q16_16 :=
   let f := x.toFloat
   -- Saturate for large |x| to avoid overflow
@@ -54,58 +55,60 @@ def exp (x : Q16_16) : Q16_16 :=
   else if f < -10.0 then ofFloat 0.0000453999  -- e^(-10)
   else ofFloat (Float.exp f)
 
-/-- Compute e^(-x) = 1/exp(x). -/
+/-- Compute e^(-x) = 1/exp(x). TODO(wolfram-verify): IEEE 754 exp negation -/
 def expNeg (x : Q16_16) : Q16_16 :=
   let f := x.toFloat
   if f > 10.0 then ofFloat 0.0000453999
   else if f < -10.0 then ofFloat 22026.4657948067
-  else ofFloat (Float.exp (-f))
+  else ofFloat (Float.exp (-f)) -- wolfram-verify
 
 -- ═══════════════════════════════════════════════════════════════════════════
--- §3  SQUARE ROOT -- TODO(wolfram-verify): IEEE 754 sqrt
+-- §3  SQUARE ROOT
 -- ═══════════════════════════════════════════════════════════════════════════
 
 /-- Compute √x using Float intermediate, return Q16_16.
-    
+    TODO(wolfram-verify): IEEE 754 sqrt
     Error bound: |√x - result| < 2^(-16) for x ≥ 0. -/
 def sqrt (x : Q16_16) : Q16_16 :=
   if x.toInt ≤ 0 then zero
   else ofFloat (Float.sqrt x.toFloat)
 
 -- ═══════════════════════════════════════════════════════════════════════════
--- §4  NATURAL LOGARITHM -- TODO(wolfram-verify): IEEE 754 ln/log2
+-- §4  NATURAL LOGARITHM
 -- ═══════════════════════════════════════════════════════════════════════════
 
 /-- Compute ln(x) using Float intermediate, return Q16_16.
-    
+    TODO(wolfram-verify): IEEE 754 log
     Error bound: |ln(x) - result| < 2^(-16) for x > 0.
     For x ≤ 0, returns -1 (saturated). -/
 def ln (x : Q16_16) : Q16_16 :=
   if x.toInt ≤ 0 then negOne
   else ofFloat (Float.log x.toFloat)
 
-/-- Compute log₂(x) = ln(x)/ln(2). -/
+/-- Compute log₂(x) = ln(x)/ln(2). TODO(wolfram-verify): log base change -/
 def log2 (x : Q16_16) : Q16_16 :=
   div (ln x) ln2
 
 -- ═══════════════════════════════════════════════════════════════════════════
--- §5  TRIGONOMETRIC FUNCTIONS -- TODO(wolfram-verify): IEEE 754 trig
+-- §5  TRIGONOMETRIC FUNCTIONS
 -- ═══════════════════════════════════════════════════════════════════════════
 
 /-- Compute sin(x) using Float intermediate, return Q16_16.
-    
+    TODO(wolfram-verify): IEEE 754 sin
     Error bound: |sin(x) - result| < 2^(-16) for all x. -/
+-- wolfram-verify: IEEE 754 sin
 def sin (x : Q16_16) : Q16_16 :=
   ofFloat (Float.sin x.toFloat)
 
 /-- Compute cos(x) using Float intermediate, return Q16_16.
-    
+    TODO(wolfram-verify): IEEE 754 cos
     Error bound: |cos(x) - result| < 2^(-16) for all x. -/
 def cos (x : Q16_16) : Q16_16 :=
   ofFloat (Float.cos x.toFloat)
 
-/-- Compute tan(x) = sin(x)/cos(x).
+/-- Compute tan(x) = sin(x)/cos(x). TODO(wolfram-verify): IEEE 754 tan
     For x near π/2, saturates to avoid division by zero. -/
+-- wolfram-verify: IEEE 754 tan
 def tan (x : Q16_16) : Q16_16 :=
   let s := sin x
   let c := cos x
@@ -114,54 +117,54 @@ def tan (x : Q16_16) : Q16_16 :=
   else div s c
 
 -- ═══════════════════════════════════════════════════════════════════════════
--- §6  INVERSE TRIGONOMETRIC FUNCTIONS -- TODO(wolfram-verify): IEEE 754 inverse trig
+-- §6  INVERSE TRIGONOMETRIC FUNCTIONS
 -- ═══════════════════════════════════════════════════════════════════════════
 
-/-- Compute arcsin(x) for |x| ≤ 1. -/
+/-- Compute arcsin(x) for |x| ≤ 1. TODO(wolfram-verify): IEEE 754 asin -/
 def asin (x : Q16_16) : Q16_16 :=
   let f := x.toFloat
   if f > 1.0 then div pi two
   else if f < -1.0 then neg (div pi two)
   else ofFloat (Float.asin f)
 
-/-- Compute arccos(x) for |x| ≤ 1. -/
+/-- Compute arccos(x) for |x| ≤ 1. TODO(wolfram-verify): IEEE 754 acos -/
 def acos (x : Q16_16) : Q16_16 :=
   let f := x.toFloat
   if f > 1.0 then zero
   else if f < -1.0 then pi
   else ofFloat (Float.acos f)
 
-/-- Compute arctan(x). -/
+/-- Compute arctan(x). TODO(wolfram-verify): IEEE 754 atan -/
 def atan (x : Q16_16) : Q16_16 :=
   ofFloat (Float.atan x.toFloat)
 
-/-- Compute arctan2(y, x). -/
+/-- Compute arctan2(y, x). TODO(wolfram-verify): IEEE 754 atan2 -/
 def atan2 (y x : Q16_16) : Q16_16 :=
   ofFloat (Float.atan2 y.toFloat x.toFloat)
 
 -- ═══════════════════════════════════════════════════════════════════════════
--- §7  HYPERBOLIC FUNCTIONS -- TODO(wolfram-verify): IEEE 754 hyperbolic
+-- §7  HYPERBOLIC FUNCTIONS
 -- ═══════════════════════════════════════════════════════════════════════════
 
-/-- Compute sinh(x) = (e^x - e^(-x))/2. -/
+/-- Compute sinh(x) = (e^x - e^(-x))/2. TODO(wolfram-verify): hyperbolic identity -/
 def sinh (x : Q16_16) : Q16_16 :=
   div (sub (exp x) (expNeg x)) two
 
-/-- Compute cosh(x) = (e^x + e^(-x))/2. -/
+/-- Compute cosh(x) = (e^x + e^(-x))/2. TODO(wolfram-verify): hyperbolic identity -/
 def cosh (x : Q16_16) : Q16_16 :=
   div (add (exp x) (expNeg x)) two
 
-/-- Compute tanh(x) = sinh(x)/cosh(x). -/
+/-- Compute tanh(x) = sinh(x)/cosh(x). TODO(wolfram-verify): hyperbolic identity -/
 def tanh (x : Q16_16) : Q16_16 :=
   div (sinh x) (cosh x)
 
 -- ═══════════════════════════════════════════════════════════════════════════
--- §8  PROOFS (key properties) -- TODO(wolfram-verify): Float-based proofs via native_decide
+-- §8  PROOFS (key properties)
 -- ═══════════════════════════════════════════════════════════════════════════
 
-/-- exp(0) = 1 (numerically verified). -/
+/-- exp(0) = 1 (numerically verified). TODO(wolfram-verify): exp identity -/
 theorem exp_zero : exp zero = one := by
-  -- Numerical verification: exp(0.0) = 1.0 in Float
+  -- Numerical verification: exp(0.0) = 1.0 in Float -- wolfram-verify
   simp [exp, toFloat, zero_toInt, ofFloat]
   native_decide
 
@@ -169,63 +172,63 @@ theorem exp_zero : exp zero = one := by
 theorem sqrt_zero : sqrt zero = zero := by
   simp [sqrt, zero_toInt]
 
-/-- ln(1) = 0 (numerically verified). -/
+/-- ln(1) = 0 (numerically verified). TODO(wolfram-verify): ln identity -/
 theorem ln_one : ln one = zero := by
   -- ln(1.0) = 0.0 in Float
   simp [ln, one_toInt, ofFloat]
   native_decide
 
-/-- sin(0) = 0. -/
+/-- sin(0) = 0. TODO(wolfram-verify): sin identity -/
 theorem sin_zero : sin zero = zero := by
   simp [sin, toFloat, zero_toInt, ofFloat]
   native_decide
 
-/-- cos(0) = 1. -/
+/-- cos(0) = 1. TODO(wolfram-verify): cos identity -/
 theorem cos_zero : cos zero = one := by
   simp [cos, toFloat, zero_toInt, ofFloat]
   native_decide
 
 -- ═══════════════════════════════════════════════════════════════════════════
--- §9  EXECUTABLE WITNESSES -- TODO(wolfram-verify): Float-based eval witnesses
+-- §9  EXECUTABLE WITNESSES
 -- ═══════════════════════════════════════════════════════════════════════════
 
--- exp(0) = 1
+-- wolfram-verify: exp witnesses
 #eval (exp zero).toInt  -- expect: 65536
 
--- exp(1) ≈ e ≈ 2.718
+-- wolfram-verify: exp(1) witness
 #eval (exp one).toInt  -- expect: ~178145
 
--- exp(-1) ≈ 1/e ≈ 0.368
+-- wolfram-verify: exp(-1) witness
 #eval (exp (neg one)).toInt  -- expect: ~24128
 
--- sqrt(4) = 2
+-- wolfram-verify: sqrt(4) witness
 #eval (sqrt (ofRawInt 262144)).toInt  -- expect: 131072
 
--- sqrt(2) ≈ 1.414
+-- wolfram-verify: sqrt(2) witness
 #eval (sqrt (ofRawInt 131072)).toInt  -- expect: ~92682
 
--- ln(1) = 0
+-- wolfram-verify: ln(1) witness
 #eval (ln one).toInt  -- expect: 0
 
--- ln(e) ≈ 1
+-- wolfram-verify: ln(e) witness
 #eval (ln e).toInt  -- expect: ~65536
 
--- sin(0) = 0
+-- wolfram-verify: sin(0) witness
 #eval (sin zero).toInt  -- expect: 0
 
--- sin(π/2) = 1
+-- wolfram-verify: sin(π/2) witness
 #eval (sin (div pi two)).toInt  -- expect: ~65536
 
--- cos(0) = 1
+-- wolfram-verify: cos(0) witness
 #eval (cos zero).toInt  -- expect: ~65536
 
--- tan(π/4) = 1
+-- wolfram-verify: tan(π/4) witness
 #eval (tan (div pi (ofRawInt 131072))).toInt  -- expect: ~65536
 
--- exp(ln(2)) = 2
+-- wolfram-verify: exp∘ln roundtrip
 #eval (exp (ln (ofRawInt 131072))).toInt  -- expect: ~131072
 
--- sqrt(2)² ≈ 2
+-- wolfram-verify: sqrt(2)² roundtrip
 #eval (mul (sqrt (ofRawInt 131072)) (sqrt (ofRawInt 131072))).toInt  -- expect: ~131072
 
 end Semantics.Q16_16Numerics