diff --git a/lean4/Sunbeam/Model/DecisionTree.lean b/lean4/Sunbeam/Model/DecisionTree.lean
index 81fb421..0b49191 100644
--- a/lean4/Sunbeam/Model/DecisionTree.lean
+++ b/lean4/Sunbeam/Model/DecisionTree.lean
@@ -2,13 +2,23 @@ import Sunbeam.Model.Basic
 
 namespace Sunbeam
 
-/-- A decision tree node (inductive = automatic termination for structural recursion). -/
+/-- A decision tree node (inductive = automatic termination for structural recursion).
+
+This is an abstract specification of the Rust packed-array representation:
+  `type PackedNode = (u8, f32, u16, u16)` — `(feature_index, threshold, left, right)`
+Leaf nodes in Rust use `feature_index = 255`; the threshold encodes the decision:
+  `< 0.25` → Allow, `> 0.75` → Block, otherwise → Defer.
+Here we use an inductive type so that structural recursion gives automatic termination. -/
 inductive TreeNode where
   | leaf (decision : Decision) : TreeNode
   | split (featureIdx : Nat) (threshold : Float) (left right : TreeNode) : TreeNode
   deriving Repr
 
-/-- Tree prediction by structural recursion (termination is automatic). -/
+/-- Tree prediction by structural recursion (termination is automatic).
+
+Corresponds to `ensemble::tree::tree_predict` in Rust, which loops over a flat
+packed-node array. The semantic behavior is identical: split nodes compare
+`input[featureIdx]` against `threshold` and branch left/right. -/
 def treePredictAux {n : Nat} (input : Fin n → Float) : TreeNode → Decision
   | .leaf d => d
   | .split idx thr left right =>
diff --git a/lean4/Sunbeam/Model/MLP.lean b/lean4/Sunbeam/Model/MLP.lean
index 534a564..872e299 100644
--- a/lean4/Sunbeam/Model/MLP.lean
+++ b/lean4/Sunbeam/Model/MLP.lean
@@ -4,7 +4,11 @@ import Sunbeam.Model.ReLU
 
 namespace Sunbeam
 
-/-- Weights for a 2-layer MLP (input → hidden → scalar output). -/
+/-- Weights for a 2-layer MLP (input → hidden → scalar output).
+
+Corresponds to `ensemble::mlp::mlp_predict_32` in Rust, which uses const generic
+`INPUT` and a fixed hidden dimension of 32. Here `hiddenDim` is a parameter so
+structural properties can be proved generically. -/
 structure MLPWeights (inputDim hiddenDim : Nat) where
   w1 : Fin hiddenDim → FloatVec inputDim
   b1 : FloatVec hiddenDim
diff --git a/lean4/Sunbeam/Model/Sigmoid.lean b/lean4/Sunbeam/Model/Sigmoid.lean
index eda8f09..8c7d72a 100644
--- a/lean4/Sunbeam/Model/Sigmoid.lean
+++ b/lean4/Sunbeam/Model/Sigmoid.lean
@@ -13,8 +13,8 @@ float inputs. They cannot be proved inside Lean because `Float` operations are
 `@[extern]` (opaque to the kernel). The axioms form a documented trust boundary:
 we trust the C runtime's `exp` implementation.
 
-When TorchLean ships its verified Float32 kernel, these axioms can be replaced
-with proofs against that kernel.
+When TorchLean (arXiv:2602.22631) ships its verified Float32 kernel, these
+axioms can be replaced with proofs against that kernel.
 -/
 
 /-- Sigmoid output is always positive: exp(-x) ≥ 0 ⟹ 1+exp(-x) ≥ 1 ⟹ 1/(1+exp(-x)) > 0. -/