diff --git a/0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean b/0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean
index b498f515..ca18bc88 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean
@@ -55,6 +55,7 @@ private def intSqrt (n : Int) : Int :=
 -- Q0.16 signed normalized fraction
 -- ═══════════════════════════════════════════════════════════════════════════
 
+-- TODO(wolfram-verify): standard Q0.16 fixed-point scale constants
 def q0_16MinRaw : Int := -32768
 def q0_16MaxRaw : Int := 32767
 def q0_16Scale  : Int := 32767
@@ -330,7 +331,8 @@ def log2 (q : Q16_16) : Q16_16 :=
     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. -/
+    7-segment linear interpolation. Maximum error ~0.02.
+    TODO(wolfram-verify): coefficients derived from exp(-x) endpoint matching -/
 def expNeg (x : Q16_16) : Q16_16 :=
   if x.toInt ≤ 0 then one
   else if x.toInt ≥ 3 * q16Scale then zero
@@ -823,7 +825,7 @@ theorem abs_triangle (a b : Q16_16) :
 end Q16_16
 
 -- ═══════════════════════════════════════════════════════════════════════════
--- Q0.64 signed normalized fraction
+-- Q0.64 signed normalized fraction -- TODO(wolfram-verify): standard Q0.64 range constants
 -- ═══════════════════════════════════════════════════════════════════════════
 
 def q0_64MinRaw : Int := -9223372036854775808
diff --git a/0-Core-Formalism/lean/Semantics/Semantics/LawfulLoss.lean b/0-Core-Formalism/lean/Semantics/Semantics/LawfulLoss.lean
index e1c3d6fe..826d239f 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/LawfulLoss.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/LawfulLoss.lean
@@ -5,7 +5,7 @@
 
   Every translation yields a `BindResult` recording:
     - lawful : Bool   — did invariants survive?
-    - cost   : Q0_16  — dimensional mismatch penalty (normalized)
+    - cost   : Q0_16  — dimensional mismatch penalty (normalized) -- TODO(wolfram-verify): Q0_16 arithmetic
     - witness : String — what was sacrificed (human-readable trace)
 
   Substrate-agnostic: no runtime dependencies, no Float, no IO.
@@ -69,7 +69,7 @@ def mkUnlawful (witness : String) (klass : BindClass) : BindResult :=
 /-- Predicate: is the translation lawful? -/
 def isLawful (r : BindResult) : Bool := r.lawful
 
-/-- Extract normalized cost. -/
+/-- Extract normalized cost. -- TODO(wolfram-verify): identity projection -/
 def bindCost (r : BindResult) : Q0_16 := r.cost
 
 /-- Extract witness string. -/
diff --git a/0-Core-Formalism/lean/Semantics/Semantics/NUVMATH.lean b/0-Core-Formalism/lean/Semantics/Semantics/NUVMATH.lean
index 2e1e75bb..5cbeb8ab 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/NUVMATH.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/NUVMATH.lean
@@ -148,7 +148,8 @@ def defaultGovernorConfig : S3CGovernorConfig :=
     maxRetries := 8 }
 
 /-- Scale `dt` by the normalized S3C J-score. High J near a throat permits
-    larger steps; low J near a boundary throttles the solver. -/
+    larger steps; low J near a boundary throttles the solver.
+    TODO(wolfram-verify): geometric dt scaling formula -/
 def geometricDt (audit : S3CAudit) (baseDt : Q16_16) (jMax : Nat) : Q16_16 :=
   if audit.emit then
     if jMax = 0 then
diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Q16_16Numerics.lean b/0-Core-Formalism/lean/Semantics/Semantics/Q16_16Numerics.lean
index cae37719..b2c51056 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/Q16_16Numerics.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/Q16_16Numerics.lean
@@ -31,7 +31,7 @@ open Semantics.FixedPoint
 open Semantics.Q16_16
 
 -- ═══════════════════════════════════════════════════════════════════════════
--- §1  CONSTANTS
+-- §1  CONSTANTS -- TODO(wolfram-verify): standard mathematical constants
 -- ═══════════════════════════════════════════════════════════════════════════
 
 def pi : Q16_16 := ofFloat 3.14159265358979
@@ -40,7 +40,7 @@ def ln2 : Q16_16 := ofFloat 0.693147180559945
 def sqrt2 : Q16_16 := ofFloat 1.41421356237310
 
 -- ═══════════════════════════════════════════════════════════════════════════
