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>
12 lines
170 B
Lean4
12 lines
170 B
Lean4
import Lake
|
|
open Lake DSL
|
|
|
|
package «sunbeam» where
|
|
leanOptions := #[
|
|
⟨`autoImplicit, false⟩
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib «Sunbeam» where
|
|
srcDir := "."
|