Performance

4 measured workloads · Node.js · Apple M4 Pro

Typical processing

1.38 µs

Busier blocks

1.58 µs

Share of the test budget

0.1%

Pole 0.999 · 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.98 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.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.00111
Signed mean over the same steady-render channels and final 4096 frames.
Output RMS · -16.99 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.00 dB
Left-channel RMS gain from the measured tone-gain sweep.
All measured cases
Sample rate · kHzWorkloadTypical · µsBusier blocks · µsTest budget usedObservations
481.381.420.1%—
481.381.460.1%—
961.381.500.1%—
961.381.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.

5 Lean 4 results: 4 proofs in exact arithmetic; 1 counterexample.

Proved in exact arithmetic.Adding the same DC offset to the current and previous inputs leaves the exact blocker step unchanged.
Domain
Exact rational filter state, finite mathematical controls and explicit interval hypotheses
Limits and assumptions
  • Hand-written source-reviewed exact-rational model, not formal TypeScript or compiled-code refinement. Named source files and symbols are digest-bound, and executable dyadic cases are compared with canonical JavaScript. The real DC blocker frounds input, pole, difference, product and output; the model omits all those roundings and excludes NaN, infinity, overflow and signed-zero distinctions. The default 0.99f is not asserted equal to an exact design constant. Constant-response identities do not by themselves prove arbitrary-input stability, and the public pole API does not enforce a stable pole.
Theorem
MaruLean.FilterContracts.dc_offset_invariant
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.Once the previous input equals a constant stream, the exact blocker output is the initial output times the pole raised to the sample count.
Domain
Exact rational filter state, finite mathematical controls and explicit interval hypotheses
Limits and assumptions
  • Hand-written source-reviewed exact-rational model, not formal TypeScript or compiled-code refinement. Named source files and symbols are digest-bound, and executable dyadic cases are compared with canonical JavaScript. The real DC blocker frounds input, pole, difference, product and output; the model omits all those roundings and excludes NaN, infinity, overflow and signed-zero distinctions. The default 0.99f is not asserted equal to an exact design constant. Constant-response identities do not by themselves prove arbitrary-input stability, and the public pole API does not enforce a stable pole.
Theorem
MaruLean.FilterContracts.dc_constant_history_response
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.From cleared history, a constant input produces its amplitude followed by the exact geometric pole response at every sample index.
Domain
Exact rational filter state, finite mathematical controls and explicit interval hypotheses
Limits and assumptions
  • Hand-written source-reviewed exact-rational model, not formal TypeScript or compiled-code refinement. Named source files and symbols are digest-bound, and executable dyadic cases are compared with canonical JavaScript. The real DC blocker frounds input, pole, difference, product and output; the model omits all those roundings and excludes NaN, infinity, overflow and signed-zero distinctions. The default 0.99f is not asserted equal to an exact design constant. Constant-response identities do not by themselves prove arbitrary-input stability, and the public pole API does not enforce a stable pole.
Theorem
MaruLean.FilterContracts.dc_constant_after_first
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.Explicit bounded-input, previous-input, pole and output hypotheses bound one exact blocker step.
Domain
Exact rational filter state, finite mathematical controls and explicit interval hypotheses
Limits and assumptions
  • Hand-written source-reviewed exact-rational model, not formal TypeScript or compiled-code refinement. Named source files and symbols are digest-bound, and executable dyadic cases are compared with canonical JavaScript. The real DC blocker frounds input, pole, difference, product and output; the model omits all those roundings and excludes NaN, infinity, overflow and signed-zero distinctions. The default 0.99f is not asserted equal to an exact design constant. Constant-response identities do not by themselves prove arbitrary-input stability, and the public pole API does not enforce a stable pole.
Theorem
MaruLean.FilterContracts.dc_step_bound
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Counterexample.An unrestricted pole of two makes a unit constant input grow to eight by the fourth sample.
Domain
Exact rational filter state, finite mathematical controls and explicit interval hypotheses
Limits and assumptions
  • Hand-written source-reviewed exact-rational model, not formal TypeScript or compiled-code refinement. Named source files and symbols are digest-bound, and executable dyadic cases are compared with canonical JavaScript. The real DC blocker frounds input, pole, difference, product and output; the model omits all those roundings and excludes NaN, infinity, overflow and signed-zero distinctions. The default 0.99f is not asserted equal to an exact design constant. Constant-response identities do not by themselves prove arbitrary-input stability, and the public pole API does not enforce a stable pole.
Theorem
MaruLean.FilterContracts.dc_unstable_pole_refuses_decay
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed