Performance

No benchmarks published

No timing measurements are published for this node.
View target support

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.

Counterexample.The clamp in filters/biquad.ts keeps -0 with bounds [0, 1], while the clamp in math/range.ts gives +0.
Domain
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 exact arithmetic.Nested minimum/maximum and the conditional clamp agree over exact values when the bounds are ordered.
Domain
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.minmax_clamp_eq
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.Clamping places every exact value inside its ordered inclusive bounds.
Domain
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.clamp_bounded
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.An exact value already inside the clamp interval is unchanged.
Domain
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.clamp_fixed
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Proved in exact arithmetic.Clamping an exact value twice gives the same result as clamping it once.
Domain
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.clamp_idempotent
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed