TorchLean

8.2. Floating-Point Numerics🔗

The numerical map starts with FloatLib's generic formats and configured executable scalars. TorchLean keeps two binary32 specializations in view: FP32 is the imported rounded-real model with binary32's gradual-underflow grid; ExecFloat.Binary 8 23 includes signed zeros, infinities, and NaNs. Bridge theorems connect their finite cases. TorchLean's runtime-approximation layer then composes local operator bounds over whole forward and backward graphs. Other configured widths share FloatLib's public scalar API, while a network error bound must still use the format and operation sequence actually selected.

Definition8.2.1
Group: Generic formats, rounding, and quantization. (6)
Group member previews
Preview
Definition 8.2.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

FloatRep stores an integer mantissa and exponent at a chosen radix. Its real interpretation is the exact value of that pair.

Lean code for Definition8.2.1●1 definition
  • structure(2 fields)defined in FloatLib/Floats/Formats/Flocq/Theory/Core.lean
    complete
    structure FloatLib.Floats.Formats.Flocq.FloatRep (β : FloatLib.Numerics.Radix) :
  Type
    structure FloatLib.Floats.Formats.Flocq.FloatRep
  (β : FloatLib.Numerics.Radix) : Type
    A radix-$\beta$ floating-point representation with integer mantissa and exponent.

    Fields

    mantissa : ℤ
    Integer mantissa `m`. 
    exponent : ℤ
    Integer exponent `e`.
Definition8.2.2
Group: Generic formats, rounding, and quantization. (6)
Group member previews
Preview
Definition 8.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

genericFormat says when a real number belongs to the grid selected by a radix and a valid exponent policy. Fixed, unbounded, and gradual-underflow formats are instances of this setup.

Lean code for Definition8.2.2●1 definition
  • defdefined in FloatLib/Floats/Formats/Flocq/Theory/Core.lean
    complete
    def FloatLib.Floats.Formats.Flocq.genericFormat
  (β : FloatLib.Numerics.Radix) (fexp : ℤ → ℤ)
  [FloatLib.Floats.Formats.Flocq.ValidExp fexp] (x : ℝ) : Prop
    def FloatLib.Floats.Formats.Flocq.genericFormat
  (β : FloatLib.Numerics.Radix)
  (fexp : ℤ → ℤ)
  [FloatLib.Floats.Formats.Flocq.ValidExp
      fexp]
  (x : ℝ) : Prop
    Generic format predicate (Flocq-style).

This says that $x$ is exactly representable in the format picked out by $\beta$ and `fexp`.
One way to read it is: the scaled mantissa is an integer (so there is no rounding error).
Definition8.2.3
Group: Generic formats, rounding, and quantization. (6)
Group member previews
Preview
Definition 8.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0
Used by 2
Reverse dependency previews
Preview
Theorem 8.2.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

ValidRndToNearest is the contract required of an integer rounding rule: it is monotone, fixes integers, and stays within one half of its input.

Lean code for Definition8.2.3●1 definition
  • class(extends 1, 3 methods)defined in FloatLib/Floats/Formats/Flocq/Theory/Rounding/Core.lean
    complete
    class FloatLib.Floats.Formats.Flocq.ValidRndToNearest (rnd : ℝ → ℤ) : Prop
    class FloatLib.Floats.Formats.Flocq.ValidRndToNearest
  (rnd : ℝ → ℤ) : Prop
    Rounding modes with a half-unit error bound on the rounded integer.

This matches "round-to-nearest" style roundings (ties can be resolved arbitrarily):
`|rnd x - x| ≤ 1/2` for all `x`.

    Extends

    • FloatLib.Floats.Formats.Flocq.ValidRnd rnd

    Methods

    monotone : ∀ (x y : ℝ), x ≤ y → rnd x ≤ rnd y
    Inherited from
    1. FloatLib.Floats.Formats.Flocq.ValidRnd
    id : ∀ (n : ℤ), rnd ↑n = n
    Inherited from
    1. FloatLib.Floats.Formats.Flocq.ValidRnd
    abs_sub_le_half : ∀ (x : ℝ), |↑(rnd x) - x| ≤ 2⁻¹
    Rounding changes a real input by at most one half on the integer grid.
Definition8.2.4
Group: Generic formats, rounding, and quantization. (6)
Group member previews
Preview
Definition 8.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 8.2.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

round scales at the canonical exponent, applies its supplied integer rounding rule, and maps the resulting mantissa/exponent pair back to a real value. Nearestness and tie handling come from that supplied rule.

The scale is selected from the input magnitude before integer rounding. Separating these choices lets the same format support nearest and directed modes; a nearest-error theorem cannot be transferred to a directed mode merely because their representable values coincide.

Lean code for Definition8.2.4●1 definition
  • defdefined in FloatLib/Floats/Formats/Flocq/Theory/Rounding/Core.lean
    complete
    def FloatLib.Floats.Formats.Flocq.round {β : FloatLib.Numerics.Radix}
  {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp]
  (rnd : ℝ → ℤ) (x : ℝ) : ℝ
    def FloatLib.Floats.Formats.Flocq.round
  {β : FloatLib.Numerics.Radix}
  {fexp : ℤ → ℤ}
  [FloatLib.Floats.Formats.Flocq.ValidExp
      fexp]
  (rnd : ℝ → ℤ) (x : ℝ) : ℝ
    Round the scaled mantissa to an integer, then reconstruct the value at the canonical exponent
of the input.
Theorem8.2.5
Group: Generic formats, rounding, and quantization. (6)
Group member previews
Preview
Definition 8.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 8.2.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

When its integer rule satisfies the nearest-rounding contract, generic grid rounding is within half an ULP.

Lean code for Theorem8.2.5●1 theorem
  • theoremdefined in FloatLib/Floats/Formats/Flocq/Theory/Rounding/Core.lean
    complete
    theorem FloatLib.Floats.Formats.Flocq.error_bound_ulp
  {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ}
  [FloatLib.Floats.Formats.Flocq.ValidExp fexp] (rnd : ℝ → ℤ)
  [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] (x : ℝ) :
  |FloatLib.Floats.Formats.Flocq.round rnd x - x| ≤
    FloatLib.Floats.Formats.Flocq.ulp β fexp x / 2
    theorem FloatLib.Floats.Formats.Flocq.error_bound_ulp
  {β : FloatLib.Numerics.Radix}
  {fexp : ℤ → ℤ}
  [FloatLib.Floats.Formats.Flocq.ValidExp
      fexp]
  (rnd : ℝ → ℤ)
  [FloatLib.Floats.Formats.Flocq.ValidRndToNearest
      rnd]
  (x : ℝ) :
  |FloatLib.Floats.Formats.Flocq.round rnd
          x -
        x| ≤
    FloatLib.Floats.Formats.Flocq.ulp β
        fexp x /
      2
    Half-ULP error bound for `round` under round-to-nearest.

This is the basic “one-step” bound used by most error propagation arguments:
`round` deviates from `x` by at most half an ulp at the chosen exponent scale.
Proof for Theorem 8.2.5
Proof uses 2
Proof dependency previews
Preview
Definition 8.2.3
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

The proof applies the half-integer error bound to the scaled mantissa, then rescales it at the exponent used by the grid rounder.

Definition8.2.6
Group: Generic formats, rounding, and quantization. (6)
Group member previews
Preview
Definition 8.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

A bounded affine quantizer records its positive scale, zero point, and nonempty integer code range. Its quantize operation accepts the integer rounding rule separately.

Lean code for Definition8.2.6●1 definition
  • structure(6 fields)defined in FloatLib/Numerics/Quantization/Affine/Real.lean
    complete
    structure FloatLib.Numerics.Quantization.RealAffineQuantizer : Type
    structure FloatLib.Numerics.Quantization.RealAffineQuantizer :
  Type
    A bounded affine grid with real-valued spacing and caller-supplied integer rounding.

    Fields

    scale : ℝ
    Distance between adjacent reconstructed values. 
    zeroPoint : ℤ
    Integer code whose reconstruction is zero. It need not be inside the storage interval. 
    qmin : ℤ
    Smallest stored code. 
    qmax : ℤ
    Largest stored code. 
    scale_pos : 0 < self.scale
    The grid spacing is strictly positive. 
    codeRange : self.qmin ≤ self.qmax
    The storage interval is nonempty.
Theorem8.2.7
Group: Generic formats, rounding, and quantization. (6)
Group member previews
Preview
Definition 8.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 8.2.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

An unclipped value passed through the affine quantizer reconstructs within half a scale step when its integer rule satisfies the nearest-rounding contract.

The unclipped hypothesis says that the rounded code lies inside the allowed integer range. It is needed because saturation can introduce an error larger than the half-step rounding budget.

Lean code for Theorem8.2.7●1 theorem
  • theoremdefined in FloatLib/Floats/Formats/Flocq/Theory/Rounding/Affine.lean
    complete
    theorem FloatLib.Floats.Formats.Flocq.affine_dequantize_quantize_error_le_half
  (q : FloatLib.Numerics.Quantization.RealAffineQuantizer) (rnd : ℝ → ℤ)
  [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] (x : ℝ)
  (hlo : q.qmin ≤ q.rawCode rnd x) (hhi : q.rawCode rnd x ≤ q.qmax) :
  |q.roundedValue rnd x - x| ≤ q.scale / 2
    theorem FloatLib.Floats.Formats.Flocq.affine_dequantize_quantize_error_le_half
  (q :
    FloatLib.Numerics.Quantization.RealAffineQuantizer)
  (rnd : ℝ → ℤ)
  [FloatLib.Floats.Formats.Flocq.ValidRndToNearest
      rnd]
  (x : ℝ) (hlo : q.qmin ≤ q.rawCode rnd x)
  (hhi : q.rawCode rnd x ≤ q.qmax) :
  |q.roundedValue rnd x - x| ≤ q.scale / 2
    Without saturation, every valid nearest rounder reconstructs within half a grid step.
Proof for Theorem 8.2.7
Proof uses 2
Proof dependency previews
Preview
Definition 8.2.3
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

The proof applies the half-integer error bound before multiplying by the positive scale from the quantizer.

Definition8.2.8
Group: Proof-oriented and executable accounts of IEEE 754 binary32. (5)
Group member previews
Preview
Theorem 8.2.9
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 8.2.9
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

FP32 specializes the generic format theory to a proof-oriented nearest-even model over real values. It leaves out NaNs, infinities, and the upper exponent cutoff, so claims about those cases belong to FloatLib binary32.

Lean code for Definition8.2.8●1 definition
  • abbrevdefined in NN/Floats/FP32/Core.lean
    complete
    abbrev TorchLean.Floats.FP32 : Type
    abbrev TorchLean.Floats.FP32 : Type
    `FP32`: finite float32 rounding model, as a rounded real value.

This is the type you want if you are proving numerical stability/error bounds without dealing with
NaN/Inf behavior.
Theorem8.2.9
Group: Proof-oriented and executable accounts of IEEE 754 binary32. (5)
Group member previews
Preview
Definition 8.2.8
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

Rounding in the rounded-real model differs from its real input by at most half an ULP.

Lean code for Theorem8.2.9●1 theorem
  • theoremdefined in NN/Floats/FP32/Error.lean
    complete
    theorem TorchLean.Floats.FP32.round_abs_error (x : ℝ) :
  |TorchLean.Floats.round32 x - x| ≤ TorchLean.Floats.eps32 x
    theorem TorchLean.Floats.FP32.round_abs_error
  (x : ℝ) :
  |TorchLean.Floats.round32 x - x| ≤
    TorchLean.Floats.eps32 x
    Core rounding lemma for the binary32 parameters fixed by `FP32`.

This is the “one thing we use everywhere”: once you know an operation is defined as “round the real
result”, the proof goal reduces to an instance of this lemma.

Informal: if `fl32(x)` denotes rounding `x : ℝ` to the binary32 grid, then
$|\operatorname{fl}_{32}(x)-x|\le\varepsilon_{32}(x)$.
Proof for Theorem 8.2.9
Proof uses 2
Proof dependency previews
Preview
Theorem 8.2.5
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

Unfolding binary32 rounding exposes the generic real-valued rounder with binary32's exponent policy and nearest-even integer rounding. The generic half-ULP theorem then supplies the error bound.

Definition8.2.10
Group: Proof-oriented and executable accounts of IEEE 754 binary32. (5)
Group member previews
Preview
Definition 8.2.8
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0
Used by 5
Reverse dependency previews
Preview
Theorem 8.2.11
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Choose exponent and fraction widths in FloatLib's configured binary constructor. The 8, 23 configuration is binary32; wider and custom formats use the same interface. Encodings drive executable addition, multiplication, division, fused multiply-add, and square root, with explicit rounding modes and operation-specific exception status.

