Build with this node

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

Ask Studio

@maruaudio/dsp/stereo/width scales the side signal of a stereo pair through a mid/side matrix:

M = (L + R)/2 S = (L − R)/2
L' = M + w·S R' = M − w·S

The setter folds this into two coefficients, same = (1 + w)/2 and cross = (1 − w)/2, so each output channel is L × same + R × cross (or the mirror). Width 0 is mono, 1 is an exact identity and 1.5 is the widest image. It also exports f32 mid/side encode and decode functions.

Parameters

SetterRange the setter enforcesDefault
setStereoWidth0 to 1.51 (identity)

midSideEncodeMid, midSideEncodeSide, midSideDecodeLeft and midSideDecodeRight take their samples as arguments and round to f32.

Lifecycle

initStereoWidthNode → setStereoWidth → stereoWidthLeft and stereoWidthRight per frame. There is no reset; the state holds only the width and its two coefficients. Sample operations allocate nothing and do no I/O.

When to use it

Narrowing a stereo source towards mono, widening it moderately, or converting to and from mid/side so another DSP node can process the two parts separately. The effects inventory lists the multi-effect's M/S Encoder slot against this DSP node.

Limits

  • Stereo in, stereo out, one frame per call; the two channel functions read the same coefficients.
  • The width operations are double multiplies with no rounding; the mid/side functions round to f32.
  • Width 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.

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.

9 Lean 4 results: 9 proofs in exact arithmetic.

Proved in exact arithmetic.Stereo width one preserves both channel values in exact arithmetic.Exact rational channel samples; width = 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.width_unity
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.Stereo width zero sends the same arithmetic mean to both channels.Exact rational channel samples; width = 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.width_zero_mono
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The stereo width matrix preserves the mid signal at every width.Exact rational channel samples and width
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.width_mid_preserved
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Show 6 more Lean 4 results
Proved in exact arithmetic.The stereo width matrix scales the channel difference by the width coefficient.Exact rational channel samples and width
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.width_side_scaled
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The stereo arithmetic mean stays inside the common interval of its input channels.Exact rationals; ordered finite bounds and stated coefficient guards
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.mono_bounded
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.Matched mid/side encoding and decoding recover both input channels in exact arithmetic.Exact rational channel samples; rounding treated as identity
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.mid_side_roundtrip
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The stereo width matrix cannot increase total squared-channel energy whenever w²<=1.Ordered field; arbitrary left/right samples and width with w²<=1.
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 proves a signal-energy inequality, not a loudness or sound-quality judgment. The width setter and per-operation rounding are not assumed to satisfy additional properties.
  • This record also covers MaruLean.SignalBounds.width_energy_identity, MaruLean.SignalBounds.width_energy_change; axioms describe MaruLean.SignalBounds.width_energy_nonincreasing only.
Theorem
MaruLean.SignalBounds.width_energy_nonincreasing
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.The width matrix has squared-energy gain at most K whenever K>=1 and K>=w²; common and opposite channel modes attain the gains 1 and w².Ordered field; arbitrary channel samples and width; K>=1 and K>=w².
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 common/side mode equalities establish the sharp modal gains. This is exact linear algebra; it does not measure perceived loudness or prove floating-point bit identity.
  • This record also covers MaruLean.SignalBounds.width_common_mode, MaruLean.SignalBounds.width_side_mode_energy; axioms describe MaruLean.SignalBounds.width_energy_gain_bound only.
Theorem
MaruLean.SignalBounds.width_energy_gain_bound
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.Amplitude-normalized mid/side encoding has exactly half the input stereo squared-channel energy.Ordered field; M=(L+R)/2 and S=(L-R)/2; arbitrary channel samples.
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 source rounds the encoded values to binary32; this identity omits those rounding boundaries. It describes amplitude normalization rather than a unit-energy normalization.
Theorem
MaruLean.SignalBounds.mid_side_energy
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Explore proofs alongside performance

Parameters

ParameterTypeSetter
Width widthfloatsetStereoWidth

Dependencies

None: this node imports no other node.

Dependents

Used by