Tone filter (@maru/filters-tone)

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 tone control · 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: -17.05 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 · -17.05 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.00023: Signed mean over the same steady-render channels and final 4096 frames.
Output RMS · -20.05 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 · -3.07 dB: Left-channel RMS gain from the measured tone-gain sweep.

All measured cases

Sample rate · kHz	Typical · µs	Busier blocks · µs	Test budget used	Observations
48	1.38	1.50	0.1%	—
48	1.38	1.50	0.1%	Timing varies
96	1.38	1.50	0.1%	—
96	1.38	1.46	0.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 · Nov 7, 2026

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: 5 proofs in exact arithmetic; 1 counterexample.

Proved in exact arithmetic.The clamped tone coefficient lies between one thousandth and unity in the rational design model.

Domain: Exact rational tone state and controls; finite positive sample rates for coefficient design; explicit coefficient and zero-containing 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 model includes the strict flush interval but omits binary64 rounding, NaN, infinity and signed-zero distinctions. The design recurrence requires positive sample rates and assumes rational division/clamping, not arbitrary IEEE sample-rate admission. The stream theorem requires a zero-containing interval and finite valid state; no transcendental coefficient design, processing deadline or Rust artifact theorem is claimed.
Theorem: MaruLean.FilterContracts.tone_coefficient_bounded
Recorded axioms: propext, Classical.choice, Quot.sound
Manifest reviewed: 2026-11-08

Proved in exact arithmetic.The tone update with flush-to-zero preserves any bounded interval containing zero when its coefficient lies in [0,1].

Domain: Exact rational tone state and controls; finite positive sample rates for coefficient design; explicit coefficient and zero-containing 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 model includes the strict flush interval but omits binary64 rounding, NaN, infinity and signed-zero distinctions. The design recurrence requires positive sample rates and assumes rational division/clamping, not arbitrary IEEE sample-rate admission. The stream theorem requires a zero-containing interval and finite valid state; no transcendental coefficient design, processing deadline or Rust artifact theorem is claimed.
Theorem: MaruLean.FilterContracts.tone_step_interval
Recorded axioms: propext, Classical.choice, Quot.sound
Manifest reviewed: 2026-11-08

Proved in exact arithmetic.For every sample index, an arbitrarily modulated tone stream remains in its zero-containing input/state interval with admitted coefficients.

Domain: Exact rational tone state and controls; finite positive sample rates for coefficient design; explicit coefficient and zero-containing 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 model includes the strict flush interval but omits binary64 rounding, NaN, infinity and signed-zero distinctions. The design recurrence requires positive sample rates and assumes rational division/clamping, not arbitrary IEEE sample-rate admission. The stream theorem requires a zero-containing interval and finite valid state; no transcendental coefficient design, processing deadline or Rust artifact theorem is claimed.
Theorem: MaruLean.FilterContracts.tone_run_interval
Recorded axioms: propext, Classical.choice, Quot.sound
Manifest reviewed: 2026-11-08

Proved in exact arithmetic.The clamped coefficient model establishes interval preservation for arbitrary tone-frequency streams and positive sample rates in exact rational arithmetic.

Domain: Exact rational tone state and controls; finite positive sample rates for coefficient design; explicit coefficient and zero-containing 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 model includes the strict flush interval but omits binary64 rounding, NaN, infinity and signed-zero distinctions. The design recurrence requires positive sample rates and assumes rational division/clamping, not arbitrary IEEE sample-rate admission. The stream theorem requires a zero-containing interval and finite valid state; no transcendental coefficient design, processing deadline or Rust artifact theorem is claimed.
Theorem: MaruLean.FilterContracts.tone_designed_stream_interval
Recorded axioms: propext, Classical.choice, Quot.sound
Manifest reviewed: 2026-11-08

Proved in exact arithmetic.A constant tone state outside the flush interval is a fixed point in exact arithmetic.

Domain: Exact rational tone state and controls; finite positive sample rates for coefficient design; explicit coefficient and zero-containing 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 model includes the strict flush interval but omits binary64 rounding, NaN, infinity and signed-zero distinctions. The design recurrence requires positive sample rates and assumes rational division/clamping, not arbitrary IEEE sample-rate admission. The stream theorem requires a zero-containing interval and finite valid state; no transcendental coefficient design, processing deadline or Rust artifact theorem is claimed.
Theorem: MaruLean.FilterContracts.tone_normal_constant_fixed
Recorded axioms: propext, Classical.choice, Quot.sound
Manifest reviewed: 2026-11-08

Counterexample.A constant signal inside the flush interval is zeroed rather than remaining a fixed point.

Domain: Exact rational tone state and controls; finite positive sample rates for coefficient design; explicit coefficient and zero-containing 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 model includes the strict flush interval but omits binary64 rounding, NaN, infinity and signed-zero distinctions. The design recurrence requires positive sample rates and assumes rational division/clamping, not arbitrary IEEE sample-rate admission. The stream theorem requires a zero-containing interval and finite valid state; no transcendental coefficient design, processing deadline or Rust artifact theorem is claimed.
Theorem: MaruLean.FilterContracts.tone_small_constant_refuses_fixed
Recorded axioms: propext, Classical.choice, Quot.sound
Manifest reviewed: 2026-11-08