Canonical f32 RBJ biquad state, coefficient design, tick and reset semantics for the seven kernel filter types.

Build with this node

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

Ask Studio

Editable example

Connect a biquad filter to a gain stage. Open the complete project in Studio to edit the composition, adjust Tone and Level, and save your own version.

Biquad and gain
src/index.tsTypeScript
import maruProjectConfig from "../maru.config.json";
import { defineEffect } from "maruaudio/audio/define"
import { nodes } from "maruaudio/audio/graph";
export const AUDIO_MODULE = defineEffect({
    id: "music.example.sdk-graph-effect",
    name: "SDK Graph Effect",
    vendor: "Example Audio",
    version: maruProjectConfig.version,
    schema: {
        params: [
            {
                path: "tone",
                label: "Tone",
                group: "Main",
                type: "float",
                min: 80,
                max: 12000,
                default: 2400,
                units: "Hz",
            },
            {
                path: "level",
                label: "Level",
                group: "Main",
                type: "float",
                min: 0,
                max: 1,
                default: 0.8,
            },
        ],
    },
    ui: {
        entry: "./ui/index.tsx",
        minSize: { width: 320, height: 360 },
        defaultSize: { width: 720, height: 520 },
        maxSize: { width: 1200, height: 900 },
        hostCapabilities: { optional: ["app.generation/v1"] },
    },
}, ({ input, output, connect, expose }) => {
    const filter = nodes.biquad("filter", {
        type: 0,
        frequency: 2400,
        q: 0.7,
        gainDb: 0,
    });
    const gain = nodes.gain("gain", { gain: 0.8 });
    connect(input.output, filter.audioInput);
    connect(filter.audioOutput, gain.audioInput);
    connect(gain.audioOutput, output.input);
    expose("tone", filter.params.frequency);
    expose("level", gain.params.gain);
});

@maruaudio/dsp/filters/biquad is a second-order IIR filter with RBJ Audio EQ Cookbook coefficients, run in transposed direct form II. It filters one mono signal, one sample per biquadNodeTick call. Coefficients, outputs and state are rounded to 32-bit floats (Math.fround).

const state = initBiquadNode(48000)
setBiquadNodeType(state, BIQUAD_LOWPASS)
setBiquadNodeFrequency(state, 1200)
updateBiquadNodeCoefficients(state) // before the next tick
const y = biquadNodeTick(state, x)

Parameters

SetterRange the setter enforcesDefault
setBiquadNodeTypeRounded, then 0 to 6: BIQUAD_LOWPASS, HIGHPASS, BANDPASS, NOTCH, PEAKING, LOWSHELF, HIGHSHELFLow-pass
setBiquadNodeFrequency10 Hz to 0.45 × the sample rate1000 Hz
setBiquadNodeQ0.0001 to 400.7071
setBiquadNodeGainDb−24 to +24 dB; read by peaking and shelf types only0 dB

Band-pass has a constant 0 dB peak; gain enters as 10^(dB/40) (math/decibels).

Lifecycle

initBiquadNode → setters → updateBiquadNodeCoefficients → biquadNodeTick → resetBiquadNode. Setters only store values; a new state passes its input through until the coefficients are updated. prepareBiquadNodeSampleRate sets a new rate and clamps the stored frequency to its ceiling; update the coefficients again before the next tick. resetBiquadNode clears the two state words and keeps the settings. Ticks allocate nothing and do no I/O. The update calls cos, sin and pow, so run it when a parameter changes, not per sample.

When to use it

One fixed or occasionally retuned second-order filter per channel, with one state per channel: a tone control, an EQ band, a notch, a shelf. The leaf catalog lists filters/parametric-eq (a fused EQ with transitions) and filters/state-variable (a TPT filter).

Limits

  • Mono sample tick, not a block Processor.
  • Coefficient changes apply at once, with no smoothing.
  • The clamp is the kernel node's conditional clamp, not the math/range policy: a NaN passes through unchanged.
  • A frequency clamped at a low rate stays clamped at a higher one until set again.

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.

22 Lean 4 results: 4 proofs in their stated domains; 9 proofs in exact arithmetic; 1 refused rewrite; 8 counterexamples.

Proved in exact arithmetic.Direct form I and transposed direct form II give the same output on every input, for every coefficient set and related start state.exact arithmetic over any commutative ring
Limits and assumptions
  • Not a theorem about floats, which are not a ring, so it says nothing about bit-exact output; the measured output of the two forms differs, by at most 2.5e-15 on the bench input.
  • This record also covers MaruLean.BiquadForms.step_related; axioms describe MaruLean.BiquadForms.run_eq only.
Theorem
MaruLean.BiquadForms.run_eq
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Rewrite refused.Computing Math.fround(a * b + c), the biquadOutput shape, entirely in binary32 gives different bits from double arithmetic rounded once, so an all-f32 biquad is a sound change and not a lowering.binary32 and binary64, one concrete input
Limits and assumptions
  • One witness; native_decide puts the Lean compiler and Float runtime in the trusted base. Whether an all-f32 filter is acceptable as a sound change is a design decision () for measurement and listening, not for this proof.
Theorem
MaruLean.FloatRefusals.all_f32_refused
Recorded axioms
propext, Classical.choice, Quot.sound, FloatRefusals.all_f32_refused._native.native_decide.ax_1_1
Manifest reviewed
Proved in the stated domain.In the hand-counted model, the transposed direct form II biquad kernel uses no more of any operation than the direct form I kernel.counting model
Limits and assumptions
  • Hand-counted source-level operations for the C kernels in bench/kernels.c, with no pipeline, vectorizer, cache or branch predictor; measurement decides speed, and the C control measured no clear difference between the two forms.
  • Axioms are not pinned by a #guard_msgs check; `#print axioms` output is unguarded.
Theorem
MaruLean.CostModel.tdf2_dominates_df1
Manifest reviewed
Show 19 more Lean 4 results
Proved in exact arithmetic.The lowpass, highpass, bandpass and notch coefficients of biquad.ts satisfy the Jury conditions, so their exact poles lie strictly inside the unit circle.exact arithmetic in any ordered field, with -1 < cos w0 < 1 and 0 < alpha assumed
Limits and assumptions
  • Exact arithmetic in an ordered field, with the trigonometry assumed: the code rounds the cosine to binary32 first, and the binary32 rounding of a1 and a2 is where the filter really fails, so this does not protect the shipped code (). Frozen settings only; a moving cutoff is a different question.
  • This record also covers MaruLean.FilterStability.rbj_dPlus, MaruLean.FilterStability.rbj_dMinus, MaruLean.FilterStability.jury_real_root, MaruLean.FilterStability.jury_complex_root, MaruLean.FilterStability.w0_in_open_half_turn; axioms describe MaruLean.FilterStability.rbj_jury only.
Theorem
MaruLean.FilterStability.rbj_jury
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The peaking coefficients of biquad.ts satisfy the Jury conditions for every positive gain.exact arithmetic in any ordered field, with -1 < cos w0 < 1, 0 < alpha and 0 < A assumed
Limits and assumptions
  • Exact arithmetic in an ordered field, with the trigonometry assumed: the code rounds the cosine to binary32 first, and the binary32 rounding of a1 and a2 is where the filter really fails, so this does not protect the shipped code (). Frozen settings only; a moving cutoff is a different question.
Theorem
MaruLean.FilterStability.peak_jury
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The low and high shelf coefficients of biquad.ts satisfy the Jury conditions, and each shelf is the shared denominator with a cosine moved toward 1 by a boost.exact arithmetic in any ordered field, with -1 < cos w0 < 1, 0 < A and 0 < beta assumed
Limits and assumptions
  • Exact arithmetic in an ordered field, with the trigonometry assumed: the code rounds the cosine to binary32 first, and the binary32 rounding of a1 and a2 is where the filter really fails, so this does not protect the shipped code (). Frozen settings only; a moving cutoff is a different question.
  • This record also covers MaruLean.FilterStability.highShelf_jury, MaruLean.FilterStability.lowShelf_a0_pos, MaruLean.FilterStability.lowShelf_eq_rbj, MaruLean.FilterStability.highShelf_eq_lowShelf; axioms describe MaruLean.FilterStability.lowShelf_jury only.
Theorem
MaruLean.FilterStability.lowShelf_jury
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Counterexample.If rounding sends the cosine to exactly 1, the exact margin at z = 1 is zero whatever the Q, so the pole is on the unit circle.exact arithmetic in any ordered field, cosine exactly 1
Limits and assumptions
  • Shows that the clamps do not give the hypothesis the stability theorems need for the value the code actually uses; the code's binary32 cosine reaches 1 at 10 Hz above about 257 kHz.
Theorem
MaruLean.FilterStability.rbj_dPlus_at_cos_one
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.Rounded coefficients still satisfy the Jury conditions when each exact margin is larger than the rounding movement it can suffer.exact arithmetic in any ordered field, with a stated rounding budget
Limits and assumptions
  • The budget is a stated bound on the code, not something proved about its floats; at low frequency the margin at z = 1 is the hard one and real settings break it.
  • This record also covers MaruLean.FilterStability.jury_of_budget; axioms describe MaruLean.FilterStability.rbj_rounded_jury only.
Theorem
MaruLean.FilterStability.rbj_rounded_jury
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.If the denominator polynomial is not positive at some g above 1 and a2 is non-negative, the free recursion grows at least like g^n.exact arithmetic in any ordered field
Limits and assumptions
  • A lower bound on growth in exact arithmetic; the real rounded filter is measured by bench/filter-stability-sweep.mjs.
  • This record also covers MaruLean.FilterStability.freeRun_ratio; axioms describe MaruLean.FilterStability.freeRun_grows only.
Theorem
MaruLean.FilterStability.freeRun_grows
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Counterexample.At 384 kHz, 10 Hz and Q 1, the coefficients the real setter stores for the shared RBJ denominator fail the Jury conditions with a margin of -2^-24, and their free recursion grows at least like 1.0001^n.exact rational arithmetic on the real stored binary32 coefficients
Limits and assumptions
  • The coefficients are recomputed from the real function by bench/filter-stability-witnesses.mjs; the growth bound is a lower bound, and the real filter overflows sooner, in about 1.4 seconds.
  • This record also covers MaruLean.FilterStability.w384_dPlus, MaruLean.FilterStability.w384_grows; axioms describe MaruLean.FilterStability.w384_rounded_not_jury only.
Theorem
MaruLean.FilterStability.w384_rounded_not_jury
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Counterexample.A low shelf at 192 kHz, 11.27 Hz, Q 0.0139 and +24 dB is stable with exact coefficients, and rounding each to the nearest binary32 breaks the Jury conditions so the filter grows.exact rational arithmetic on the real cosine, beta and stored binary32 coefficients
Limits and assumptions
  • One real setting; the exact theorem is true and does not protect the code. Which modules reach this setting is not shown here.
  • This record also covers MaruLean.FilterStability.w192_exact_jury, MaruLean.FilterStability.w192_rounding_is_small, MaruLean.FilterStability.w192_grows; axioms describe MaruLean.FilterStability.w192_rounded_not_jury only.
Theorem
MaruLean.FilterStability.w192_rounded_not_jury
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Counterexample.A peaking filter at 96 kHz, 10 Hz, Q 0.0001 and -23.5 dB is stable with exact coefficients, and the rounded pair puts a pole exactly at z = 1.exact rational arithmetic on the real stored binary32 coefficients
Limits and assumptions
  • One real setting; which modules reach it is not shown here.
  • This record also covers MaruLean.FilterStability.w96_exact_jury, MaruLean.FilterStability.w96_pole_at_one; axioms describe MaruLean.FilterStability.w96_rounded_not_jury only.
Theorem
MaruLean.FilterStability.w96_rounded_not_jury
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.Direct form I has the same trace and determinant as the shipped transposed form under any two-setting alternation, so switching form does not escape alternation growth.exact arithmetic over any commutative ring
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.
  • Axioms are not pinned by a #guard_msgs check; `#print axioms` output is unguarded.
Theorem
MaruLean.ModulationStability.df1_same_alternation
Manifest reviewed
Counterexample.Two real binary32 biquad settings at 48 kHz and Q 0.7071, 9847.8 Hz and 20 kHz, are each stable when frozen, and alternating them on every sample grows.exact rational arithmetic on the real stored binary32 coefficients, no input
Limits and assumptions
  • One pair of settings in exact arithmetic; the biquad's modulation limit is measured, not proved.
  • Axioms are not pinned by a #guard_msgs check; `#print axioms` output is unguarded.
  • This record also covers MaruLean.ModulationStability.witness_fast_frozen_stable; axioms describe MaruLean.ModulationStability.witness_fast_grows only.
Theorem
MaruLean.ModulationStability.witness_fast_grows
Manifest reviewed
Counterexample.Moving a Q 5 biquad at 48 kHz by one octave around 100 Hz, holding each setting for 109 samples, grows although each setting is stable when frozen.exact rational arithmetic on the real stored binary32 coefficients, no input
Limits and assumptions
  • One pattern in exact arithmetic, checked with native_decide, which trusts the Lean compiler; the real tick's runaway is measured, not proved, and the biquad's modulation limit is measured, not proved.
  • Axioms are not pinned by a #guard_msgs check; `#print axioms` output is unguarded.
  • This record also covers MaruLean.ModulationStability.witness_low_frozen_stable; axioms describe MaruLean.ModulationStability.witness_low_grows only.
