diff --git a/lean4/.gitignore b/lean4/.gitignore
new file mode 100644
index 0000000..1b861c8
--- /dev/null
+++ b/lean4/.gitignore
@@ -0,0 +1,2 @@
+.lake/build/
+.lake/config/
diff --git a/lean4/Sunbeam.lean b/lean4/Sunbeam.lean
new file mode 100644
index 0000000..3c94a12
--- /dev/null
+++ b/lean4/Sunbeam.lean
@@ -0,0 +1,7 @@
+import Sunbeam.Model.Basic
+import Sunbeam.Model.Sigmoid
+import Sunbeam.Model.ReLU
+import Sunbeam.Model.MLP
+import Sunbeam.Model.DecisionTree
+import Sunbeam.Model.Ensemble
+import Sunbeam.Verify.Structural
diff --git a/lean4/Sunbeam/Model/Basic.lean b/lean4/Sunbeam/Model/Basic.lean
new file mode 100644
index 0000000..f530449
--- /dev/null
+++ b/lean4/Sunbeam/Model/Basic.lean
@@ -0,0 +1,25 @@
+namespace Sunbeam
+
+/-- Decisions that a model component can output. -/
+inductive Decision where
+  | block : Decision
+  | allow : Decision
+  | defer : Decision
+  deriving Repr, DecidableEq
+
+/-- A fixed-size vector of floats. -/
+def FloatVec (n : Nat) := Fin n → Float
+
+/-- Dot product of two float vectors. -/
+def dot {n : Nat} (a b : FloatVec n) : Float :=
+  (List.finRange n).foldl (fun acc i => acc + a i * b i) 0.0
+
+/-- Matrix-vector product. Matrix is row-major: m rows × n cols. -/
+def matVecMul {m n : Nat} (mat : Fin m → FloatVec n) (v : FloatVec n) : FloatVec m :=
+  fun i => dot (mat i) v
+
+/-- Vector addition. -/
+def vecAdd {n : Nat} (a b : FloatVec n) : FloatVec n :=
+  fun i => a i + b i
+
+end Sunbeam
diff --git a/lean4/Sunbeam/Model/DecisionTree.lean b/lean4/Sunbeam/Model/DecisionTree.lean
new file mode 100644
index 0000000..81fb421
--- /dev/null
+++ b/lean4/Sunbeam/Model/DecisionTree.lean
@@ -0,0 +1,23 @@
+import Sunbeam.Model.Basic
+
+namespace Sunbeam
+
+/-- A decision tree node (inductive = automatic termination for structural recursion). -/
+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). -/
+def treePredictAux {n : Nat} (input : Fin n → Float) : TreeNode → Decision
+  | .leaf d => d
+  | .split idx thr left right =>
+    if h : idx < n then
+      if input ⟨idx, h⟩ ≤ thr then
+        treePredictAux input left
+      else
+        treePredictAux input right
+    else
+      Decision.defer
+
+end Sunbeam
diff --git a/lean4/Sunbeam/Model/Ensemble.lean b/lean4/Sunbeam/Model/Ensemble.lean
new file mode 100644
index 0000000..c436997
--- /dev/null
+++ b/lean4/Sunbeam/Model/Ensemble.lean
@@ -0,0 +1,42 @@
+import Sunbeam.Model.Basic
+import Sunbeam.Model.MLP
+import Sunbeam.Model.DecisionTree
+
+namespace Sunbeam
+
+/-- Ensemble: tree decides first; MLP handles only Defer cases. -/
+def ensemblePredict {inputDim hiddenDim : Nat}
+    (tree : TreeNode) (mlpWeights : MLPWeights inputDim hiddenDim)
+    (threshold : Float) (input : FloatVec inputDim) : Decision :=
+  match treePredictAux input tree with
+  | Decision.block => Decision.block
+  | Decision.allow => Decision.allow
+  | Decision.defer =>
+    let score := mlpForward mlpWeights input
+    if score > threshold then Decision.block else Decision.allow
+
+/-- If the tree says Block, the ensemble says Block. -/
+theorem tree_block_implies_ensemble_block {inputDim hiddenDim : Nat}
+    (tree : TreeNode) (mlpWeights : MLPWeights inputDim hiddenDim)
+    (threshold : Float) (input : FloatVec inputDim)
+    (h : treePredictAux input tree = Decision.block) :
+    ensemblePredict tree mlpWeights threshold input = Decision.block := by
+  unfold ensemblePredict
+  rw [h]
+
+/-- Ensemble output is always Block or Allow (never Defer). -/
+theorem ensemble_output_valid {inputDim hiddenDim : Nat}
+    (tree : TreeNode) (mlpWeights : MLPWeights inputDim hiddenDim)
+    (threshold : Float) (input : FloatVec inputDim) :
+    ensemblePredict tree mlpWeights threshold input = Decision.block ∨
+    ensemblePredict tree mlpWeights threshold input = Decision.allow := by
+  unfold ensemblePredict
+  split
+  · left; rfl
+  · right; rfl
+  · dsimp only []
+    split
+    · left; rfl
+    · right; rfl
+
+end Sunbeam
diff --git a/lean4/Sunbeam/Model/MLP.lean b/lean4/Sunbeam/Model/MLP.lean
new file mode 100644
index 0000000..534a564
--- /dev/null
+++ b/lean4/Sunbeam/Model/MLP.lean
@@ -0,0 +1,30 @@
+import Sunbeam.Model.Basic
+import Sunbeam.Model.Sigmoid
+import Sunbeam.Model.ReLU
+
+namespace Sunbeam
+
+/-- Weights for a 2-layer MLP (input → hidden → scalar output). -/
+structure MLPWeights (inputDim hiddenDim : Nat) where
+  w1 : Fin hiddenDim → FloatVec inputDim
+  b1 : FloatVec hiddenDim
+  w2 : FloatVec hiddenDim
+  b2 : Float
+
+/-- Forward pass: input → linear1 → ReLU → linear2 → sigmoid. -/
+def mlpForward {inputDim hiddenDim : Nat}
+    (weights : MLPWeights inputDim hiddenDim) (input : FloatVec inputDim) : Float :=
+  let hidden := vecAdd (matVecMul weights.w1 input) weights.b1
+  let activated := reluVec hidden
+  let output := dot weights.w2 activated + weights.b2
+  sigmoid output
+
+/-- MLP output is bounded in (0, 1) — follows directly from sigmoid bounds. -/
+theorem mlp_output_bounded {inputDim hiddenDim : Nat}
+    (weights : MLPWeights inputDim hiddenDim) (input : FloatVec inputDim) :
+    0 < mlpForward weights input ∧ mlpForward weights input < 1 := by
+  constructor
+  · exact sigmoid_pos _
+  · exact sigmoid_lt_one _
+
+end Sunbeam
diff --git a/lean4/Sunbeam/Model/ReLU.lean b/lean4/Sunbeam/Model/ReLU.lean
new file mode 100644
index 0000000..3670f28
--- /dev/null
+++ b/lean4/Sunbeam/Model/ReLU.lean
@@ -0,0 +1,21 @@
+import Sunbeam.Model.Basic
+
+namespace Sunbeam
+
+/-- ReLU activation: max(0, x). -/
+def relu (x : Float) : Float :=
+  if x > 0.0 then x else 0.0
+
+/-- Pointwise ReLU on a vector. -/
+def reluVec {n : Nat} (v : FloatVec n) : FloatVec n :=
+  fun i => relu (v i)
+
+/-! ## Trust boundary: ReLU axioms -/
+
+/-- ReLU output is non-negative. -/
+axiom relu_nonneg (x : Float) : relu x ≥ 0.0
+
+/-- ReLU is monotone. -/
+axiom relu_monotone {x y : Float} (h : x ≤ y) : relu x ≤ relu y
+
+end Sunbeam
diff --git a/lean4/Sunbeam/Model/Sigmoid.lean b/lean4/Sunbeam/Model/Sigmoid.lean
new file mode 100644
index 0000000..eda8f09
--- /dev/null
+++ b/lean4/Sunbeam/Model/Sigmoid.lean
@@ -0,0 +1,29 @@
+import Sunbeam.Model.Basic
+
+namespace Sunbeam
+
+/-- The sigmoid function σ(x) = 1 / (1 + exp(-x)). -/
+def sigmoid (x : Float) : Float :=
+  1.0 / (1.0 + Float.exp (-x))
+
+/-! ## Trust boundary: sigmoid axioms
+
+These axioms capture IEEE-754 properties of sigmoid that hold for all finite
+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.
+-/
+
+/-- Sigmoid output is always positive: exp(-x) ≥ 0 ⟹ 1+exp(-x) ≥ 1 ⟹ 1/(1+exp(-x)) > 0. -/
+axiom sigmoid_pos (x : Float) : sigmoid x > 0
+
+/-- Sigmoid output is always less than 1: 1+exp(-x) > 1 ⟹ 1/(1+exp(-x)) < 1. -/
+axiom sigmoid_lt_one (x : Float) : sigmoid x < 1
+
+/-- Sigmoid is monotonically increasing (derivative = σ(1-σ) > 0). -/
+axiom sigmoid_monotone {x y : Float} (h : x ≤ y) : sigmoid x ≤ sigmoid y
+
+end Sunbeam
diff --git a/lean4/Sunbeam/Verify/Structural.lean b/lean4/Sunbeam/Verify/Structural.lean
new file mode 100644
index 0000000..0727cea
--- /dev/null
+++ b/lean4/Sunbeam/Verify/Structural.lean
@@ -0,0 +1,28 @@
+import Sunbeam.Model.Sigmoid
+import Sunbeam.Model.ReLU
+import Sunbeam.Model.MLP
+import Sunbeam.Model.DecisionTree
+import Sunbeam.Model.Ensemble
+
+namespace Sunbeam.Verify
+
+/-! # Tier 1: Structural properties (hold for ANY model weights)
+
+## Axioms (trust boundary — Float operations are opaque to Lean's kernel)
+- `sigmoid_pos`: σ(x) > 0
+- `sigmoid_lt_one`: σ(x) < 1
+- `sigmoid_monotone`: x ≤ y → σ(x) ≤ σ(y)
+- `relu_nonneg`: relu(x) ≥ 0
+- `relu_monotone`: x ≤ y → relu(x) ≤ relu(y)
+
+## Theorems (proved from axioms + structural reasoning)
+- `mlp_output_bounded`: 0 < mlpForward w x ∧ mlpForward w x < 1
+- `tree_block_implies_ensemble_block`: tree = Block → ensemble = Block
+- `ensemble_output_valid`: ensemble ∈ {Block, Allow} (never Defer)
+
+## Automatic guarantees
+- All tree predictions terminate (structural recursion on `TreeNode` inductive)
+- Ensemble composition is total (all match arms covered)
+-/
+
+end Sunbeam.Verify
diff --git a/lean4/lake-manifest.json b/lean4/lake-manifest.json
new file mode 100644
index 0000000..39b011d
--- /dev/null
+++ b/lean4/lake-manifest.json
@@ -0,0 +1,95 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "e308ae1c000103672c716cd6b013a931b02b12d3",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "8629a535d10cd7edfbf1a2c5cdfbaeee135a62cd",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "606af1bfde518881e70b2013ad37f28b3608e4c7",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "5a4234b81b903726764307df9cb23ec3cc3e5758",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.91",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "6d5ec850924e710ea67881e3ca9d1e920c929dbe",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "bc486babc10837d7f43351f12b53879581924163",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "ac3fb7297326c5429ce2844712fb54ba9dd20198",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "06c8b4d690d9b7ef98d594672bbdaa618156215a",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.29.0-rc4",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "sunbeam",
+ "lakeDir": ".lake"}
diff --git a/lean4/lakefile.lean b/lean4/lakefile.lean
new file mode 100644
index 0000000..e7ed1d2
--- /dev/null
+++ b/lean4/lakefile.lean
@@ -0,0 +1,11 @@
+import Lake
+open Lake DSL
+
+package «sunbeam» where
+  leanOptions := #[
+    ⟨`autoImplicit, false⟩
+  ]
+
+@[default_target]
+lean_lib «Sunbeam» where
+  srcDir := "."
diff --git a/lean4/lean-toolchain b/lean4/lean-toolchain
new file mode 100644
index 0000000..b963c47
--- /dev/null
+++ b/lean4/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.29.0-rc4
\ No newline at end of file