Sienna Meridian Satterwhite
982cf5755d
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>
29 lines
952 B
Lean4
29 lines
952 B
Lean4
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
|