lean4/Sunbeam/Model/Sigmoid.lean

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 (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. -/
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
-												feat(lean4): add formal verification specs for ensemble models

Lean 4 formalization of the decision tree + MLP ensemble architecture.
Axiomatizes Float properties (sigmoid bounds, ReLU nonnegativity) since
Lean's Float ops are extern-backed. Proves MLP output is bounded in (0,1)
and ensemble output is always a valid decision. No mathlib dependency.

Signed-off-by: Sienna Meridian Satterwhite <sienna@sunbeam.pt>

											
										
										
											2026-03-10 23:38:21 +00:00
+								import Sunbeam.Model.Basic
 								namespace Sunbeam
 								/-- The sigmoid function σ(x) = 1 / (1 + exp(-x)). -/
 								def sigmoid (x : Float) : Float :=
 .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.
-												docs(lean4): add Rust cross-references to formal specs

Add documentation comments linking Lean 4 specifications to their
corresponding Rust implementations (tree_predict, mlp_predict_32,
PackedNode). Reference TorchLean arXiv ID for future axiom replacement.

Signed-off-by: Sienna Meridian Satterwhite <sienna@sunbeam.pt>

											
										
										
											2026-03-10 23:38:22 +00:00
+								When TorchLean (arXiv:2602.22631) ships its verified Float32 kernel, these
 								axioms can be replaced with proofs against that kernel.
-												feat(lean4): add formal verification specs for ensemble models

Lean 4 formalization of the decision tree + MLP ensemble architecture.
Axiomatizes Float properties (sigmoid bounds, ReLU nonnegativity) since
Lean's Float ops are extern-backed. Proves MLP output is bounded in (0,1)
and ensemble output is always a valid decision. No mathlib dependency.

Signed-off-by: Sienna Meridian Satterwhite <sienna@sunbeam.pt>

											
										
										
											2026-03-10 23:38:21 +00:00
+								-/
 								/-- 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