Lean code for Definition8.2.10●1 definition
  • abbrevdefined in FloatLib/Floats/Formats/BinaryInterchange/Configured/Type.lean
    complete
    abbrev FloatLib.Floats.ExecFloat.Binary (exponentBits fractionBits : ℕ)
  (encoding : FloatFormat.Encoding := FloatFormat.Encoding.ieee)
  (bias : ℕ := encoding.defaultBias exponentBits)
  (exponentBits_ge_two : 2 ≤ exponentBits := by
    first
    | decide
    | fail "ExecFloat.Binary requires exponentBits ≥ 2")
  (fractionBits_pos : 0 < fractionBits := by
    first
    | decide
    | fail "ExecFloat.Binary requires fractionBits ≥ 1")
  (bias_pos : 0 < bias := by
    first
    | decide
    | fail "ExecFloat.Binary requires a positive exponent bias")
  (bias_le_maxFinite :
    bias ≤ encoding.maxFiniteExponent exponentBits := by
    first
    | decide
    |
      fail
        "ExecFloat.Binary requires bias ≤ encoding.maxFiniteExponent exponentBits") :
  Type
    abbrev FloatLib.Floats.ExecFloat.Binary
  (exponentBits fractionBits : ℕ)
  (encoding : FloatFormat.Encoding :=
    FloatFormat.Encoding.ieee)
  (bias : ℕ :=
    encoding.defaultBias exponentBits)
  (exponentBits_ge_two :
    2 ≤ exponentBits := by
    first
    | decide
    |
      fail
        "ExecFloat.Binary requires exponentBits ≥ 2")
  (fractionBits_pos :
    0 < fractionBits := by
    first
    | decide
    |
      fail
        "ExecFloat.Binary requires fractionBits ≥ 1")
  (bias_pos : 0 < bias := by
    first
    | decide
    |
      fail
        "ExecFloat.Binary requires a positive exponent bias")
  (bias_le_maxFinite :
    bias ≤
      encoding.maxFiniteExponent
        exponentBits := by
    first
    | decide
    |
      fail
        "ExecFloat.Binary requires bias ≤ encoding.maxFiniteExponent exponentBits") :
  Type
    An executable binary format selected directly by its numerical parameters.

The stored width is derived as `1 + exponentBits + fractionBits`; it is not a separate parameter
that can disagree with the layout. Storage and operation implementations are selected statically
from the resulting format.
Theorem8.2.11
Group: Proof-oriented and executable accounts of IEEE 754 binary32. (5)
Group member previews
Preview
Definition 8.2.8
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 8.2.8
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

On the stated finite-result path, executable addition agrees with rounded-real binary32 addition. Matching bridge theorems cover subtraction, multiplication, fused multiply-add, square root, and division.

Lean code for Theorem8.2.11●1 theorem
  • theoremdefined in NN/Floats/IEEEExec/Bridge/Finite.lean
    complete
    theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_add_eq_fp32Round_of_isFinite
  {x y :
    ExecFloat.Binary 8 23 FloatFormat.Encoding.ieee
      (FloatFormat.Encoding.ieee.defaultBias 8)
      TorchLean.Floats.IEEE754.IEEE32Exec.toModel_add._proof_1
      TorchLean.Floats.IEEE754.IEEE32Exec.toModel_add._proof_2
      TorchLean.Floats.IEEE754.IEEE32Exec.toModel_add._proof_3
      TorchLean.Floats.IEEE754.IEEE32Exec.toModel_add._proof_4}
  (hfin : ExecFloat.Binary.isFinite (ExecFloat.add x y) = true) :
  (ExecFloat.Binary.toModel (ExecFloat.add x y)).toReal =
    TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round
      ((ExecFloat.Binary.toModel x).toReal +
        (ExecFloat.Binary.toModel y).toReal)
    theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_add_eq_fp32Round_of_isFinite
  {x y :
    ExecFloat.Binary 8 23
      FloatFormat.Encoding.ieee
      (FloatFormat.Encoding.ieee.defaultBias
        8)
      TorchLean.Floats.IEEE754.IEEE32Exec.toModel_add._proof_1
      TorchLean.Floats.IEEE754.IEEE32Exec.toModel_add._proof_2
      TorchLean.Floats.IEEE754.IEEE32Exec.toModel_add._proof_3
      TorchLean.Floats.IEEE754.IEEE32Exec.toModel_add._proof_4}
  (hfin :
    ExecFloat.Binary.isFinite
        (ExecFloat.add x y) =
      true) :
  (ExecFloat.Binary.toModel
        (ExecFloat.add x y)).toReal =
    TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round
      ((ExecFloat.Binary.toModel
            x).toReal +
        (ExecFloat.Binary.toModel
            y).toReal)
    A finite executable sum is one binary32 rounding of the exact real sum.
Proof for Theorem 8.2.11
Proof uses 2
Proof dependency previews
Preview
Definition 8.2.8
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

The proof decodes finite operands to dyadics and identifies the bit-level result with nearest-even real rounding.

For a composed expression, each intermediate operation must meet the hypotheses of its bridge. Finite source tensors alone do not establish this: addition or multiplication of finite operands can overflow before the final output is formed.

Theorem8.2.12
Group: Proof-oriented and executable accounts of IEEE 754 binary32. (5)
Group member previews
Preview
Definition 8.2.8
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

For finite inputs, downward-rounded binary32 addition is no greater than the exact real sum, including overflow to negative infinity.

Lean code for Theorem8.2.12●1 theorem
  • theoremdefined in FloatLib/Floats/Formats/BinaryInterchange/DirectedSemantics/Addition.lean
    complete
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_addDown_le
  {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true)
  (hx : x.isFinite = true) (hy : y.isFinite = true) :
  (x.addDown y).toEReal ≤ ↑(x.toReal + y.toReal)
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_addDown_le
  {fmt : FloatFormat} (x y : Model fmt)
  (hfmt : fmt.isIEEE = true)
  (hx : x.isFinite = true)
  (hy : y.isFinite = true) :
  (x.addDown y).toEReal ≤
    ↑(x.toReal + y.toReal)
    Downward-rounded addition is a lower bound on exact real addition for finite operands.
Proof for Theorem 8.2.12
uses 1

The proof decodes the finite inputs to dyadics, computes their exact dyadic sum, and applies soundness of downward rounding in the extended reals.

Theorem8.2.13
Group: Proof-oriented and executable accounts of IEEE 754 binary32. (5)
Group member previews
Preview
Definition 8.2.8
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

For finite inputs, the exact real sum is no greater than upward-rounded binary32 addition, including overflow to positive infinity.

Lean code for Theorem8.2.13●1 theorem
  • theoremdefined in FloatLib/Floats/Formats/BinaryInterchange/DirectedSemantics/Addition.lean
    complete
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_toEReal_addUp
  {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true)
  (hx : x.isFinite = true) (hy : y.isFinite = true) :
  ↑(x.toReal + y.toReal) ≤ (x.addUp y).toEReal
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_toEReal_addUp
  {fmt : FloatFormat} (x y : Model fmt)
  (hfmt : fmt.isIEEE = true)
  (hx : x.isFinite = true)
  (hy : y.isFinite = true) :
  ↑(x.toReal + y.toReal) ≤
    (x.addUp y).toEReal
    Exact real addition is bounded above by upward-rounded addition for finite operands.
Proof for Theorem 8.2.13
uses 1

The proof decodes the finite inputs to their exact dyadic sum and applies soundness of upward rounding in the extended reals.

Extended-real endpoints allow these two directed statements to remain useful when a finite exact sum exceeds the largest binary32 value. A lower endpoint of negative infinity or an upper endpoint of positive infinity still gives a valid one-sided bound, although it may be too wide for a later verification claim. This differs from the finite refinement theorem, whose conclusion identifies a decoded result with rounded-real arithmetic and therefore needs its finite-path premise.

Theorem8.2.14
Group: Operator bounds composed across programs. (8)
Group member previews
Preview
Theorem 8.2.15
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N

Local approximation contracts over typed tensors compose through forward graph evaluation.

Lean code for Theorem8.2.14●1 theorem
  • theoremdefined in NN/Proofs/RuntimeApprox/Graph/ForwardApprox.lean
    complete
    theorem Proofs.RuntimeApprox.FwdGraph.eval_approx {α : Type}
  [TorchLean.Storage α] {toSpec : α → Spec.SpecScalar}
  {Γ ss : List Spec.Shape}
  (g : Proofs.RuntimeApprox.FwdGraph toSpec Γ ss)
  (xS : TorchLean.TensorPack Spec.SpecScalar Γ)
  (xR : TorchLean.TensorPack α Γ)
  (epsIn : Proofs.RuntimeApprox.EList Γ) :
  Proofs.RuntimeApprox.approxCtx toSpec xS xR epsIn →
    Proofs.RuntimeApprox.approxCtx toSpec (g.evalSpec xS)
      (g.evalRuntime xR) (g.evalBounds epsIn xR)
    theorem Proofs.RuntimeApprox.FwdGraph.eval_approx
  {α : Type} [TorchLean.Storage α]
  {toSpec : α → Spec.SpecScalar}
  {Γ ss : List Spec.Shape}
  (g :
    Proofs.RuntimeApprox.FwdGraph toSpec Γ
      ss)
  (xS :
    TorchLean.TensorPack Spec.SpecScalar
      Γ)
  (xR : TorchLean.TensorPack α Γ)
  (epsIn : Proofs.RuntimeApprox.EList Γ) :
  Proofs.RuntimeApprox.approxCtx toSpec xS
      xR epsIn →
    Proofs.RuntimeApprox.approxCtx toSpec
      (g.evalSpec xS) (g.evalRuntime xR)
      (g.evalBounds epsIn xR)
    End-to-end forward approximation theorem for `FwdGraph`.

Informally:
assume every input tensor in the runtime context `xR` is within the provided per-entry bounds
`epsIn` of the corresponding spec tensor in `xS`. Then evaluating the whole graph preserves that
approximation relation, with output bounds given by `evalBounds`.

Proof idea: induction over the snoc-list graph; at each step, apply the node's local bound/soundness
theorem (`FwdNode.sound`) and then extend the context approximation via `approxCtx_snoc`.
Proof for Theorem 8.2.14
uses 1

Forward graph induction carries every local contract through the stored typed context.

Theorem8.2.15
Group: Operator bounds composed across programs. (8)
Group member previews
Preview
Theorem 8.2.14
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

Given approximate inputs and cotangent seeds, local forward and backward contracts compose into an approximation bound for every gradient produced by reverse graph evaluation.

Lean code for Theorem8.2.15●1 theorem
  • theoremdefined in NN/Proofs/RuntimeApprox/Graph/BackwardApprox.lean
    complete
    theorem Proofs.RuntimeApprox.RevGraph.backprop_approx {α : Type}
  {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape}
  (g : Proofs.RuntimeApprox.RevGraph toSpec Γ ss) [Add α]
  (addBound :
    {Δ : List Spec.Shape} →
      Proofs.RuntimeApprox.EList Δ →
        Proofs.RuntimeApprox.EList Δ →
          TorchLean.TensorPack α Δ →
            TorchLean.TensorPack α Δ → Proofs.RuntimeApprox.EList Δ)
  (addSound :
    ∀ {Δ : List Spec.Shape}
      (xS yS : TorchLean.TensorPack Spec.SpecScalar Δ)
      (xR yR : TorchLean.TensorPack α Δ)
      (epsx epsy : Proofs.RuntimeApprox.EList Δ),
      Proofs.RuntimeApprox.approxCtx toSpec xS xR epsx →
        Proofs.RuntimeApprox.approxCtx toSpec yS yR epsy →
          Proofs.RuntimeApprox.approxCtx toSpec (xS.add yS) (xR.add yR)
            (addBound epsx epsy xR yR))
  (xS : TorchLean.TensorPack Spec.SpecScalar Γ)
  (xR : TorchLean.TensorPack α Γ) (epsIn : Proofs.RuntimeApprox.EList Γ)
  (seedS : TorchLean.TensorPack Spec.SpecScalar (Γ ++ ss))
  (seedR : TorchLean.TensorPack α (Γ ++ ss))
  (epsSeed : Proofs.RuntimeApprox.EList (Γ ++ ss)) :
  Proofs.RuntimeApprox.approxCtx toSpec xS xR epsIn →
    Proofs.RuntimeApprox.approxCtx toSpec seedS seedR epsSeed →
      Proofs.RuntimeApprox.approxCtx toSpec (g.backpropSpec xS seedS)
        (g.backpropRuntime xR seedR)
        (g.backpropBounds epsIn xR epsSeed seedR fun {Δ} => addBound)
    theorem Proofs.RuntimeApprox.RevGraph.backprop_approx
  {α : Type}
  {toSpec : α → Spec.SpecScalar}
  {Γ ss : List Spec.Shape}
  (g :
    Proofs.RuntimeApprox.RevGraph toSpec Γ
      ss)
  [Add α]
  (addBound :
    {Δ : List Spec.Shape} →
      Proofs.RuntimeApprox.EList Δ →
        Proofs.RuntimeApprox.EList Δ →
          TorchLean.TensorPack α Δ →
            TorchLean.TensorPack α Δ →
              Proofs.RuntimeApprox.EList
                Δ)
  (addSound :
    ∀ {Δ : List Spec.Shape}
      (xS yS :
        TorchLean.TensorPack
          Spec.SpecScalar Δ)
      (xR yR : TorchLean.TensorPack α Δ)
      (epsx epsy :
        Proofs.RuntimeApprox.EList Δ),
      Proofs.RuntimeApprox.approxCtx
          toSpec xS xR epsx →
        Proofs.RuntimeApprox.approxCtx
            toSpec yS yR epsy →
          Proofs.RuntimeApprox.approxCtx
            toSpec (xS.add yS) (xR.add yR)
            (addBound epsx epsy xR yR))
  (xS :
    TorchLean.TensorPack Spec.SpecScalar
      Γ)
  (xR : TorchLean.TensorPack α Γ)
  (epsIn : Proofs.RuntimeApprox.EList Γ)
  (seedS :
    TorchLean.TensorPack Spec.SpecScalar
      (Γ ++ ss))
  (seedR :
    TorchLean.TensorPack α (Γ ++ ss))
  (epsSeed :
    Proofs.RuntimeApprox.EList
      (Γ ++ ss)) :
  Proofs.RuntimeApprox.approxCtx toSpec xS
      xR epsIn →
    Proofs.RuntimeApprox.approxCtx toSpec
        seedS seedR epsSeed →
      Proofs.RuntimeApprox.approxCtx
        toSpec (g.backpropSpec xS seedS)
        (g.backpropRuntime xR seedR)
        (g.backpropBounds epsIn xR epsSeed
          seedR fun {Δ} => addBound)
    End-to-end reverse-mode approximation theorem for `RevGraph.backprop*`.

Informally:
assume (1) the runtime inputs `xR` approximate the spec inputs `xS` with bounds `epsIn`, and
(2) the runtime seed cotangents `seedR` approximate the spec seeds `seedS` with bounds `epsSeed`.
Then the *whole* backprop result `backpropRuntime g xR seedR` approximates the spec backprop result
`backpropSpec g xS seedS`, with an explicit bound computed by `backpropBounds`.

The only "extra" ingredient beyond per-node VJP approximation is how we accumulate contributions:
`addBound` describes how addition affects error bounds, and `addSound` is the theorem justifying it
(e.g. for exact reals it is trivial; for rounding models it carries the rounding-error analysis).
Proof for Theorem 8.2.15
uses 1

Reverse graph induction reuses forward composition and threads the local backward bounds through the accumulated cotangent context.

The accumulation law is an explicit numerical premise. When two graph paths reach one variable, their cotangents are added, so bounds for the two local VJPs must also account for that rounded sum. Analytic correctness additionally requires identifying the ideal VJP with the forward derivative.

Definition8.2.16
Group: Operator bounds composed across programs. (8)
Group member previews
Preview
Theorem 8.2.14
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N

divPosErrorBound η epsx epsy xhat yhat is an upper bound for a rounded division's forward error; xhat and yhat are the approximate operands interpreted as reals. The exact denominator is at least η, and the approximate denominator is within \mathtt{epsy} < \eta of it. The bound is the sum of three terms: the numerator error scaled by the effective margin, the denominator error scaled by the squared margin, and half an ULP of the quotient under grid rounding. The theorem approx_div_nf_of_pos_lb proves it, and the sigmoid, logistic, and mean bounds are built on top of it.

Lean code for Definition8.2.16●1 definition
  • defdefined in NN/Proofs/RuntimeApprox/NF/Ops/Elementwise/SafeDivSigmoid.lean
    complete
    def Proofs.RuntimeApprox.NFBackend.divPosErrorBound
  {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ}
  [FloatLib.Floats.Formats.Flocq.ValidExp fexp]
  (η epsx epsy xhat yhat : ℝ) : ℝ
    def Proofs.RuntimeApprox.NFBackend.divPosErrorBound
  {β : FloatLib.Numerics.Radix}
  {fexp : ℤ → ℤ}
  [FloatLib.Floats.Formats.Flocq.ValidExp
      fexp]
  (η epsx epsy xhat yhat : ℝ) : ℝ
    Error budget for division with exact denominator lower bound `η` and denominator approximation
error `epsy`. The caller must separately establish `epsy < η`; otherwise the rounded denominator
may cross zero and no finite perturbation bound follows.
Theorem8.2.17
Group: Operator bounds composed across programs. (8)
Group member previews
Preview
Theorem 8.2.14
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

Under explicit small-error hypotheses on the rounded one, the rounded sigmoid denominator, and the ULP of the quotient, the error budget for the sequence 1/(1+\exp(-x)) derived from the positive-division bound is at most one. This is a regression theorem: it pins the size of the budget so that a refactor cannot silently make it vacuous. The public sigmoid evaluates this sequence on positive inputs and uses \exp(x)/(1+\exp(x)) otherwise. Its theorem approx_sigmoid_nf selects the error budget for the branch that was evaluated.

The two branches agree as real functions, allowing the exact and rounded inputs to fall on opposite sides of zero. Their budgets still follow different rounded operation sequences, including the numerator exponential in the nonpositive branch.

Lean code for Theorem8.2.17●1 theorem
  • theoremdefined in NN/Proofs/RuntimeApprox/NF/Ops/Elementwise/SafeDivSigmoid.lean
    complete
    theorem Proofs.RuntimeApprox.NFBackend.reciprocal_sigmoid_bound_scalar_le_one
  {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ}
  [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ}
  [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {eps : ℝ}
  (xR : FloatLib.Floats.Formats.Flocq.NF β fexp rnd) (heps : 0 ≤ eps)
  (hone : Proofs.RuntimeApprox.NFBackend.oneEps ≤ 1 / 16)
  (hden :
    Proofs.RuntimeApprox.NFBackend.reciprocalSigmoidDenomError eps xR ≤
      1 / 16)
  (hulp :
    FloatLib.Floats.Formats.Flocq.ulp β fexp
        (Proofs.RuntimeApprox.NFBackend.toSpec 1 /
          Proofs.RuntimeApprox.NFBackend.toSpec
            (Proofs.RuntimeApprox.NFBackend.reciprocalSigmoidDenomR
              xR)) ≤
      1 / 2) :
  Proofs.RuntimeApprox.NFBackend.reciprocalSigmoidBoundScalar eps xR ≤ 1
    theorem Proofs.RuntimeApprox.NFBackend.reciprocal_sigmoid_bound_scalar_le_one
  {β : FloatLib.Numerics.Radix}
  {fexp : ℤ → ℤ}
  [FloatLib.Floats.Formats.Flocq.ValidExp
      fexp]
  {rnd : ℝ → ℤ}
  [FloatLib.Floats.Formats.Flocq.ValidRndToNearest
      rnd]
  {eps : ℝ}
  (xR :
    FloatLib.Floats.Formats.Flocq.NF β
      fexp rnd)
  (heps : 0 ≤ eps)
  (hone :
    Proofs.RuntimeApprox.NFBackend.oneEps ≤
      1 / 16)
  (hden :
    Proofs.RuntimeApprox.NFBackend.reciprocalSigmoidDenomError
        eps xR ≤
      1 / 16)
  (hulp :
    FloatLib.Floats.Formats.Flocq.ulp β
        fexp
        (Proofs.RuntimeApprox.NFBackend.toSpec
            1 /
          Proofs.RuntimeApprox.NFBackend.toSpec
            (Proofs.RuntimeApprox.NFBackend.reciprocalSigmoidDenomR
              xR)) ≤
      1 / 2) :
  Proofs.RuntimeApprox.NFBackend.reciprocalSigmoidBoundScalar
      eps xR ≤
    1
    For a format whose half ulp at `1` is at most `1/16`, whose output half ulp is at most `1/4`,
and whose rounded denominator error is at most `1/16`, the reciprocal sequence's bound is at
most `1`.
Proof for Theorem 8.2.17
uses 1

The three terms of the division bound are each estimated against the hypotheses and summed.

Definition8.2.18
Group: Operator bounds composed across programs. (8)
Group member previews
Preview
Theorem 8.2.14
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

NumericalStepContract packages specification and runtime optimizer states, their approximation relation, an update bound, any domain checks, and the theorem that one update respects the bound.

Lean code for Definition8.2.18●1 definition
  • structure(13 fields)defined in NN/Proofs/RuntimeApprox/Optimizer.lean
    complete
    structure Proofs.RuntimeApprox.Optimizer.NumericalStepContract (R : Type)
  (toSpec : R → ℝ) : Type 1
    structure Proofs.RuntimeApprox.Optimizer.NumericalStepContract
  (R : Type) (toSpec : R → ℝ) : Type 1
    A numerical refinement contract for one shape-polymorphic optimizer update.

`StepAssumptions` carries numerical information required only for the current update. It is `Unit`
for unconditional rules such as SGD, while adaptive optimizers use it for denominator margins and
rounded scalar-expression bounds. This lets one finite-run theorem cover both cases.

    Fields

    name : String
    Stable optimizer name used in numerical reports. 
    ExactState : Spec.Shape → Type
    Mathematical optimizer state. 
    RuntimeState : Spec.Shape → Type
    Rounded runtime optimizer state. 
    StateError : Spec.Shape → Type
    Error information relating mathematical and runtime state. 
    StepAssumptions : Spec.Shape → Type
    Numerical data and domain margins supplied for one update. 
    stateApprox : {shape : Spec.Shape} → self.ExactState shape → self.RuntimeState shape → self.StateError shape → Prop
    Relation certified between mathematical and runtime state. 
    assumptionsHold : {shape : Spec.Shape} →
  self.ExactState shape →
    self.RuntimeState shape →
      self.StateError shape →
        TorchLean.Tensor ℝ shape →
          TorchLean.Tensor R shape →
            ℝ → TorchLean.Tensor ℝ shape → TorchLean.Tensor R shape → ℝ → self.StepAssumptions shape → Prop
    Conditions under which one step's numerical data is valid. 
    updateExact : {shape : Spec.Shape} →
  self.ExactState shape →
    TorchLean.Tensor ℝ shape → TorchLean.Tensor ℝ shape → Optim.Step ℝ shape (self.ExactState shape)
    One exact-real optimizer update. 
    updateRuntime : {shape : Spec.Shape} →
  self.RuntimeState shape →
    TorchLean.Tensor R shape → TorchLean.Tensor R shape → Optim.Step R shape (self.RuntimeState shape)
    One rounded runtime optimizer update. 
    nextError : {shape : Spec.Shape} →
  self.StateError shape →
    ℝ →
      ℝ →
        self.RuntimeState shape →
          TorchLean.Tensor R shape →
            TorchLean.Tensor R shape →
              self.StepAssumptions shape → Proofs.RuntimeApprox.Optimizer.StepError self.StateError shape
    Compute the next state/parameter bounds from current errors and runtime values. 
    stateErrorReport : {shape : Spec.Shape} → self.StateError shape → Array (String × ℝ)
    Proof-free scalar components of a state bound for reports and UI consumers. 
    assumptionReport : {shape : Spec.Shape} → self.StepAssumptions shape → Array (String × ℝ)
    Proof-free scalar components of one step's side data. 
    updateApprox : ∀ {shape : Spec.Shape} (exactState : self.ExactState shape) (runtimeState : self.RuntimeState shape)
  (stateError : self.StateError shape) (exactParameters : TorchLean.Tensor ℝ shape)
  (runtimeParameters : TorchLean.Tensor R shape) (parameterError : ℝ) (exactGradients : TorchLean.Tensor ℝ shape)
  (runtimeGradients : TorchLean.Tensor R shape) (gradientError : ℝ) (assumptions : self.StepAssumptions shape),
  self.stateApprox exactState runtimeState stateError →
    Proofs.RuntimeApprox.approxTensor toSpec exactParameters runtimeParameters parameterError →
      Proofs.RuntimeApprox.approxTensor toSpec exactGradients runtimeGradients gradientError →
        self.assumptionsHold exactState runtimeState stateError exactParameters runtimeParameters parameterError
            exactGradients runtimeGradients gradientError assumptions →
          let error :=
            self.nextError stateError parameterError gradientError runtimeState runtimeParameters runtimeGradients
              assumptions;
          self.stateApprox (self.updateExact exactState exactParameters exactGradients).optimizerState
              (self.updateRuntime runtimeState runtimeParameters runtimeGradients).optimizerState
              error.optimizerStateError ∧
            Proofs.RuntimeApprox.approxTensor toSpec
              (self.updateExact exactState exactParameters exactGradients).parameters
              (self.updateRuntime runtimeState runtimeParameters runtimeGradients).parameters error.parameterError
    One-step numerical soundness.
Theorem8.2.19
Group: Operator bounds composed across programs. (8)
Group member previews
Preview
Theorem 8.2.14
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Theorem 8.2.15
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

For one parameter in an already constructed typed reverse graph, the reverse approximation theorem and a valid optimizer contract carry the stated input, seed, parameter, state, and step-data bounds through backpropagation and one optimizer update.

Lean code for Theorem8.2.19●1 theorem
  • theoremdefined in NN/Proofs/RuntimeApprox/NF/EndToEnd.lean
    complete
    theorem Proofs.RuntimeApprox.NFBackend.backprop_optimizer_update_approx_graphData
  {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ}
  [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ}
  [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd]
  {Γ ss : List Spec.Shape}
  (g :
    Proofs.RuntimeApprox.RevGraph Proofs.RuntimeApprox.NFBackend.toSpec
      Γ ss)
  (i : Fin Γ.length)
  (contract :
    Proofs.RuntimeApprox.Optimizer.NumericalStepContract
      (FloatLib.Floats.Formats.Flocq.NF β fexp rnd)
      Proofs.RuntimeApprox.NFBackend.toSpec)
  (xS : TorchLean.TensorPack Spec.SpecScalar Γ)
  (xR :
    TorchLean.TensorPack (FloatLib.Floats.Formats.Flocq.NF β fexp rnd)
      Γ)
  (epsIn : Proofs.RuntimeApprox.EList Γ)
  (seedS : TorchLean.TensorPack Spec.SpecScalar (Γ ++ ss))
  (seedR :
    TorchLean.TensorPack (FloatLib.Floats.Formats.Flocq.NF β fexp rnd)
      (Γ ++ ss))
  (epsSeed : Proofs.RuntimeApprox.EList (Γ ++ ss))
  (paramsS : TorchLean.Tensor ℝ (Γ.get i))
  (paramsR :
    TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd)
      (Γ.get i))
  (paramsError : ℝ) (stateS : contract.ExactState (Γ.get i))
  (stateR : contract.RuntimeState (Γ.get i))
  (stateError : contract.StateError (Γ.get i))
  (assumptions : contract.StepAssumptions (Γ.get i))
  (hx :
    Proofs.RuntimeApprox.approxCtx Proofs.RuntimeApprox.NFBackend.toSpec
      xS xR epsIn)
  (hseed :
    Proofs.RuntimeApprox.approxCtx Proofs.RuntimeApprox.NFBackend.toSpec
      seedS seedR epsSeed)
  (hparams :
    Proofs.RuntimeApprox.approxTensor
      Proofs.RuntimeApprox.NFBackend.toSpec paramsS paramsR paramsError)
  (hstate : contract.stateApprox stateS stateR stateError)
  (hAssumptions :
    have exactGradients := g.backpropSpec xS seedS;
    have runtimeGradients :=
      (Proofs.RuntimeApprox.LinkAutogradAlgebra.RevGraph.toGraphData
            g).backpropCtx
        xR () seedR;
    have gradientError :=
      (g.backpropBounds epsIn xR epsSeed seedR fun {Δ} =>
            Proofs.RuntimeApprox.NFBackend.ctxAddBound).get
        i;
    contract.assumptionsHold stateS stateR stateError paramsS paramsR
      paramsError (exactGradients.get i) (runtimeGradients.get i)
      gradientError assumptions) :
  have exactGradients := g.backpropSpec xS seedS;
  have runtimeGradients :=
    (Proofs.RuntimeApprox.LinkAutogradAlgebra.RevGraph.toGraphData
          g).backpropCtx
      xR () seedR;
  have gradientError :=
    (g.backpropBounds epsIn xR epsSeed seedR fun {Δ} =>
          Proofs.RuntimeApprox.NFBackend.ctxAddBound).get
      i;
  have nextError :=
    contract.nextError stateError paramsError gradientError stateR
      paramsR (runtimeGradients.get i) assumptions;
  contract.stateApprox
      (contract.updateExact stateS paramsS
          (exactGradients.get i)).optimizerState
      (contract.updateRuntime stateR paramsR
          (runtimeGradients.get i)).optimizerState
      nextError.optimizerStateError ∧
    Proofs.RuntimeApprox.approxTensor
      Proofs.RuntimeApprox.NFBackend.toSpec
      (contract.updateExact stateS paramsS
          (exactGradients.get i)).parameters
      (contract.updateRuntime stateR paramsR
          (runtimeGradients.get i)).parameters
      nextError.parameterError
    theorem Proofs.RuntimeApprox.NFBackend.backprop_optimizer_update_approx_graphData
  {β : FloatLib.Numerics.Radix}
  {fexp : ℤ → ℤ}
  [FloatLib.Floats.Formats.Flocq.ValidExp
      fexp]
  {rnd : ℝ → ℤ}
  [FloatLib.Floats.Formats.Flocq.ValidRndToNearest
      rnd]
  {Γ ss : List Spec.Shape}
  (g :
    Proofs.RuntimeApprox.RevGraph
      Proofs.RuntimeApprox.NFBackend.toSpec
      Γ ss)
  (i : Fin Γ.length)
  (contract :
    Proofs.RuntimeApprox.Optimizer.NumericalStepContract
      (FloatLib.Floats.Formats.Flocq.NF β
        fexp rnd)
      Proofs.RuntimeApprox.NFBackend.toSpec)
  (xS :
    TorchLean.TensorPack Spec.SpecScalar
      Γ)
  (xR :
    TorchLean.TensorPack
      (FloatLib.Floats.Formats.Flocq.NF β
        fexp rnd)
      Γ)
  (epsIn : Proofs.RuntimeApprox.EList Γ)
  (seedS :
    TorchLean.TensorPack Spec.SpecScalar
      (Γ ++ ss))
  (seedR :
    TorchLean.TensorPack
      (FloatLib.Floats.Formats.Flocq.NF β
        fexp rnd)
      (Γ ++ ss))
  (epsSeed :
    Proofs.RuntimeApprox.EList (Γ ++ ss))
  (paramsS : TorchLean.Tensor ℝ (Γ.get i))
  (paramsR :
    TorchLean.Tensor
      (FloatLib.Floats.Formats.Flocq.NF β
        fexp rnd)
      (Γ.get i))
  (paramsError : ℝ)
  (stateS : contract.ExactState (Γ.get i))
  (stateR :
    contract.RuntimeState (Γ.get i))
  (stateError :
    contract.StateError (Γ.get i))
  (assumptions :
    contract.StepAssumptions (Γ.get i))
  (hx :
    Proofs.RuntimeApprox.approxCtx
      Proofs.RuntimeApprox.NFBackend.toSpec
      xS xR epsIn)
  (hseed :
    Proofs.RuntimeApprox.approxCtx
      Proofs.RuntimeApprox.NFBackend.toSpec
      seedS seedR epsSeed)
  (hparams :
    Proofs.RuntimeApprox.approxTensor
      Proofs.RuntimeApprox.NFBackend.toSpec
      paramsS paramsR paramsError)
  (hstate :
    contract.stateApprox stateS stateR
      stateError)
  (hAssumptions :
    have exactGradients :=
      g.backpropSpec xS seedS;
    have runtimeGradients :=
      (Proofs.RuntimeApprox.LinkAutogradAlgebra.RevGraph.toGraphData
            g).backpropCtx
        xR () seedR;
    have gradientError :=
      (g.backpropBounds epsIn xR epsSeed
            seedR fun {Δ} =>
            Proofs.RuntimeApprox.NFBackend.ctxAddBound).get
        i;
    contract.assumptionsHold stateS stateR
      stateError paramsS paramsR
      paramsError (exactGradients.get i)
      (runtimeGradients.get i)
      gradientError assumptions) :
  have exactGradients :=
    g.backpropSpec xS seedS;
  have runtimeGradients :=
    (Proofs.RuntimeApprox.LinkAutogradAlgebra.RevGraph.toGraphData
          g).backpropCtx
      xR () seedR;
  have gradientError :=
    (g.backpropBounds epsIn xR epsSeed
          seedR fun {Δ} =>
          Proofs.RuntimeApprox.NFBackend.ctxAddBound).get
      i;
  have nextError :=
    contract.nextError stateError
      paramsError gradientError stateR
      paramsR (runtimeGradients.get i)
      assumptions;
  contract.stateApprox
      (contract.updateExact stateS paramsS
          (exactGradients.get
            i)).optimizerState
      (contract.updateRuntime stateR
          paramsR
          (runtimeGradients.get
            i)).optimizerState
      nextError.optimizerStateError ∧
    Proofs.RuntimeApprox.approxTensor
      Proofs.RuntimeApprox.NFBackend.toSpec
      (contract.updateExact stateS paramsS
          (exactGradients.get
            i)).parameters
      (contract.updateRuntime stateR
          paramsR
          (runtimeGradients.get
            i)).parameters
      nextError.parameterError
    Executable reverse mode followed by any valid numerical optimizer contract is sound.

The theorem is shape-polymorphic and optimizer-polymorphic. `assumptionsHold` is trivial for
globally sound updates such as SGD and records domain conditions for updates such as AdamW whose
square root and division must stay away from singularities. No optimizer needs a separate graph
theorem. Models with several parameter tensors instantiate this theorem at each typed index.
Proof for Theorem 8.2.19
Proof uses 2
Proof dependency previews
Preview
Theorem 8.2.15
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

The proof obtains the indexed gradient bound from reverse composition, then applies the update-soundness field of the supplied optimizer contract.

The parameter tensor being updated is a separate argument from the graph context. For ordinary training, the application chooses the tensor at that context index, so the gradient is evaluated at the parameter value that receives the update.

Definition8.2.20
Group: Operator bounds composed across programs. (8)
Group member previews
Preview
Theorem 8.2.14
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0
Used by 2
Reverse dependency previews
Preview
Definition 8.2.21
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

A registry-checked numerical certificate retains the submitted artifact together with the canonical source ranges, node-range trace, accepted kernel plan, and proofs that the recomputed trace and audit match the artifact. Real-valued enclosure is a separate theorem.

This distinction separates consistency of submitted data from mathematical soundness of the range transfer. Reconstructing the same interval twice proves agreement with the registry, but enclosure still needs a connection to the operation's real denotation.

Lean code for Definition8.2.20●1 definition
  • structure(7 fields)defined in NN/Proofs/RuntimeApprox/Graph/NumericalCertificate/Certificate.lean
    complete
    structure Proofs.RuntimeApprox.NumericalCertificate.RegistryCheckedCertificate :
  Type
    structure Proofs.RuntimeApprox.NumericalCertificate.RegistryCheckedCertificate :
  Type
    Result returned after registry replay and backend-plan checking.

The checker reconstructs the range rows and proves that the artifact matches that reconstruction.
This structure does not by itself prove that the rows enclose the graph's real denotation; that
semantic statement is carried separately by `ProvedRealEnclosure`.

    Fields

    graph : NN.IR.Graph
    The exact graph whose ranges and kernel plan were reconstructed by the checker. 
    raw : Proofs.RuntimeApprox.NumericalCertificate.GraphNumericalCertificate
    The untrusted artifact supplied to the checker, retained for inspection and serialization. 
    sources : Array Proofs.RuntimeApprox.NumericalCertificate.CheckedSourceRange
    Source assumptions whose interval endpoints have been proved finite and ordered. 
    ranges : Array Proofs.RuntimeApprox.NumericalCertificate.CheckedNodeRange
    The canonical node-by-node range trace reconstructed from the graph. 
    backendPlan : NN.Backend.AcceptedGraphKernelPlan
    The kernel plan accepted when the checker replanned `graph`. 
    rangesMatch : Proofs.RuntimeApprox.NumericalCertificate.sameRangeTrace self.ranges self.raw.ranges = true
    Proof that the reconstructed trace matches every range row claimed by `raw`. 
    auditMatch : self.backendPlan.audit = self.raw.audit
    Proof that the accepted plan's audit is the one stored in `raw`.
Definition8.2.21
Group: Operator bounds composed across programs. (8)
Group member previews
Preview
Theorem 8.2.14
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 8.1.23
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

For one registry-checked certificate, ProvedRealEnclosure stores a real payload and input, the complete IR execution trace, and a proof that each real node value lies in its checked interval.

Lean code for Definition8.2.21●1 definition
  • structure(5 fields)defined in NN/Proofs/RuntimeApprox/Graph/NumericalCertificate/Certificate.lean
    complete
    structure Proofs.RuntimeApprox.NumericalCertificate.ProvedRealEnclosure
  (certificate :
    Proofs.RuntimeApprox.NumericalCertificate.RegistryCheckedCertificate) :
  Type
    structure Proofs.RuntimeApprox.NumericalCertificate.ProvedRealEnclosure
  (certificate :
    Proofs.RuntimeApprox.NumericalCertificate.RegistryCheckedCertificate) :
  Type
    Exact-real execution evidence for the graph stored in a registry-checked certificate.

The numerical checker reconstructs interval transfers, while a semantic proof establishes that the
real graph trace lies in those intervals. Keeping this proof separate prevents successful endpoint
replay from being mistaken for a theorem about an unsupported real operation.

    Fields

    payload : NN.IR.Payload ℝ
    Real-valued constants and external tensors used by the graph execution. 
    input : Spec.SomeTensor ℝ
    Real-valued graph input. 
    values : Array (Spec.SomeTensor ℝ)
    Complete real-valued node trace, in graph order. 
    denotation : certificate.graph.denoteAll self.payload self.input = Except.ok self.values
    Evidence that `values` is exactly the graph's denotational execution trace. 
    enclosed : Proofs.RuntimeApprox.NumericalCertificate.ArraysRelated Proofs.RuntimeApprox.NumericalCertificate.SomeTensorEnclosed
  certificate.ranges self.values
    Pointwise evidence that every real node value lies in its checked interval.
Theorem8.2.22
Group: Operator bounds composed across programs. (8)
Group member previews
Preview
Theorem 8.2.14
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 8.2.20
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

A checked IEEE replay plus a separately supplied real-execution enclosure for the same certificate yields a graph-wide pointwise error trace whose budget at each node is the width of its checked interval.

Lean code for Theorem8.2.22●1 theorem
  • theoremdefined in NN/Proofs/RuntimeApprox/Graph/NumericalCertificate/Certificate.lean
    complete
    theorem Proofs.RuntimeApprox.NumericalCertificate.RangeCheckedExecution.error_trace
  (execution :
    Proofs.RuntimeApprox.NumericalCertificate.RangeCheckedExecution)
  (exact :
    Proofs.RuntimeApprox.NumericalCertificate.ProvedRealEnclosure
      execution.certificate) :
  Proofs.RuntimeApprox.NumericalCertificate.ExecutionErrorTrace
    execution.certificate.ranges exact.values execution.values
    theorem Proofs.RuntimeApprox.NumericalCertificate.RangeCheckedExecution.error_trace
  (execution :
    Proofs.RuntimeApprox.NumericalCertificate.RangeCheckedExecution)
  (exact :
    Proofs.RuntimeApprox.NumericalCertificate.ProvedRealEnclosure
      execution.certificate) :
  Proofs.RuntimeApprox.NumericalCertificate.ExecutionErrorTrace
    execution.certificate.ranges
    exact.values execution.values
    Pair a checked IEEE replay with a proved real enclosure trace to obtain a graph-wide,
pointwise error trace. Each node's error budget is the width of its checked outward interval.
Proof for Theorem 8.2.22
uses 1

The proof combines the IEEE replay's range check with the supplied real enclosure, node by node.

Both values lie between the same endpoints, so their distance is bounded by the interval width. This is pointwise in the two supplied executions. A statement for every input in a region requires real-enclosure and execution evidence quantified over that region.