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.
1 Lean 4 result: 1 proof in exact arithmetic.
Proved in exact arithmetic.The stereo arithmetic mean stays inside the common interval of its input channels.
Domain
Exact rationals; ordered finite bounds and stated coefficient guards
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.