Build with this node

Start with a prompt in Studio, or copy it into your own coding agent.

Ask Studio

@maruaudio/dsp/filters/one-pole holds the stateless pieces of a one-pole low-pass, y[n] = y[n-1] + a·(x[n] − y[n-1]): two ways to turn a cutoff into the coefficient a, and the per-sample update. The caller owns the state, a double accumulator that is never rounded to f32. The chain and @maruaudio/filters-tone both call these functions.

const a = onePoleLowpassCoefficient(5000, 48000) // once, outside the loop
let y = 0
y = onePoleLowpassTick(y, x, a) // per sample

Parameters

This DSP node has no setters; cutoff and rate are passed to the coefficient functions, and state, input and coefficient to the tick.

FunctionMapping and bounds as codedUnit
toneFilterCoefficient(toneHz, sampleRate)toneHz / sampleRate, conditionally clamped to 0.001 to 1Hz in, coefficient out
onePoleLowpassCoefficient(cutoffHz, sampleRate)Exact digital −3 dB cutoff: sqrt(y² + 2y) − y with y = 2·sin²(π·fc/fs); cutoff clamped to 0 to NyquistHz in, coefficient out
onePoleLowpassTick(state, input, coefficient)Returns the new statesample

Lifecycle

No instance state: derive the coefficient when cutoff or rate changes, tick once per sample keeping the return value as the state, and set it to 0 to reset.

When to use it

A gentle treble roll-off or a smoothing stage inside a larger DSP node. Use onePoleLowpassCoefficient when the cutoff must mean an actual −3 dB frequency; toneFilterCoefficient is the legacy mapping that keeps the chain's bytes.

Limits

  • Mono, one sample per call; first order only.
  • toneFilterCoefficient uses a conditional clamp, not the @maru/math-range policy, so a NaN passes through it.
  • onePoleLowpassCoefficient returns 0 for a non-finite cutoff or a rate that is not finite and positive, and 2·(√2 − 1) at Nyquist, which is still −3 dB rather than bypass.
  • The tick flushes results whose magnitude is below the smallest normal f32 (about 1.18e−38) to zero, so a decaying state never emits subnormal samples.

Algorithm properties and proofs

Lean 4 checks specific properties of this algorithm’s mathematical model. Each model result applies within its stated domain and assumptions.

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

Proved in the stated domain.One concrete onePoleLowpassTick generated from Maru compiler IR gives the bits Node gives.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.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.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
Show 3 more Lean 4 results
Proved in exact arithmetic.Flush-to-zero cannot increase squared sample energy and preserves the one-pole stream bound whenever the interval contains zero.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.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.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
Explore proofs alongside performance

Dependencies

Dependents

Used by