Performance

No benchmarks published

No timing measurements are published for this node.
View target support

Lean 4 proofs and optimization limits

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.

9 Lean 4 results: 9 proofs in exact arithmetic.

Explore the mathematics

Move the controls to explore a theorem’s behavior and assumptions. These browser calculations use floating-point numbers to illustrate the mathematical model. They do not run Lean or the audio engine. Lean checks the general statement; a plotted example does not prove it.

Stereo width and energy

Eout = (L + R)² / 2 + w² (L − R)² / 2 ≤ max(1, w²) Ein

Exact arithmetic. The gain bound uses a factor at least 1 and at least w²; this example chooses max(1, w²).

Left input L0.75
Right input R-0.25
Width w0.5

Within theorem assumptions

At widths up to 1, energy cannot increase. Above 1, the permitted gain grows with w². The vertical line marks the selected width.

Width w → Output energy. Solid line: numerical example. Dashed lines: energy bound. Vertical lines: selected positions.
Input energy
0.625
Selected output energy
0.25
Selected energy bound
0.625
Read this proof’s domain and limits
Proved in exact arithmetic.Stereo width one preserves both channel values in exact arithmetic.
Domain
Exact rational channel samples; width = 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.width_unity
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.Stereo width zero sends the same arithmetic mean to both channels.
Domain
Exact rational channel samples; width = 0
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.width_zero_mono
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The stereo width matrix preserves the mid signal at every width.
Domain
Exact rational channel samples and width
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.width_mid_preserved
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The stereo width matrix scales the channel difference by the width coefficient.
Domain
Exact rational channel samples and width
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.width_side_scaled
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
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.
Theorem
MaruLean.LeafContracts.mono_bounded
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.Matched mid/side encoding and decoding recover both input channels in exact arithmetic.
Domain
Exact rational channel samples; rounding treated as identity
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.mid_side_roundtrip
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The stereo width matrix cannot increase total squared-channel energy whenever w²<=1.
Domain
Ordered field; arbitrary left/right samples and width with w²<=1.
Limits and assumptions
  • Mathematical theorem over an arbitrary ordered field, with every hypothesis in its Lean type. Exact arithmetic only; IEEE rounding, overflow, non-finites and platform transcendental implementations are outside this theorem. Source bindings identify the reviewed DSP relationship, not a formal translation or a compiled-artifact proof. This proves a signal-energy inequality, not a loudness or sound-quality judgment. The width setter and per-operation rounding are not assumed to satisfy additional properties.
  • This record also covers MaruLean.SignalBounds.width_energy_identity, MaruLean.SignalBounds.width_energy_change; axioms describe MaruLean.SignalBounds.width_energy_nonincreasing only.
Theorem
MaruLean.SignalBounds.width_energy_nonincreasing
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The width matrix has squared-energy gain at most K whenever K>=1 and K>=w²; common and opposite channel modes attain the gains 1 and w².
Domain
Ordered field; arbitrary channel samples and width; K>=1 and K>=w².
Limits and assumptions
  • Mathematical theorem over an arbitrary ordered field, with every hypothesis in its Lean type. Exact arithmetic only; IEEE rounding, overflow, non-finites and platform transcendental implementations are outside this theorem. Source bindings identify the reviewed DSP relationship, not a formal translation or a compiled-artifact proof. The common/side mode equalities establish the sharp modal gains. This is exact linear algebra; it does not measure perceived loudness or prove floating-point bit identity.
  • This record also covers MaruLean.SignalBounds.width_common_mode, MaruLean.SignalBounds.width_side_mode_energy; axioms describe MaruLean.SignalBounds.width_energy_gain_bound only.
Theorem
MaruLean.SignalBounds.width_energy_gain_bound
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.Amplitude-normalized mid/side encoding has exactly half the input stereo squared-channel energy.
Domain
Ordered field; M=(L+R)/2 and S=(L-R)/2; arbitrary channel samples.
Limits and assumptions
  • Mathematical theorem over an arbitrary ordered field, with every hypothesis in its Lean type. Exact arithmetic only; IEEE rounding, overflow, non-finites and platform transcendental implementations are outside this theorem. Source bindings identify the reviewed DSP relationship, not a formal translation or a compiled-artifact proof. The source rounds the encoded values to binary32; this identity omits those rounding boundaries. It describes amplitude normalization rather than a unit-energy normalization.
Theorem
MaruLean.SignalBounds.mid_side_energy
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed