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.

2 Lean 4 results: 1 proof in exact arithmetic; 1 refused rewrite.

Proved in exact arithmetic.Two successive scalar gains can be combined algebraically in exact arithmetic.
Domain
Exact rational input and gain coefficients
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.gain_fusion_exact
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed
Rewrite refused.Fusing two small gains can underflow their product to zero while sequential gains keep a nonzero output.
Domain
One finite IEEE binary64 witness; input 2^600 and both gains 2^-600
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. One concrete witness; it refutes the stated unrestricted claim, not every possible guarded implementation.
Theorem
MaruLean.LeafContracts.gain_fusion_refused_on_float
Recorded axioms
propext, Classical.choice, Quot.sound
Manifest reviewed