Performance

4 measured workloads · Node.js · Apple M4 Pro

Typical processing

1.38 µs

Busier blocks

1.46 µs

Share of the test budget

0.1%

6 kHz lowpass · 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
0 bytes
Impulse first arrival
0.00 ms
Peak output
-14.10 dBFS

Measured tone gain

Gain · dB

Nine separate 0.2-peak sine renders; left-channel RMS gain during 250–500 ms. Includes modulation/envelope behavior; not an LTI error or phase-response measurement.
Measurement details
Retained DSP buffers · 0 bytes
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 · -14.10 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.00098
Signed mean over the same steady-render channels and final 4096 frames.
Output RMS · -17.11 dBFS
RMS over all channels of the same steady-render window.
Impulse first arrival · 0.00 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.
Gain at 1 kHz · -0.12 dB
Left-channel RMS gain from the measured tone-gain sweep.
All measured cases
Sample rate · kHzWorkloadTypical · µsBusier blocks · µsTest budget usedObservations
481.381.540.1%Timing varies
481.421.500.1%—
961.421.750.1%Timing varies
961.381.460.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.

6 Lean 4 results: 1 proof in its stated domain; 5 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.

One-pole signal bounds

y[n + 1] = y[n] + α (u − y[n])

0 ≤ α ≤ 1. The initial state and every input lie inside the displayed interval.

Coefficient α0.25
Initial state-0.75
Constant input0.75

Within theorem assumptions

The theorem covers every sample and every bounded input sequence. The plot shows 32 steps with one constant input.

Sample → State. Solid line: numerical example. Dashed lines: interval bounds.
State after 32 steps
0.74985
Lower bound
-0.75
Upper bound
0.75
Read this proof’s domain and limits
Proved in the stated domain.One concrete onePoleLowpassTick generated from Maru compiler IR gives the bits Node gives.
Domain
one concrete binary64 input, evaluated in the kernel
Limits and assumptions
  • A single test vector, which is evidence and not a theorem about all inputs.
Theorem
IrToLean.Proof.onePole_vector
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The one-pole design has exactly half power at its design point on the unit circle; its coefficient and pole lie strictly between zero and one.
Domain
Ordered field; c²+s²=1, c<1, r>=0, r²=(1-c)²+2(1-c), coefficient a=r-(1-c).
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 nonnegative-root and unit-circle equations are explicit assumptions; their numerical computation is not proved. The squared response equals 1/2, not an approximate sampled-frequency check.
  • This record also covers MaruLean.SignalBounds.coefficient_stable, MaruLean.SignalBounds.coefficient_design_equation, MaruLean.SignalBounds.coefficient_half_power, MaruLean.SignalBounds.frequency_denominator_identity; axioms describe MaruLean.SignalBounds.coefficient_half_power_on_circle only.
Theorem
MaruLean.SignalBounds.coefficient_half_power_on_circle
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.For every input stream and every sample index, a one-pole update remains in the common input/initial-state interval even when its coefficient changes on every sample.
Domain
Ordered field; every coefficient in [0,1], all inputs and initial state in [lo,hi]; arbitrary natural sample index.
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 theorem treats the unflushed recurrence. The separate flush theorem preserves intervals containing zero. It does not infer coefficient validity from an unverified setter.
  • This record also covers MaruLean.SignalBounds.pole_step_interval; axioms describe MaruLean.SignalBounds.pole_run_interval only.
Theorem
MaruLean.SignalBounds.pole_run_interval
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.Flush-to-zero cannot increase squared sample energy and preserves the one-pole stream bound whenever the interval contains zero.
Domain
Ordered field; 0 in [lo,hi], every coefficient in [0,1], all inputs and initial state in [lo,hi]; every sample index.
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 zeroing branch is included as exact mathematics; rounded intermediate arithmetic is not. This is an arbitrary-duration induction, not a finite render.
  • This record also covers MaruLean.SignalBounds.flush_energy_nonincreasing; axioms describe MaruLean.SignalBounds.flushed_pole_run_interval only.
Theorem
MaruLean.SignalBounds.flushed_pole_run_interval
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.For a constant input and coefficient, the exact state at every sample is target + (1-a)^n times the initial error.
Domain
Ordered field; constant coefficient a and input target; arbitrary initial state and natural sample index n.
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 closed-form response is for the linear unflushed recurrence. The formula is valid algebraically for any a; decay requires the pole factor to have magnitude below one.
  • This record also covers MaruLean.SignalBounds.decay_constant, MaruLean.SignalBounds.pole_constant_fixed; axioms describe MaruLean.SignalBounds.pole_step_response only.
Theorem
MaruLean.SignalBounds.pole_step_response
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.Under arbitrary shared input and coefficient modulation, squared initial-state error is bounded by (1-amin)^n squared times its initial value.
Domain
Ordered field; 0<=amin<=a[n]<=1, same input/coefficient streams, arbitrary initial states and sample index.
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. A strictly positive coefficient floor makes the geometric factor less than one. This proves the finite-index bound for every n, not a topological convergence theorem. The error identity excludes flushing.
  • This record also covers MaruLean.SignalBounds.pole_state_difference, MaruLean.SignalBounds.decay_product_interval, MaruLean.SignalBounds.decay_geometric_bound; axioms describe MaruLean.SignalBounds.pole_state_contraction only.
Theorem
MaruLean.SignalBounds.pole_state_contraction
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed