Performance

4 measured workloads · Node.js · Apple M4 Pro

Typical processing

1.54 µs

Busier blocks

1.63 µs

Share of the test budget

0.1%

6 kHz cutoff · Q 2 · 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
-13.77 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 · -13.77 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.00106
Signed mean over the same steady-render channels and final 4096 frames.
Output RMS · -16.79 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.21 dB
Left-channel RMS gain from the measured tone-gain sweep.
All measured cases
Sample rate · kHzWorkloadTypical · µsBusier blocks · µsTest budget usedObservations
481.501.580.1%—
481.541.670.1%—
961.541.670.1%—
961.541.630.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.

5 Lean 4 results: 1 proof in its stated domain; 4 proofs in exact arithmetic.

Proved in exact arithmetic.The state-variable filter's exact coefficients from g = tan(pi f / fs) and k = 1 / Q satisfy the Jury conditions for every positive g and k.
Domain
exact arithmetic in any ordered field, g > 0 and k > 0
Limits and assumptions
  • Frozen settings and exact coefficients; the tangent is assumed, not proved.
Theorem
MaruLean.FilterStability.svf_jury
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in the stated domain.Two of the state-variable filter's three Jury conditions hold for any coefficients with the stated signs and bounds, rounded or not, because the sum they test has no cancellation.
Domain
any coefficient values in an ordered field that satisfy the stated sign bounds
Limits and assumptions
  • Covers two of the three conditions only. That round-to-nearest keeps those signs and bounds is argued in the file, not proved about floats.
  • This record also covers MaruLean.FilterStability.svf_rounded_dMinus, MaruLean.FilterStability.svf_dPlus_identity, MaruLean.FilterStability.svf_dMinus_identity; axioms describe MaruLean.FilterStability.svf_rounded_dPlus only.
Theorem
MaruLean.FilterStability.svf_rounded_dPlus
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.At a fixed Q, the order in which the state-variable filter's cutoffs arrive does not change its state.
Domain
exact arithmetic over any commutative ring, no input
Limits and assumptions
  • Exact arithmetic with no input; the rounded tick is measured in bench/modulation/time-warp-check.mjs, not proved. Nobody has listened, so it says nothing about which filter sounds better. A moving Q is not covered.
  • This record also covers MaruLean.ModulationStability.step_eq, MaruLean.ModulationStability.step_det; axioms describe MaruLean.ModulationStability.step_comm only.
Theorem
MaruLean.ModulationStability.step_comm
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.No cutoff and no Q can raise the state-variable filter's stored energy on any sample.
Domain
exact arithmetic in an ordered commutative ring, g >= 0 and k >= 0, no input
Limits and assumptions
  • Exact arithmetic with no input; the rounded tick is measured in bench/modulation/time-warp-check.mjs, not proved. Nobody has listened, so it says nothing about which filter sounds better.
  • This record also covers MaruLean.ModulationStability.energy_identity, MaruLean.ModulationStability.lossless_set_leaves; axioms describe MaruLean.ModulationStability.energy_step only.
Theorem
MaruLean.ModulationStability.energy_step
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.With no damping, two state-variable steps are one step at the tangent sum of their g, so the ring follows the cutoff with no pitch error.
Domain
exact arithmetic over any commutative ring, k = 0, no input
Limits and assumptions
  • Exact arithmetic with no input; the rounded tick is measured in bench/modulation/time-warp-check.mjs, not proved. Nobody has listened, so it says nothing about which filter sounds better.
Theorem
MaruLean.ModulationStability.step_compose_lossless
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed