studio/proxy
2
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
45 Commits 1 Branch 0 Tags
mainline
Commit Graph

2 Commits

Author SHA1 Message Date
Sienna Meridian Satterwhite
3628424f43 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
Sienna Meridian Satterwhite
982cf5755d 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