TorchLean

8.2. Floating-Point Numerics🔗

The numerical map keeps two binary32 models in view. FP32 is a rounded-real model for proofs; IEEE32Exec computes from raw bits and includes signed zeros, infinities, and NaNs. Bridge theorems connect their finite cases. The runtime-approximation layer then composes local operator bounds over whole forward and backward graphs.

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

NeuralFloat 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 NN/Floats/NeuralFloat/Core.lean
    complete
    structure TorchLean.Floats.NeuralFloat (β : TorchLean.Floats.NeuralRadix) : Type
    structure TorchLean.Floats.NeuralFloat
  (β : TorchLean.Floats.NeuralRadix) :
  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

neuralGenericFormat 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 NN/Floats/NeuralFloat/Core.lean
    complete
    def TorchLean.Floats.neuralGenericFormat (β : TorchLean.Floats.NeuralRadix)
  (fexp : ℤ → ℤ) [TorchLean.Floats.NeuralValidExp fexp] (x : ℝ) : Prop
    def TorchLean.Floats.neuralGenericFormat
  (β : TorchLean.Floats.NeuralRadix)
  (fexp : ℤ → ℤ)
  [TorchLean.Floats.NeuralValidExp 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

NeuralValidRndToNearest 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 NN/Floats/NeuralFloat/Rounding/Core.lean
    complete
    class TorchLean.Floats.NeuralValidRndToNearest (rnd : ℝ → ℤ) : Prop
    class TorchLean.Floats.NeuralValidRndToNearest
  (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

    • TorchLean.Floats.NeuralValidRnd rnd

    Methods

    monotone : ∀ (x y : ℝ), x ≤ y → rnd x ≤ rnd y
    Inherited from
    1. TorchLean.Floats.NeuralValidRnd
    id : ∀ (n : ℤ), rnd ↑n = n
    Inherited from
    1. TorchLean.Floats.NeuralValidRnd
    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 1used by 1✓L∃∀N

neuralRound 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.

Lean code for Definition8.2.4●1 definition
  • defdefined in NN/Floats/NeuralFloat/Rounding/Core.lean
    complete
    def TorchLean.Floats.neuralRound {β : TorchLean.Floats.NeuralRadix}
  {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] (rnd : ℝ → ℤ)
  (x : ℝ) : ℝ
    def TorchLean.Floats.neuralRound
  {β : TorchLean.Floats.NeuralRadix}
  {fexp : ℤ → ℤ}
  [TorchLean.Floats.NeuralValidExp fexp]
  (rnd : ℝ → ℤ) (x : ℝ) : ℝ
    Core rounding operator (“compute in `ℝ`, then round back to the grid”).

We build a pure `NeuralFloat` mantissa/exponent pair and interpret it with `neuralToReal`.
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 NN/Floats/NeuralFloat/Rounding/Core.lean
    complete
    theorem TorchLean.Floats.neural_error_bound_ulp
  {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ}
  [TorchLean.Floats.NeuralValidExp fexp] (rnd : ℝ → ℤ)
  [TorchLean.Floats.NeuralValidRndToNearest rnd] (x : ℝ) :
  |TorchLean.Floats.neuralRound rnd x - x| ≤
    TorchLean.Floats.neuralUlp β fexp x / 2
    theorem TorchLean.Floats.neural_error_bound_ulp
  {β : TorchLean.Floats.NeuralRadix}
  {fexp : ℤ → ℤ}
  [TorchLean.Floats.NeuralValidExp fexp]
  (rnd : ℝ → ℤ)
  [TorchLean.Floats.NeuralValidRndToNearest
      rnd]
  (x : ℝ) :
  |TorchLean.Floats.neuralRound rnd x -
        x| ≤
    TorchLean.Floats.neuralUlp β fexp x /
      2
    Half-ULP error bound for `neural_round` under round-to-nearest.

This is the basic “one-step” bound used by most error propagation arguments:
`neural_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 NN/Floats/Quantization.lean
    complete
    structure TorchLean.Floats.Quantization.AffineQuantizer : Type
    structure TorchLean.Floats.Quantization.AffineQuantizer :
  Type
    Parameters of a bounded affine quantizer.

    Fields

    scale : ℝ
    Distance between adjacent reconstructed real values. 
    zeroPoint : ℤ
    Integer code representing real zero when it lies in the code range. 
    qmin : ℤ
    Smallest stored code. 
    qmax : ℤ
    Largest stored code. 
    scale_pos : 0 < self.scale
    A quantization scale is strictly positive. 
    codeRange : self.qmin ≤ self.qmax
    The code 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.

Lean code for Theorem8.2.7●1 theorem
  • theoremdefined in NN/Floats/Quantization.lean
    complete
    theorem TorchLean.Floats.Quantization.AffineQuantizer.dequantize_quantize_error_le
  (q : TorchLean.Floats.Quantization.AffineQuantizer) (rnd : ℝ → ℤ)
  [TorchLean.Floats.NeuralValidRndToNearest rnd] (x : ℝ)
  (hlo : q.qmin ≤ q.rawCode rnd x) (hhi : q.rawCode rnd x ≤ q.qmax) :
  |q.dequantize (q.quantize rnd x) - x| ≤ q.scale / 2
    theorem TorchLean.Floats.Quantization.AffineQuantizer.dequantize_quantize_error_le
  (q :
    TorchLean.Floats.Quantization.AffineQuantizer)
  (rnd : ℝ → ℤ)
  [TorchLean.Floats.NeuralValidRndToNearest
      rnd]
  (x : ℝ) (hlo : q.qmin ≤ q.rawCode rnd x)
  (hhi : q.rawCode rnd x ≤ q.qmax) :
  |q.dequantize (q.quantize rnd x) - x| ≤
    q.scale / 2
    The half-step bound survives saturation whenever clipping is inactive.
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 IEEE32Exec.

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.round₃₂ x - x| ≤ TorchLean.Floats.eps₃₂ x
    theorem TorchLean.Floats.FP32.round_abs_error
  (x : ℝ) :
  |TorchLean.Floats.round₃₂ x - x| ≤
    TorchLean.Floats.eps₃₂ 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.

The implementation of binary32 rounding reduces to exact integer arithmetic, and the generic half-ULP theorem 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

Raw 32-bit words drive executable addition, multiplication, division, fused multiply-add, and square root, together with IEEE exception status.

Lean code for Definition8.2.10●1 definition
  • structure(1 field)defined in NN/Floats/IEEEExec/Exec32/Core.lean
    complete
    structure TorchLean.Floats.IEEE754.IEEE32Exec : Type
    structure TorchLean.Floats.IEEE754.IEEE32Exec : Type
    Executable IEEE-754 binary32 value, stored as raw bits.

    Fields

    bits : UInt32
    bits.
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/FP32Total/Arithmetic.lean
    complete
    theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_add_eq_fp32Round_of_isFinite
  (x y : TorchLean.Floats.IEEE754.IEEE32Exec)
  (hfin : (x.add y).isFinite = true) :
  (x.add y).toReal =
    TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round (x.toReal + y.toReal)
    theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_add_eq_fp32Round_of_isFinite
  (x y :
    TorchLean.Floats.IEEE754.IEEE32Exec)
  (hfin : (x.add y).isFinite = true) :
  (x.add y).toReal =
    TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round
      (x.toReal + y.toReal)
    Addition refinement packaged for total reasoning.
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.

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 NN/Floats/IEEEExec/DirectedRoundingSoundness/SignedOps.lean
    complete
    theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_addDown_le
  (x y : TorchLean.Floats.IEEE754.IEEE32Exec) (hx : x.isFinite = true)
  (hy : y.isFinite = true) :
  (x.addDown y).toEReal ≤ ↑(x.toReal + y.toReal)
    theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_addDown_le
  (x y :
    TorchLean.Floats.IEEE754.IEEE32Exec)
  (hx : x.isFinite = true)
  (hy : y.isFinite = true) :
  (x.addDown y).toEReal ≤
    ↑(x.toReal + y.toReal)
    Lower-endpoint soundness for `addDown` on finite inputs:
$\operatorname{toEReal}(\operatorname{addDown}(x,y))
\leq\operatorname{toReal}(x)+\operatorname{toReal}(y)$, even when the result overflows to
$-\infty$.
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 NN/Floats/IEEEExec/DirectedRoundingSoundness/SignedOps.lean
    complete
    theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_addUp_ge
  (x y : TorchLean.Floats.IEEE754.IEEE32Exec) (hx : x.isFinite = true)
  (hy : y.isFinite = true) :
  ↑(x.toReal + y.toReal) ≤ (x.addUp y).toEReal
    theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_addUp_ge
  (x y :
    TorchLean.Floats.IEEE754.IEEE32Exec)
  (hx : x.isFinite = true)
  (hy : y.isFinite = true) :
  ↑(x.toReal + y.toReal) ≤
    (x.addUp y).toEReal
    Upper-endpoint soundness for `addUp` on finite inputs:
$\operatorname{toReal}(x)+\operatorname{toReal}(y)
\leq\operatorname{toEReal}(\operatorname{addUp}(x,y))$, with overflow rounding to $+\infty$.
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.

Theorem8.2.14
Group: Operator bounds composed across programs. (6)
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}
  {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape}
  (g : Proofs.RuntimeApprox.FwdGraph toSpec Γ ss)
  (xS : Proofs.RuntimeApprox.TList Spec.SpecScalar Γ)
  (xR : Proofs.RuntimeApprox.TList α Γ)
  (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}
  {toSpec : α → Spec.SpecScalar}
  {Γ ss : List Spec.Shape}
  (g :
    Proofs.RuntimeApprox.FwdGraph toSpec Γ
      ss)
  (xS :
    Proofs.RuntimeApprox.TList
      Spec.SpecScalar Γ)
  (xR : Proofs.RuntimeApprox.TList α Γ)
  (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
lemma (`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. (6)
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 Δ →
          Proofs.RuntimeApprox.TList α Δ →
            Proofs.RuntimeApprox.TList α Δ →
              Proofs.RuntimeApprox.EList Δ)
  (addSound :
    ∀ {Δ : List Spec.Shape}
      (xS yS : Proofs.RuntimeApprox.TList Spec.SpecScalar Δ)
      (xR yR : Proofs.RuntimeApprox.TList α Δ)
      (epsx epsy : Proofs.RuntimeApprox.EList Δ),
      Proofs.RuntimeApprox.approxCtx toSpec xS xR epsx →
        Proofs.RuntimeApprox.approxCtx toSpec yS yR epsy →
          Proofs.RuntimeApprox.approxCtx toSpec
            (Proofs.Autograd.Algebra.TList.add xS yS)
            (Proofs.Autograd.Algebra.TList.add xR yR)
            (addBound epsx epsy xR yR))
  (xS : Proofs.RuntimeApprox.TList Spec.SpecScalar Γ)
  (xR : Proofs.RuntimeApprox.TList α Γ)
  (epsIn : Proofs.RuntimeApprox.EList Γ)
  (seedS : Proofs.RuntimeApprox.TList Spec.SpecScalar (Γ ++ ss))
  (seedR : Proofs.RuntimeApprox.TList α (Γ ++ 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 Δ →
          Proofs.RuntimeApprox.TList α Δ →
            Proofs.RuntimeApprox.TList α
                Δ →
              Proofs.RuntimeApprox.EList
                Δ)
  (addSound :
    ∀ {Δ : List Spec.Shape}
      (xS yS :
        Proofs.RuntimeApprox.TList
          Spec.SpecScalar Δ)
      (xR yR :
        Proofs.RuntimeApprox.TList α Δ)
      (epsx epsy :
        Proofs.RuntimeApprox.EList Δ),
      Proofs.RuntimeApprox.approxCtx
          toSpec xS xR epsx →
        Proofs.RuntimeApprox.approxCtx
            toSpec yS yR epsy →
          Proofs.RuntimeApprox.approxCtx
            toSpec
            (Proofs.Autograd.Algebra.TList.add
              xS yS)
            (Proofs.Autograd.Algebra.TList.add
              xR yR)
            (addBound epsx epsy xR yR))
  (xS :
    Proofs.RuntimeApprox.TList
      Spec.SpecScalar Γ)
  (xR : Proofs.RuntimeApprox.TList α Γ)
  (epsIn : Proofs.RuntimeApprox.EList Γ)
  (seedS :
    Proofs.RuntimeApprox.TList
      Spec.SpecScalar (Γ ++ ss))
  (seedR :
    Proofs.RuntimeApprox.TList α
      (Γ ++ 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.

Definition8.2.16
Group: Operator bounds composed across programs. (6)
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.16●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.

`StepData` 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. 
    StateSpec : Spec.Shape → Type
    Mathematical optimizer state. 
    StateRuntime : Spec.Shape → Type
    Rounded runtime optimizer state. 
    StateBound : Spec.Shape → Type
    Error information relating mathematical and runtime state. 
    StepData : Spec.Shape → Type
    Numerical data and domain margins supplied for one update. 
    stateApprox : {s : Spec.Shape} → self.StateSpec s → self.StateRuntime s → self.StateBound s → Prop
    Relation certified between mathematical and runtime state. 
    stepDataValid : {s : Spec.Shape} →
  self.StateSpec s →
    self.StateRuntime s →
      self.StateBound s →
        Spec.Tensor ℝ s → Spec.Tensor R s → ℝ → Spec.Tensor ℝ s → Spec.Tensor R s → ℝ → self.StepData s → Prop
    Conditions under which one step's numerical data is valid. 
    updateSpec : {s : Spec.Shape} → self.StateSpec s → Spec.Tensor ℝ s → Spec.Tensor ℝ s → self.StateSpec s × Spec.Tensor ℝ s
    One exact-real optimizer update. 
    updateRuntime : {s : Spec.Shape} → self.StateRuntime s → Spec.Tensor R s → Spec.Tensor R s → self.StateRuntime s × Spec.Tensor R s
    One rounded runtime optimizer update. 
    updateBound : {s : Spec.Shape} →
  self.StateBound s →
    ℝ →
      ℝ →
        self.StateRuntime s →
          Spec.Tensor R s →
            Spec.Tensor R s → self.StepData s → Proofs.RuntimeApprox.Optimizer.StepBound self.StateBound s
    Compute the next state/parameter bounds from current errors and runtime values. 
    stateBoundReport : {s : Spec.Shape} → self.StateBound s → List (String × ℝ)
    Proof-free scalar components of a state bound for reports and UI consumers. 
    stepDataReport : {s : Spec.Shape} → self.StepData s → List (String × ℝ)
    Proof-free scalar components of one step's side data. 
    updateSound : ∀ {s : Spec.Shape} (stateS : self.StateSpec s) (stateR : self.StateRuntime s) (stateBound : self.StateBound s)
  (paramsS : Spec.Tensor ℝ s) (paramsR : Spec.Tensor R s) (paramsError : ℝ) (gradsS : Spec.Tensor ℝ s)
  (gradsR : Spec.Tensor R s) (gradsError : ℝ) (stepData : self.StepData s),
  self.stateApprox stateS stateR stateBound →
    Proofs.RuntimeApprox.approxT toSpec paramsS paramsR paramsError →
      Proofs.RuntimeApprox.approxT toSpec gradsS gradsR gradsError →
        self.stepDataValid stateS stateR stateBound paramsS paramsR paramsError gradsS gradsR gradsError stepData →
          let nextBound := self.updateBound stateBound paramsError gradsError stateR paramsR gradsR stepData;
          self.stateApprox (self.updateSpec stateS paramsS gradsS).1 (self.updateRuntime stateR paramsR gradsR).1
              nextBound.state ∧
            Proofs.RuntimeApprox.approxT toSpec (self.updateSpec stateS paramsS gradsS).2
              (self.updateRuntime stateR paramsR gradsR).2 nextBound.params
    One-step numerical soundness.
Theorem8.2.17
Group: Operator bounds composed across programs. (6)
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.17●1 theorem
  • theoremdefined in NN/Proofs/RuntimeApprox/NF/EndToEnd.lean
    complete
    theorem Proofs.RuntimeApprox.NFBackend.backprop_optimizer_update_approx_graphData
  {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ}
  [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ}
  [TorchLean.Floats.NeuralValidRndToNearest rnd]
  {Γ ss : List Spec.Shape}
  (g :
    Proofs.RuntimeApprox.RevGraph Proofs.RuntimeApprox.NFBackend.toSpec
      Γ ss)
  (i : Fin Γ.length)
  (contract :
    Proofs.RuntimeApprox.Optimizer.NumericalStepContract
      (TorchLean.Floats.NF β fexp rnd)
      Proofs.RuntimeApprox.NFBackend.toSpec)
  (xS : Proofs.RuntimeApprox.TList Spec.SpecScalar Γ)
  (xR : Proofs.RuntimeApprox.TList (TorchLean.Floats.NF β fexp rnd) Γ)
  (epsIn : Proofs.RuntimeApprox.EList Γ)
  (seedS : Proofs.RuntimeApprox.TList Spec.SpecScalar (Γ ++ ss))
  (seedR :
    Proofs.RuntimeApprox.TList (TorchLean.Floats.NF β fexp rnd)
      (Γ ++ ss))
  (epsSeed : Proofs.RuntimeApprox.EList (Γ ++ ss))
  (paramsS : Spec.Tensor ℝ (Γ.get i))
  (paramsR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) (Γ.get i))
  (paramsError : ℝ) (stateS : contract.StateSpec (Γ.get i))
  (stateR : contract.StateRuntime (Γ.get i))
  (stateError : contract.StateBound (Γ.get i))
  (stepData : contract.StepData (Γ.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.approxT Proofs.RuntimeApprox.NFBackend.toSpec
      paramsS paramsR paramsError)
  (hstate : contract.stateApprox stateS stateR stateError)
  (hstepData :
    have gradsS := g.backpropSpec xS seedS;
    have gradsR :=
      (Proofs.RuntimeApprox.LinkAutogradAlgebra.RevGraph.toGraphData
            g).backpropCtx
        xR () seedR;
    have gradError :=
      (g.backpropBounds epsIn xR epsSeed seedR fun {Δ} =>
            Proofs.RuntimeApprox.NFBackend.ctxAddBound).get
        i;
    contract.stepDataValid stateS stateR stateError paramsS paramsR
      paramsError (Proofs.Autograd.Algebra.TList.get gradsS i)
      (gradsR.get i) gradError stepData) :
  have gradsS := g.backpropSpec xS seedS;
  have gradsR :=
    (Proofs.RuntimeApprox.LinkAutogradAlgebra.RevGraph.toGraphData
          g).backpropCtx
      xR () seedR;
  have gradError :=
    (g.backpropBounds epsIn xR epsSeed seedR fun {Δ} =>
          Proofs.RuntimeApprox.NFBackend.ctxAddBound).get
      i;
  have nextBound :=
    contract.updateBound stateError paramsError gradError stateR paramsR
      (gradsR.get i) stepData;
  contract.stateApprox
      (contract.updateSpec stateS paramsS
          (Proofs.Autograd.Algebra.TList.get gradsS i)).1
      (contract.updateRuntime stateR paramsR (gradsR.get i)).1
      nextBound.state ∧
    Proofs.RuntimeApprox.approxT Proofs.RuntimeApprox.NFBackend.toSpec
      (contract.updateSpec stateS paramsS
          (Proofs.Autograd.Algebra.TList.get gradsS i)).2
      (contract.updateRuntime stateR paramsR (gradsR.get i)).2
      nextBound.params
    theorem Proofs.RuntimeApprox.NFBackend.backprop_optimizer_update_approx_graphData
  {β : TorchLean.Floats.NeuralRadix}
  {fexp : ℤ → ℤ}
  [TorchLean.Floats.NeuralValidExp fexp]
  {rnd : ℝ → ℤ}
  [TorchLean.Floats.NeuralValidRndToNearest
      rnd]
  {Γ ss : List Spec.Shape}
  (g :
    Proofs.RuntimeApprox.RevGraph
      Proofs.RuntimeApprox.NFBackend.toSpec
      Γ ss)
  (i : Fin Γ.length)
  (contract :
    Proofs.RuntimeApprox.Optimizer.NumericalStepContract
      (TorchLean.Floats.NF β fexp rnd)
      Proofs.RuntimeApprox.NFBackend.toSpec)
  (xS :
    Proofs.RuntimeApprox.TList
      Spec.SpecScalar Γ)
  (xR :
    Proofs.RuntimeApprox.TList
      (TorchLean.Floats.NF β fexp rnd) Γ)
  (epsIn : Proofs.RuntimeApprox.EList Γ)
  (seedS :
    Proofs.RuntimeApprox.TList
      Spec.SpecScalar (Γ ++ ss))
  (seedR :
    Proofs.RuntimeApprox.TList
      (TorchLean.Floats.NF β fexp rnd)
      (Γ ++ ss))
  (epsSeed :
    Proofs.RuntimeApprox.EList (Γ ++ ss))
  (paramsS : Spec.Tensor ℝ (Γ.get i))
  (paramsR :
    Spec.Tensor
      (TorchLean.Floats.NF β fexp rnd)
      (Γ.get i))
  (paramsError : ℝ)
  (stateS : contract.StateSpec (Γ.get i))
  (stateR :
    contract.StateRuntime (Γ.get i))
  (stateError :
    contract.StateBound (Γ.get i))
  (stepData : contract.StepData (Γ.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.approxT
      Proofs.RuntimeApprox.NFBackend.toSpec
      paramsS paramsR paramsError)
  (hstate :
    contract.stateApprox stateS stateR
      stateError)
  (hstepData :
    have gradsS :=
      g.backpropSpec xS seedS;
    have gradsR :=
      (Proofs.RuntimeApprox.LinkAutogradAlgebra.RevGraph.toGraphData
            g).backpropCtx
        xR () seedR;
    have gradError :=
      (g.backpropBounds epsIn xR epsSeed
            seedR fun {Δ} =>
            Proofs.RuntimeApprox.NFBackend.ctxAddBound).get
        i;
    contract.stepDataValid stateS stateR
      stateError paramsS paramsR
      paramsError
      (Proofs.Autograd.Algebra.TList.get
        gradsS i)
      (gradsR.get i) gradError stepData) :
  have gradsS := g.backpropSpec xS seedS;
  have gradsR :=
    (Proofs.RuntimeApprox.LinkAutogradAlgebra.RevGraph.toGraphData
          g).backpropCtx
      xR () seedR;
  have gradError :=
    (g.backpropBounds epsIn xR epsSeed
          seedR fun {Δ} =>
          Proofs.RuntimeApprox.NFBackend.ctxAddBound).get
      i;
  have nextBound :=
    contract.updateBound stateError
      paramsError gradError stateR paramsR
      (gradsR.get i) stepData;
  contract.stateApprox
      (contract.updateSpec stateS paramsS
          (Proofs.Autograd.Algebra.TList.get
            gradsS i)).1
      (contract.updateRuntime stateR
          paramsR (gradsR.get i)).1
      nextBound.state ∧
    Proofs.RuntimeApprox.approxT
      Proofs.RuntimeApprox.NFBackend.toSpec
      (contract.updateSpec stateS paramsS
          (Proofs.Autograd.Algebra.TList.get
            gradsS i)).2
      (contract.updateRuntime stateR
          paramsR (gradsR.get i)).2
      nextBound.params
    Executable reverse mode followed by any valid numerical optimizer contract is sound.

The theorem is shape-polymorphic and optimizer-polymorphic. `stepDataValid` 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.17
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.

Definition8.2.18
Group: Operator bounds composed across programs. (6)
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.19
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

A checked numerical certificate retains the submitted artifact together with the canonical source ranges, node-range trace, accepted backend plan, and proofs that the recomputed trace and audit match the artifact.

Lean code for Definition8.2.18●1 definition
  • structure(7 fields)defined in NN/Proofs/RuntimeApprox/Graph/NumericalCertificate.lean
    complete
    structure Proofs.RuntimeApprox.NumericalCertificate.CheckedCertificate : Type
    structure Proofs.RuntimeApprox.NumericalCertificate.CheckedCertificate :
  Type
    Proof-carrying result returned by `check`. Raw endpoint data has been replaced by the canonical
trace reconstructed from the graph, and `backendPlan` contains the acceptance-gate proof.

    Fields

    graph : NN.IR.Graph
    The exact graph whose ranges and backend 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.AcceptedGraphPlan
    The backend 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.19
Group: Operator bounds composed across programs. (6)
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.20
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

For one checked certificate, CheckedRealExecution 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.19●1 definition
  • structure(5 fields)defined in NN/Proofs/RuntimeApprox/Graph/NumericalCertificate.lean
    complete
    structure Proofs.RuntimeApprox.NumericalCertificate.CheckedRealExecution
  (certificate :
    Proofs.RuntimeApprox.NumericalCertificate.CheckedCertificate) :
  Type
    structure Proofs.RuntimeApprox.NumericalCertificate.CheckedRealExecution
  (certificate :
    Proofs.RuntimeApprox.NumericalCertificate.CheckedCertificate) :
  Type
    Exact-real execution evidence for the graph stored in a 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 : NN.IR.DVal ℝ
    Real-valued graph input. 
    values : Array (NN.IR.DVal ℝ)
    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 : List.Forall₂ Proofs.RuntimeApprox.NumericalCertificate.RealDValEnclosed certificate.ranges.toList self.values.toList
    Pointwise evidence that every real node value lies in its checked interval.
Theorem8.2.20
Group: Operator bounds composed across programs. (6)
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.18
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.20●1 theorem
  • theoremdefined in NN/Proofs/RuntimeApprox/Graph/NumericalCertificate.lean
    complete
    theorem Proofs.RuntimeApprox.NumericalCertificate.CheckedExecution.errorTrace
  (execution :
    Proofs.RuntimeApprox.NumericalCertificate.CheckedExecution)
  (exact :
    Proofs.RuntimeApprox.NumericalCertificate.CheckedRealExecution
      execution.certificate) :
  Proofs.RuntimeApprox.NumericalCertificate.ExecutionErrorTrace
    execution.certificate.ranges.toList exact.values.toList
    execution.values.toList
    theorem Proofs.RuntimeApprox.NumericalCertificate.CheckedExecution.errorTrace
  (execution :
    Proofs.RuntimeApprox.NumericalCertificate.CheckedExecution)
  (exact :
    Proofs.RuntimeApprox.NumericalCertificate.CheckedRealExecution
      execution.certificate) :
  Proofs.RuntimeApprox.NumericalCertificate.ExecutionErrorTrace
    execution.certificate.ranges.toList
    exact.values.toList
    execution.values.toList
    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.20
uses 1

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