--- §2  EXPONENTIAL FUNCTION
+-- §2  EXPONENTIAL FUNCTION -- TODO(wolfram-verify): IEEE 754 exp/expNeg
 -- ═══════════════════════════════════════════════════════════════════════════
 
 /-- Compute e^x using Float intermediate, return Q16_16.
@@ -62,7 +62,7 @@ def expNeg (x : Q16_16) : Q16_16 :=
   else ofFloat (Float.exp (-f))
 
 -- ═══════════════════════════════════════════════════════════════════════════
--- §3  SQUARE ROOT
+-- §3  SQUARE ROOT -- TODO(wolfram-verify): IEEE 754 sqrt
 -- ═══════════════════════════════════════════════════════════════════════════
 
 /-- Compute √x using Float intermediate, return Q16_16.
@@ -73,7 +73,7 @@ def sqrt (x : Q16_16) : Q16_16 :=
   else ofFloat (Float.sqrt x.toFloat)
 
 -- ═══════════════════════════════════════════════════════════════════════════
--- §4  NATURAL LOGARITHM
+-- §4  NATURAL LOGARITHM -- TODO(wolfram-verify): IEEE 754 ln/log2
 -- ═══════════════════════════════════════════════════════════════════════════
 
 /-- Compute ln(x) using Float intermediate, return Q16_16.
@@ -89,7 +89,7 @@ def log2 (x : Q16_16) : Q16_16 :=
   div (ln x) ln2
 
 -- ═══════════════════════════════════════════════════════════════════════════
--- §5  TRIGONOMETRIC FUNCTIONS
+-- §5  TRIGONOMETRIC FUNCTIONS -- TODO(wolfram-verify): IEEE 754 trig
 -- ═══════════════════════════════════════════════════════════════════════════
 
 /-- Compute sin(x) using Float intermediate, return Q16_16.
@@ -114,7 +114,7 @@ def tan (x : Q16_16) : Q16_16 :=
   else div s c
 
 -- ═══════════════════════════════════════════════════════════════════════════
--- §6  INVERSE TRIGONOMETRIC FUNCTIONS
+-- §6  INVERSE TRIGONOMETRIC FUNCTIONS -- TODO(wolfram-verify): IEEE 754 inverse trig
 -- ═══════════════════════════════════════════════════════════════════════════
 
 /-- Compute arcsin(x) for |x| ≤ 1. -/
@@ -140,7 +140,7 @@ def atan2 (y x : Q16_16) : Q16_16 :=
   ofFloat (Float.atan2 y.toFloat x.toFloat)
 
 -- ═══════════════════════════════════════════════════════════════════════════
--- §7  HYPERBOLIC FUNCTIONS
+-- §7  HYPERBOLIC FUNCTIONS -- TODO(wolfram-verify): IEEE 754 hyperbolic
 -- ═══════════════════════════════════════════════════════════════════════════
 
 /-- Compute sinh(x) = (e^x - e^(-x))/2. -/
@@ -156,7 +156,7 @@ def tanh (x : Q16_16) : Q16_16 :=
   div (sinh x) (cosh x)
 
 -- ═══════════════════════════════════════════════════════════════════════════
--- §8  PROOFS (key properties)
+-- §8  PROOFS (key properties) -- TODO(wolfram-verify): Float-based proofs via native_decide
 -- ═══════════════════════════════════════════════════════════════════════════
 
 /-- exp(0) = 1 (numerically verified). -/
@@ -186,7 +186,7 @@ theorem cos_zero : cos zero = one := by
   native_decide
 
 -- ═══════════════════════════════════════════════════════════════════════════
--- §9  EXECUTABLE WITNESSES
+-- §9  EXECUTABLE WITNESSES -- TODO(wolfram-verify): Float-based eval witnesses
 -- ═══════════════════════════════════════════════════════════════════════════
 
 -- exp(0) = 1
diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Tape.lean b/0-Core-Formalism/lean/Semantics/Semantics/Tape.lean
index a7f30623..a397e4f2 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/Tape.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/Tape.lean
@@ -301,7 +301,7 @@ def accountKot (tm : TapeMachine) (state : TapeState) (mode : ControlMode) : KOT
   let decision := KOTBudget.evaluateEconomics newBudget state.kotYieldProjected (1 / 10 : Rat)
   { entry with decision := decision }
 
-/-- Form a new tape state from normalized input. -/
+/-- Form a new tape state from normalized input. -- TODO(wolfram-verify): tape normalization -/
 def formState (tm : TapeMachine) (data : List UInt8) (contextType : String) : TapeState :=
   let compressed := compressStructure data
   let invariants := computeInvariants compressed