Theorem
MaruLean.ModulationStability.witness_low_grows
Manifest reviewed
Proved in exact arithmetic.At a fixed point of the rounded biquad tick on a constant input, the output misses the exact answer by the sum of the three rounding errors divided by 1 + a1 + a2.exact arithmetic in an ordered field
Limits and assumptions
  • Nothing connects the values to IEEE rounding beyond real-dc-check.mjs and the half-unit checks in the file.
  • Axioms are not pinned by a #guard_msgs check; `#print axioms` output is unguarded.
Theorem
MaruLean.ErrorBounds.stuck_offset
Manifest reviewed
Counterexample.Real stuck states of the biquad lowpass at 10 Hz and 96 kHz, and at 20 Hz and 48 kHz, miss the exact constant-input answer by more than 0.03 and 0.0028, and the offset comes only from rounding.exact rational arithmetic on real stored binary32 states and coefficients
Limits and assumptions
  • Which modules reach these settings, and whether the offset is audible, is unknown; the numbers are checked against the real code by real-dc-check.mjs, not proved about it.
  • Axioms are not pinned by a #guard_msgs check; `#print axioms` output is unguarded.
  • This record also covers MaruLean.ErrorBounds.w10_offset, MaruLean.ErrorBounds.w20_offset, MaruLean.ErrorBounds.w20_offset_is_rounding; axioms describe MaruLean.ErrorBounds.w10_offset_is_rounding only.
Theorem
MaruLean.ErrorBounds.w10_offset_is_rounding
Manifest reviewed
Proved in the stated domain.Over Float, the biquad tick built from Lean generated from Maru compiler IR of biquad.ts is definitionally the hand-written fround model in BiquadForms.lean.every Float input, with fround opaque and the same on both sides
Limits and assumptions
  • The tick composition itself is written by hand, because the translator refuses biquadNodeTick; the translator covers only 7.7% of MultiFX hot-path nodes so far.
Theorem
IrToLean.Proof.tick_float_is_hand_model
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The biquad arithmetic generated from biquad.ts gives the direct form I output for any coefficients, input and related start state.exact arithmetic over any commutative ring, fround as the identity
Limits and assumptions
  • Says nothing about rounding, and floats are not a ring.
  • This record also covers IrToLean.Proof.tick_exact_is_tdf2, IrToLean.Proof.run_exact_is_tdf2; axioms describe IrToLean.Proof.run_exact_eq_df1 only.
Theorem
IrToLean.Proof.run_exact_eq_df1
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Counterexample.The clamp in filters/biquad.ts keeps -0 with bounds [0, 1], while the clamp in math/range.ts gives +0.one concrete binary64 input, compared by bits
Limits and assumptions
  • One input; whether either difference is reachable or audible in a module is not shown.
Theorem
IrToLean.Proof.clamps_disagree_on_negative_zero
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in the stated domain.The real clamp from biquad.ts returns one of its arguments bit for bit, whatever they are.every Float and every instance of the comparison class, with no arithmetic
Limits and assumptions
  • It holds on the running type only because it does no arithmetic; it does not say which argument comes back for -0, which differs between clamps.
Theorem
IrToLean.Proof.clamp_returns_an_input
Recorded axioms
propext
Manifest reviewed
Proved in the stated domain.One concrete biquadOutput generated from Maru compiler IR gives the expected bits, on Lean's Float model with froundModel and through the compiler.one concrete binary64 input
Limits and assumptions
  • A single test vector; the model form trusts this package's froundModel, and the native form trusts the Lean compiler through native_decide.
  • This record also covers IrToLean.Proof.biquadOutput_vector_native; axioms describe IrToLean.Proof.biquadOutput_vector_model only.
Theorem
IrToLean.Proof.biquadOutput_vector_model
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Explore proofs alongside performance

Parameters

ParameterTypeSetter
Type typefloatsetBiquadNodeType
Frequency frequencyfloatsetBiquadNodeFrequency
Q qfloatsetBiquadNodeQ
Gain db gainDbfloatsetBiquadNodeGainDb

Ports

  • In ininput · audio · mono
  • Out outoutput · audio · mono

One sample per biquadNodeTick call.

Dependencies

Dependents

Used by