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.

21 Lean 4 results: 10 proofs in their stated domains; 8 proofs in exact arithmetic; 3 counterexamples.

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.

Crossfade weight progression

S(t) = t² (3 − 2t); S(b) − S(a) ≥ (b − a)³ > 0

0 ≤ a < b ≤ 1. Moving either position beyond this domain removes the strict-increase guarantee.

First position a0.25
Second position b0.75

Within theorem assumptions

The vertical lines mark a and b. The curve decreases beyond 1, illustrating why the theorem needs its domain restriction.

Position t → Crossfade weight. Solid line: numerical example. Dashed lines: unit interval. Vertical lines: selected positions.
Weight at a
0.15625
Weight at b
0.84375
Weight increase
0.6875
Theorem minimum increase
0.125
Read this proof’s domain and limits
Proved in the stated domain.Reversing an in-range frame keeps the read index inside the same region.
Domain
Natural-number region addresses; index below frame count
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. Integer addresses must be valid, nonnegative and exactly representable; validated region and arena assumptions are explicit. Sampler mapping covers only its delegated indexing/interpolation stage, not voice lifecycle, arena ownership or the whole renderer.
Theorem
MaruLean.LeafContracts.reverse_in_bounds
Recorded axioms
propext, Quot.sound
Manifest reviewed
Proved in the stated domain.Reversing an in-range frame twice returns its original play index.
Domain
Natural-number region addresses; index below frame count
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. Integer addresses must be valid, nonnegative and exactly representable; validated region and arena assumptions are explicit. Sampler mapping covers only its delegated indexing/interpolation stage, not voice lifecycle, arena ownership or the whole renderer.
Theorem
MaruLean.LeafContracts.reverse_involution
Recorded axioms
propext, Quot.sound
Manifest reviewed
Proved in the stated domain.A reversed frame remains inside the arena when the entire region fits in that arena.
Domain
Natural-number base, frame count, index and arena capacity; index < frames and base + frames <= capacity
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. Integer addresses must be valid, nonnegative and exactly representable; validated region and arena assumptions are explicit. Sampler mapping covers only its delegated indexing/interpolation stage, not voice lifecycle, arena ownership or the whole renderer.
Theorem
MaruLean.LeafContracts.reverse_arena_bound
Recorded axioms
propext, Quot.sound
Manifest reviewed
Proved in the stated domain.The next interpolation partner of a valid continuous loop remains below the loop end.
Domain
Natural-number continuous-loop addresses; start < end and index < end
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. Integer addresses must be valid, nonnegative and exactly representable; validated region and arena assumptions are explicit. Sampler mapping covers only its delegated indexing/interpolation stage, not voice lifecycle, arena ownership or the whole renderer.
Theorem
MaruLean.LeafContracts.loop_partner_in_bounds
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in the stated domain.The interpolation partner of the last loop frame is the loop start, not the unlooped frame after the end.
Domain
Natural-number continuous-loop addresses; start < end
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. Integer addresses must be valid, nonnegative and exactly representable; validated region and arena assumptions are explicit. Sampler mapping covers only its delegated indexing/interpolation stage, not voice lifecycle, arena ownership or the whole renderer.
Theorem
MaruLean.LeafContracts.loop_partner_at_seam
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in the stated domain.Before the loop seam, the interpolation partner is exactly the next frame.
Domain
Natural-number continuous-loop addresses; index + 1 < end
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. Integer addresses must be valid, nonnegative and exactly representable; validated region and arena assumptions are explicit. Sampler mapping covers only its delegated indexing/interpolation stage, not voice lifecycle, arena ownership or the whole renderer.
Theorem
MaruLean.LeafContracts.loop_partner_before_seam
Recorded axioms
propext, Quot.sound
Manifest reviewed
Proved in the stated domain.Subtracting the number of whole loop lengths equals taking the integer remainder, with no iterative wrap.
Domain
Natural-number distance and length; exact integer division
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. Integer addresses must be valid, nonnegative and exactly representable; validated region and arena assumptions are explicit. Sampler mapping covers only its delegated indexing/interpolation stage, not voice lifecycle, arena ownership or the whole renderer.
Theorem
MaruLean.LeafContracts.wrap_division_is_remainder
Recorded axioms
propext, Quot.sound
Manifest reviewed
Proved in the stated domain.A cursor at or beyond the loop start wraps inside the loop even after overshooting by several lengths.
Domain
Natural-number addresses; start < end and start <= index
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. Integer addresses must be valid, nonnegative and exactly representable; validated region and arena assumptions are explicit. Sampler mapping covers only its delegated indexing/interpolation stage, not voice lifecycle, arena ownership or the whole renderer.
Theorem
MaruLean.LeafContracts.wrap_in_bounds
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in the stated domain.Wrapping leaves a cursor before the loop end unchanged, including pre-roll frames.
Domain
Natural-number addresses; index < end
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. Integer addresses must be valid, nonnegative and exactly representable; validated region and arena assumptions are explicit. Sampler mapping covers only its delegated indexing/interpolation stage, not voice lifecycle, arena ownership or the whole renderer.
Theorem
MaruLean.LeafContracts.wrap_inside_unchanged
Recorded axioms
propext, Quot.sound
Manifest reviewed
Proved in the stated domain.Wrapping a valid cursor a second time cannot move it again.
Domain
Natural-number addresses; start < end and start <= index
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. Integer addresses must be valid, nonnegative and exactly representable; validated region and arena assumptions are explicit. Sampler mapping covers only its delegated indexing/interpolation stage, not voice lifecycle, arena ownership or the whole renderer.
Theorem
MaruLean.LeafContracts.wrap_idempotent
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Counterexample.A pre-roll index of 2 stays at 2 for loop [4, 8); the unconditional claim that every cursor is at least the loop start is false.
Domain
One exact integer pre-roll witness
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. One concrete witness; it refutes the stated unrestricted claim, not every possible guarded implementation.
Theorem
MaruLean.LeafContracts.wrap_preroll_refuses_lower_bound
Manifest reviewed
Proved in exact arithmetic.Linear interpolation at fraction zero selects the first sample and at fraction one selects the second.
Domain
Exact rational samples and fractions zero or one
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.lerp_endpoints
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.Interpolating two bounded samples stays in their common interval when the fraction is between zero and one.
Domain
Exact rationals; ordered finite bounds and stated coefficient guards; fraction 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.lerp_bounded
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Counterexample.Interpolation with fraction 2 produces 2 from samples 0 and 1; a bounded-output claim requires the fraction guard.
Domain
One exact rational extrapolation witness
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. One concrete witness; it refutes the stated unrestricted claim, not every possible guarded implementation.
Theorem
MaruLean.LeafContracts.lerp_extrapolation_refused
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The cubic smoothstep loop-crossfade weight remains between zero and one for a normalized position.
Domain
Exact rational normalized position 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.smoothstep_bounded
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The cubic crossfade weight is zero at normalized position zero and one at normalized position one.
Domain
Exact rational normalized positions zero and one
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. The first actual crossfade frame uses normalized position 1/span, not zero.
Theorem
MaruLean.LeafContracts.smoothstep_endpoints
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The last frame of a positive crossfade span reaches the incoming run-up material exactly.
Domain
Exact rational samples and positive crossfade span; position = span - 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.crossfade_last
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.A loop crossfade stays in the common interval of both samples throughout its valid span.
Domain
Exact rational bounded samples; span > 0, position >= 0 and position + 1 <= span
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.crossfade_bounded
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Counterexample.The sampler cursor fraction 1 - 2^-25 rounds to exactly one at its f32 store, so a strict fraction < 1 invariant is false.
Domain
One binary64-to-binary32 conversion at the sampler cursor store
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. One concrete witness; it refutes the stated unrestricted claim, not every possible guarded implementation. The Lean conversion witness trusts native_decide; the canonical JavaScript cursor reproduces it. This alone does not establish an audible defect.
Theorem
MaruLean.LeafContracts.cursor_fraction_can_round_to_one
Recorded axioms
propext, Classical.choice, Quot.sound, MaruLean.LeafContracts.cursor_fraction_can_round_to_one._native.native_decide.ax_1_1
Manifest reviewed
Proved in exact arithmetic.Linear interpolation satisfies Jensen’s squared-energy inequality throughout the unit interval, with an exact nonnegative deficit t(1-t)(a-b)².
Domain
Ordered field; arbitrary samples a,b and interpolation fraction 0<=t<=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. The inputs are scalar samples and the blend is linear. No claim is made about changing audio inputs across a window or about unguarded extrapolation.
  • This record also covers MaruLean.SignalBounds.lerp_energy_identity; axioms describe MaruLean.SignalBounds.lerp_energy_convex only.
Theorem
MaruLean.SignalBounds.lerp_energy_convex
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The cubic crossfade S(t)=t²(3-2t) is strictly increasing on [0,1], with S(b)-S(a)>=(b-a)³ for every ordered pair of positions.
Domain
Ordered field; 0<=a<=b<=1, with strict output order when a<b.
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 is a quantified polynomial proof over the whole interval, not a sampled slope test. It concerns the blend weight; varying input audio need not itself be monotone.
  • This record also covers MaruLean.SignalBounds.smoothstep_increment_bound; axioms describe MaruLean.SignalBounds.smoothstep_strictly_increasing only.
Theorem
MaruLean.SignalBounds.smoothstep_strictly_increasing
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed