Lean 4 checks algorithm properties and candidate optimization rewrites within stated assumptions. A model proof does not establish that an optimization is enabled in this node or on any target. Performance measurements establish speed.
3 Lean 4 results: 3 proofs in exact arithmetic.
Proved in exact arithmetic.The squared velocity curve stays between zero and one for a normalized strike.
Domain
Exact rational normalized velocity in [0, 1]
Limits and assumptions
Hand-written source-reviewed model, not formal refinement of TypeScript or compiled code. Named functions and whole-file source digests are checked; finite canonical JavaScript cases are compared with executable Lean definitions. Exact rational arithmetic only: IEEE rounding, overflow, NaN, infinities and signed-zero behavior are not proved. Sampler mappings cover the named shared stage only. No optimization is enabled or claimed faster.
Theorem
MaruLean.LeafContracts.velocity_square_bounded
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.Both linear and squared velocity responses stay between the configured floor and unity.
Domain
Exact rational velocity and floor in [0, 1]; linear or squared curve
Limits and assumptions
Hand-written source-reviewed model, not formal refinement of TypeScript or compiled code. Named functions and whole-file source digests are checked; finite canonical JavaScript cases are compared with executable Lean definitions. Exact rational arithmetic only: IEEE rounding, overflow, NaN, infinities and signed-zero behavior are not proved. Sampler mappings cover the named shared stage only. No optimization is enabled or claimed faster.
Theorem
MaruLean.LeafContracts.velocity_response_bounded
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.A velocity-response floor of one gives unity gain for either curve.
Domain
Exact rational velocity; floor = 1; linear or squared curve
Limits and assumptions
Hand-written source-reviewed model, not formal refinement of TypeScript or compiled code. Named functions and whole-file source digests are checked; finite canonical JavaScript cases are compared with executable Lean definitions. Exact rational arithmetic only: IEEE rounding, overflow, NaN, infinities and signed-zero behavior are not proved. Sampler mappings cover the named shared stage only. No optimization is enabled or claimed faster.