Performance

4 measured workloads · Node.js · Apple M4 Pro

Typical processing

1.46 µs

Busier blocks

1.58 µs

Share of the test budget

0.1%

250.5 ms · feedback 0.7 · 96 kHz · 1.333 ms available per block in this test.

Processing cost

Processing time in µs · lower means less work

Select a point to inspect its measurements. Hollow points indicate variable timing. Lines guide the eye; only marked cases were measured.
Retained DSP buffers
93.9 KiB
Impulse first arrival
250.50 ms
Peak output
-13.98 dBFS

Captured energy decay

Remaining energy · dB

Stereo-summed backward squared-energy integration, sampled every 20 ms, normalized to the captured 2 s impulse response. Finite-window curve; no extrapolated RT60 claim.
Measurement details
Retained DSP buffers · 93.9 KiB
Unique backing-buffer capacity reachable from prepared DSP state, including borrowed rings and retained scratch. Excludes JS objects, scalar fields, harness buffers and transient allocation; zero does not mean zero total memory.
Peak output · -13.98 dBFS
Last 4096 frames of a 0.5 s steady render. Effects receive a 0.2-peak 1 kHz sine; sources generate their declared waveform. No automatic musical-quality verdict.
DC offset · 0.00110
Signed mean over the same steady-render channels and final 4096 frames.
Output RMS · -17.00 dBFS
RMS over all channels of the same steady-render window.
Impulse first arrival · 250.50 ms
First channel sample at or above -120 dBFS after a 0.2 impulse, following 250 ms + 127 frames of silence; 2 s observation. Includes configured delay, phase and any dry path. Not device latency or group delay. No detection is unavailable, not zero.
Energy after 1 second · -9.52 dB
Energy in the second second relative to the captured 2 s response. A long decay may extend beyond the capture.
All measured cases
Sample rate · kHzWorkloadTypical · µsBusier blocks · µsTest budget usedObservations
481.461.580.1%—
481.461.630.1%—
961.541.710.1%Timing varies
961.461.580.1%—

Times are per 128-frame audio block. Test budget used divides the p95 time by the block period at that case’s sample rate. Machine and runtime are shared.

Test setup

Node.js · Apple M4 Pro · 48 / 96 kHz · 128 frames per block · 3 repeated tests ·

Typical summarizes the middle measured block times. Busier blocks summarizes the time that 95% of blocks completed within in each repeat. These figures measure DSP processing; application scheduling, loading samples and device output require separate checks. Memory and signal probes run separately from the timing loop.

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.

8 Lean 4 results: 2 proofs in their stated domains; 5 proofs in exact arithmetic; 1 counterexample.

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.

Feedback delay bounds

y[n] = u[n] + g y[n − D]; B = A / (1 − |g|)

D is a positive integer, |g| < 1, |u[n]| ≤ A, and the initial history lies in [−B, B]. This example starts with zero history.

Feedback g0.5
Input amplitude A0.5
Delay D (samples)4

Within theorem assumptions

The BIBO theorem bounds any duration with bounded input and history. This plot shows 64 samples of a constant input.

Sample → Delay output. Solid line: numerical example. Dashed lines: bibo bounds.
Last plotted output
0.99998
Absolute bound B
1
Read this proof’s domain and limits
Proved in the stated domain.Advancing a ring cursor by compare-and-reset produces an index below every positive active length.
Domain
Natural-number cursor and positive active length
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. The read before this update still needs a valid initial cursor and allocated capacity.
Theorem
MaruLean.LeafContracts.ring_step_in_bounds
Recorded axioms
propext, Quot.sound
Manifest reviewed
Proved in the stated domain.The final active ring position advances to zero.
Domain
Natural-number positive active length
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.ring_step_last
Recorded axioms
propext, Quot.sound
Manifest reviewed
Counterexample.An empty active ring has no valid in-range cursor, even when compare-and-reset returns zero.
Domain
One zero-length integer 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. Alignment deliberately bypasses its buffer when frames is zero; this is not a claim that its bypass is unsafe.
Theorem
MaruLean.LeafContracts.ring_empty_refuses_bound
Manifest reviewed
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.
Theorem
MaruLean.LeafContracts.drywet_bounded
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The clamped feedback write is between minus one and one in exact arithmetic.
Domain
Exact rational dry sample, delayed sample and feedback
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 covers only the write stage, not feedback-system stability.
Theorem
MaruLean.LeafContracts.feedback_write_bounded
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.At zero feedback the write stage is exactly the clamped dry sample.
Domain
Exact rational dry and delayed samples; feedback = 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.feedback_zero
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.For every positive delay length and every sample, bounded input of amplitude A and arbitrary signed feedback |g[n]|<=q<1 give an exact state bound A/(1-q).
Domain
Ordered field; positive integer delay, A>=0, 0<=q<1, input in [-A,A], feedback in [-q,q], zero initial history.
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. Strong induction handles arbitrary delay lengths, input streams and feedback modulation. This is the ideal unclipped delay recurrence; the shipped node also clips writes and stores binary32. Those operations are separate obligations. The delay length is fixed within the recurrence; delay-time automation is not covered.
  • This record also covers MaruLean.SignalBounds.delay_bibo_invariant, MaruLean.SignalBounds.signed_product_bound, MaruLean.SignalBounds.feedback_step_bound; axioms describe MaruLean.SignalBounds.delay_bibo only.
Theorem
MaruLean.SignalBounds.delay_bibo
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed