Performance

4 measured workloads · Node.js · Apple M4 Pro

Typical processing

1.25 µs

Busier blocks

1.33 µs

Share of the test budget

0.1%

Feedback write helper · 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
-11.37 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 · 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 · -11.37 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.00148
Signed mean over the same steady-render channels and final 4096 frames.
Output RMS · -14.39 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.
Energy after 1 second · -120.00 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.251.330.0%—
481.251.380.1%—
961.251.380.1%Timing varies
961.251.330.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.

4 Lean 4 results: 4 proofs in exact arithmetic.

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