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.
2 Lean 4 results: 2 proofs in exact arithmetic.
Proved in exact arithmetic.The dry/wet sum and the subtract-then-scale interpolation form are algebraically equal.
Domain
Exact rational samples and mix coefficient
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. This does not authorize changing the existing floating-point operation order.
Theorem
MaruLean.LeafContracts.drywet_is_lerp
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.A dry/wet mix stays inside the common input interval for a mix between zero and one.
Domain
Exact rationals; ordered finite bounds and stated coefficient guards; mix 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.