TorchLean

8.5. Verification🔗

This part of the map follows proofs from local algebra to executable checkers. A solid dependency edge means the later statement uses the earlier definition or theorem. Runtime checkers that lack a proved acceptance-to-semantics bridge are described beside the matching proof work, without adding a dependency edge.

Definition8.5.1
Group: Algebraic, executable, and analytic accounts of reverse-mode differentiation. (10)
Group member previews
Preview
Definition 8.5.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0
Used by 3
Reverse dependency previews
Preview
Definition 8.5.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Each node in an algebraic proof graph carries forward, JVP, and VJP functions together with the local dot-product identity relating its JVP and VJP.

Lean code for Definition8.5.1●1 definition
  • structure(extends 1, 4 fields)defined in NN/Proofs/Autograd/Tape/Algebra/Soundness.lean
    complete
    structure Proofs.Autograd.Algebra.Node {α : Type} [CommSemiring α] (Δ : Type)
  (Γ : List Spec.Shape) (τ : Spec.Shape) : Type
    structure Proofs.Autograd.Algebra.Node {α : Type}
  [CommSemiring α] (Δ : Type)
  (Γ : List Spec.Shape) (τ : Spec.Shape) :
  Type
    Proof-carrying node: `NodeData` plus the local adjointness law.

The field `correct` is the algebraic version of the standard JVP/VJP inner-product law.

    Extends

    • Proofs.Autograd.Algebra.NodeData α Δ Γ τ

    Fields

    forward : Proofs.Autograd.Algebra.TList α Γ → Δ → Spec.Tensor α τ
    Inherited from
    1. Proofs.Autograd.Algebra.NodeData
    jvp : Proofs.Autograd.Algebra.TList α Γ → Proofs.Autograd.Algebra.TList α Γ → Δ → Spec.Tensor α τ
    Inherited from
    1. Proofs.Autograd.Algebra.NodeData
    vjp : Proofs.Autograd.Algebra.TList α Γ → Δ → Spec.Tensor α τ → Proofs.Autograd.Algebra.TList α Γ
    Inherited from
    1. Proofs.Autograd.Algebra.NodeData
    correct : ∀ (x dx : Proofs.Autograd.Algebra.TList α Γ) (d : Δ) (δ : Spec.Tensor α τ),
  Proofs.TensorAlgebra.dot (self.jvp x dx d) δ = dx.dotList (self.vjp x d δ)
    The node's JVP and VJP satisfy the local dot-product adjoint identity.
Definition8.5.2
Group: Algebraic, executable, and analytic accounts of reverse-mode differentiation. (10)
Group member previews
Preview
Definition 8.5.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N

GraphData stores a typed sequence of executable forward, JVP, and VJP node operations without local correctness proofs.

Lean code for Definition8.5.2●1 definition
  • inductive(2 constructors, 4 parameters)defined in NN/Proofs/Autograd/Tape/Algebra/Soundness.lean
    complete
    inductive Proofs.Autograd.Algebra.GraphData (α Δ : Type) (Γ : List Spec.Shape) :
  List Spec.Shape → Type
    inductive Proofs.Autograd.Algebra.GraphData
  (α Δ : Type) (Γ : List Spec.Shape) :
  List Spec.Shape → Type
    Executable-only graph: a snoc-list of `NodeData`.

    Constructors

    Proofs.Autograd.Algebra.GraphData.nil {α Δ : Type}
  {Γ : List Spec.Shape} :
  Proofs.Autograd.Algebra.GraphData α Δ Γ []
    A graph with no computed nodes; its context consists only of the inputs `Γ`. 
    Proofs.Autograd.Algebra.GraphData.snoc {α Δ : Type}
  {Γ ss : List Spec.Shape} {τ : Spec.Shape} :
  Proofs.Autograd.Algebra.GraphData α Δ Γ ss →
    Proofs.Autograd.Algebra.NodeData α Δ (Γ ++ ss) τ →
      Proofs.Autograd.Algebra.GraphData α Δ Γ (ss ++ [τ])
    Append one node whose inputs may use the original and previously computed values.
Definition8.5.3
Group: Algebraic, executable, and analytic accounts of reverse-mode differentiation. (10)
Group member previews
Preview
Definition 8.5.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.5.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

A proof-carrying algebraic graph is a typed sequence of locally correct nodes. Its output-shape list records each intermediate added to the graph.

Lean code for Definition8.5.3●1 definition
  • inductive(2 constructors, 5 parameters)defined in NN/Proofs/Autograd/Tape/Algebra/Soundness.lean
    complete
    inductive Proofs.Autograd.Algebra.Graph {α : Type} [CommSemiring α] (Δ : Type)
  (Γ : List Spec.Shape) : List Spec.Shape → Type
    inductive Proofs.Autograd.Algebra.Graph {α : Type}
  [CommSemiring α] (Δ : Type)
  (Γ : List Spec.Shape) :
  List Spec.Shape → Type
    A proof-carrying tape/SSA graph.

Nodes are appended in topological order and may reference any previously computed value.

    Constructors

    Proofs.Autograd.Algebra.Graph.nil {α : Type}
  [CommSemiring α] {Δ : Type} {Γ : List Spec.Shape} :
  Proofs.Autograd.Algebra.Graph Δ Γ []
    A graph with no computed nodes; its context consists only of the inputs `Γ`. 
    Proofs.Autograd.Algebra.Graph.snoc {α : Type}
  [CommSemiring α] {Δ : Type} {Γ ss : List Spec.Shape}
  {τ : Spec.Shape} :
  Proofs.Autograd.Algebra.Graph Δ Γ ss →
    Proofs.Autograd.Algebra.Node Δ (Γ ++ ss) τ →
      Proofs.Autograd.Algebra.Graph Δ Γ (ss ++ [τ])
    Append one locally correct node that may use the inputs and all preceding results.
Definition8.5.4
Group: Algebraic, executable, and analytic accounts of reverse-mode differentiation. (10)
Group member previews
Preview
Definition 8.5.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0
Used by 2
Reverse dependency previews
Preview
Definition 8.5.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

OpSpecCorrect packages a unary tensor operation, its JVP, and the local inner-product identity relating that JVP to the operation's VJP.

Lean code for Definition8.5.4●1 definition
  • structure(3 fields)defined in NN/Proofs/Autograd/Core/SemiringCorrectness.lean
    complete
    structure Proofs.Autograd.Algebra.OpSpecCorrect (α : Type) [CommSemiring α]
  (σ τ : Spec.Shape) : Type
    structure Proofs.Autograd.Algebra.OpSpecCorrect
  (α : Type) [CommSemiring α]
  (σ τ : Spec.Shape) : Type
    An `OpSpec` together with a matching JVP and a proof of VJP/JVP adjointness.

This is the backend-generic analogue of `Proofs.Autograd.OpSpecCorrect` from
`NN.Proofs.Autograd.Core.RealCorrectness`.

    Fields

    op : Spec.OpSpec α σ τ
    op. 
    jvp : Spec.Tensor α σ → Spec.Tensor α σ → Spec.Tensor α τ
    jvp. 
    correct : Proofs.Autograd.Algebra.VJPCorrect self.op.forward self.jvp self.op.backward
    correct.
Definition8.5.5
Group: Algebraic, executable, and analytic accounts of reverse-mode differentiation. (10)
Group member previews
Preview
Definition 8.5.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 8.5.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

The unary-operation adapter places an OpSpecCorrect value at a typed input index and produces a proof-carrying graph node.

Lean code for Definition8.5.5●1 definition
  • defdefined in NN/Proofs/Autograd/Tape/Algebra/Nodes.lean
    complete
    def Proofs.Autograd.Algebra.Node.ofOpSpecCorrect {α Δ : Type}
  [CommSemiring α] {Γ : List Spec.Shape} {σ τ : Spec.Shape}
  (idx : Proofs.Autograd.Algebra.Idx Γ σ)
  (op : Proofs.Autograd.Algebra.OpSpecCorrect α σ τ) :
  Proofs.Autograd.Algebra.Node Δ Γ τ
    def Proofs.Autograd.Algebra.Node.ofOpSpecCorrect
  {α Δ : Type} [CommSemiring α]
  {Γ : List Spec.Shape} {σ τ : Spec.Shape}
  (idx : Proofs.Autograd.Algebra.Idx Γ σ)
  (op :
    Proofs.Autograd.Algebra.OpSpecCorrect
      α σ τ) :
  Proofs.Autograd.Algebra.Node Δ Γ τ
    Build a proof-carrying unary node from an `OpSpecCorrect`.
Theorem8.5.6
Group: Algebraic, executable, and analytic accounts of reverse-mode differentiation. (10)
Group member previews
Preview
Definition 8.5.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

For an algebraic graph over a commutative semiring, reverse accumulation is adjoint to the graph JVP.

Lean code for Theorem8.5.6●1 theorem
  • theoremdefined in NN/Proofs/Autograd/Tape/Algebra/Soundness.lean
    complete
    theorem Proofs.Autograd.Algebra.Graph.backprop_correct {α : Type}
  [CommSemiring α] {Δ : Type} {Γ ss : List Spec.Shape}
  (g : Proofs.Autograd.Algebra.Graph Δ Γ ss)
  (x dx : Proofs.Autograd.Algebra.TList α Γ) (d : Δ)
  (seed : Proofs.Autograd.Algebra.TList α (Γ ++ ss)) :
  (g.jvpCtx x dx d).dotList seed = dx.dotList (g.backpropCtx x d seed)
    theorem Proofs.Autograd.Algebra.Graph.backprop_correct
  {α : Type} [CommSemiring α] {Δ : Type}
  {Γ ss : List Spec.Shape}
  (g :
    Proofs.Autograd.Algebra.Graph Δ Γ ss)
  (x dx :
    Proofs.Autograd.Algebra.TList α Γ)
  (d : Δ)
  (seed :
    Proofs.Autograd.Algebra.TList α
      (Γ ++ ss)) :
  (g.jvpCtx x dx d).dotList seed =
    dx.dotList (g.backpropCtx x d seed)
    Global tape soundness (algebraic form).

Assuming each node satisfies its local adjointness law, `backpropCtx` is the adjoint of `jvpCtx`
with respect to `TList.dotList`.
Proof for Theorem 8.5.6
uses 1

Graph induction expands the JVP and VJP at each node, then closes the new step with that node's local adjoint law.

Definition8.5.7
Group: Algebraic, executable, and analytic accounts of reverse-mode differentiation. (10)
Group member previews
Preview
Definition 8.5.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Theorem 8.1.7
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

The linear operation satisfies the unary operation contract over any commutative semiring. Its correctness field applies matrix-vector adjointness and commutativity of the tensor dot product.

Lean code for Definition8.5.7●1 definition
  • defdefined in NN/Proofs/Autograd/Core/SemiringCorrectness.lean
    complete
    def Proofs.Autograd.Algebra.linearCorrect {α : Type} [CommSemiring α]
  {inDim outDim : ℕ} (m : Spec.LinearSpec α inDim outDim) :
  Proofs.Autograd.Algebra.OpSpecCorrect α
    (Spec.Shape.dim inDim Spec.Shape.scalar)
    (Spec.Shape.dim outDim Spec.Shape.scalar)
    def Proofs.Autograd.Algebra.linearCorrect
  {α : Type} [CommSemiring α]
  {inDim outDim : ℕ}
  (m : Spec.LinearSpec α inDim outDim) :
  Proofs.Autograd.Algebra.OpSpecCorrect α
    (Spec.Shape.dim inDim
      Spec.Shape.scalar)
    (Spec.Shape.dim outDim
      Spec.Shape.scalar)
    Correctness of a linear layer’s backward rule (matrix–vector multiply), stated generically over `α`.

This is purely algebraic: it relies only on semiring laws and the adjointness lemma for matrix
multiplication in `TensorAlgebra`.
PyTorch analogue: `torch.nn.linear`’s linear map.
Theorem8.5.8
Group: Algebraic, executable, and analytic accounts of reverse-mode differentiation. (10)
Group member previews
Preview
Definition 8.5.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 8.3.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

Compiling an algebraic graph to the runtime tape and running dense backward returns the graph's proved reverse accumulator after its typed tensor context is converted to the runtime array representation.

Lean code for Theorem8.5.8●1 theorem
  • theoremdefined in NN/Proofs/Autograd/Runtime/Link/BackwardGraph.lean
    complete
    theorem Proofs.Autograd.Algebra.Graph.backwardDenseFrom_compileAux_eq_backpropAllCtx
  {α Δ : Type} [DecidableEq Spec.Shape] [CommSemiring α]
  {Γ ss : List Spec.Shape} (g : Proofs.Autograd.Algebra.Graph Δ Γ ss)
  (x : Proofs.Autograd.Algebra.TList α Γ) (d0 : Δ)
  (seed : Proofs.Autograd.Algebra.TList α (Γ ++ ss)) :
  (g.compileAux x d0).1.backwardDenseFrom seed.toAnyArray =
    Except.ok (g.backpropAllCtx x d0 seed).toAnyArray
    theorem Proofs.Autograd.Algebra.Graph.backwardDenseFrom_compileAux_eq_backpropAllCtx
  {α Δ : Type} [DecidableEq Spec.Shape]
  [CommSemiring α]
  {Γ ss : List Spec.Shape}
  (g :
    Proofs.Autograd.Algebra.Graph Δ Γ ss)
  (x : Proofs.Autograd.Algebra.TList α Γ)
  (d0 : Δ)
  (seed :
    Proofs.Autograd.Algebra.TList α
      (Γ ++ ss)) :
  (g.compileAux x d0).1.backwardDenseFrom
      seed.toAnyArray =
    Except.ok
      (g.backpropAllCtx x d0
          seed).toAnyArray
    **Main runtime/link theorem**: running the runtime dense backward loop on a tape produced by
`compileAux` matches the proved “full backpropagation” `backpropAllCtx`.

This is the formal statement that the executable engine implements the same reverse-mode
accumulation semantics as the proved tape model.
Proof for Theorem 8.5.8
Proof uses 2
Proof dependency previews
Preview
Definition 8.3.2
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

Induction over the compiled graph maintains the index and context correspondence of the runtime tape through reverse accumulation.

Theorem8.5.9
Group: Algebraic, executable, and analytic accounts of reverse-mode differentiation. (10)
Group member previews
Preview
Definition 8.5.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

For a real proof-carrying tape, the inner product of a JVP with a cotangent seed equals the inner product of the input tangent with reverse accumulation.

Lean code for Theorem8.5.9●1 theorem
  • theoremdefined in NN/Proofs/Autograd/Tape/Core/FDeriv.lean
    complete
    theorem Proofs.Autograd.Graph.backprop_correct_inner {Γ ss : List Spec.Shape}
  (g : Proofs.Autograd.Graph Γ ss) (xV dxV : Proofs.Autograd.CtxVec Γ)
  (seedV : Proofs.Autograd.CtxVec (Γ ++ ss)) :
  inner ℝ (g.jvpVec xV dxV) seedV = inner ℝ dxV (g.backpropVec xV seedV)
    theorem Proofs.Autograd.Graph.backprop_correct_inner
  {Γ ss : List Spec.Shape}
  (g : Proofs.Autograd.Graph Γ ss)
  (xV dxV : Proofs.Autograd.CtxVec Γ)
  (seedV :
    Proofs.Autograd.CtxVec (Γ ++ ss)) :
  inner ℝ (g.jvpVec xV dxV) seedV =
    inner ℝ dxV (g.backpropVec xV seedV)
    Vectorized tape soundness: `⟪jvp, seed⟫ = ⟪dx, backprop seed⟫`.
Proof for Theorem 8.5.9
uses 0

Tape induction applies each real node's local vector adjoint law while preserving the Euclidean inner product across context append and split operations.

Theorem8.5.10
Group: Algebraic, executable, and analytic accounts of reverse-mode differentiation. (10)
Group member previews
Preview
Definition 8.5.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

For differentiable real graph nodes, reverse accumulation equals the adjoint Fréchet derivative at the chosen point.

Lean code for Theorem8.5.10●1 theorem
  • theoremdefined in NN/Proofs/Autograd/Tape/Core/FDeriv.lean
    complete
    theorem Proofs.Autograd.Graph.backpropVec_eq_adjoint_fderiv_at
  {Γ ss : List Spec.Shape} (g : Proofs.Autograd.Graph Γ ss)
  (xV : Proofs.Autograd.CtxVec Γ)
  (seedV : Proofs.Autograd.CtxVec (Γ ++ ss)) :
  ∀ (a : Proofs.Autograd.GraphFDerivCorrectAt g xV),
    g.backpropVec xV seedV =
      (ContinuousLinearMap.adjoint (fderiv ℝ g.evalVec xV)) seedV
    theorem Proofs.Autograd.Graph.backpropVec_eq_adjoint_fderiv_at
  {Γ ss : List Spec.Shape}
  (g : Proofs.Autograd.Graph Γ ss)
  (xV : Proofs.Autograd.CtxVec Γ)
  (seedV :
    Proofs.Autograd.CtxVec (Γ ++ ss)) :
  ∀
    (a :
      Proofs.Autograd.GraphFDerivCorrectAt
        g xV),
    g.backpropVec xV seedV =
      (ContinuousLinearMap.adjoint
          (fderiv ℝ g.evalVec xV))
        seedV
    Pointwise version of `backpropVec_eq_adjoint_fderiv`.
Proof for Theorem 8.5.10
uses 1

Real tape soundness supplies the inner-product identity. The analytic hypotheses identify the graph JVP with a Fréchet derivative, and the adjoint is then characterized by its inner products.

Theorem8.5.11
Group: Algebraic, executable, and analytic accounts of reverse-mode differentiation. (10)
Group member previews
Preview
Definition 8.5.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N

For a real algebraic graph at a differentiable execution point, compiling the graph and running the exact dense tape returns the full algebraic reverse context. Its input prefix is the adjoint Fréchet derivative of graph evaluation applied to the output seed.

Lean code for Theorem8.5.11●1 theorem
  • theoremdefined in NN/Proofs/Autograd/Runtime/Link/FDeriv.lean
    complete
    theorem Proofs.Autograd.Algebra.Graph.backwardDenseFrom_compileAux_adjoint_fderiv_at
  {Δ : Type} {Γ : List Spec.Shape} [DecidableEq Spec.Shape]
  {ss : List Spec.Shape} (g : Proofs.Autograd.Algebra.Graph Δ Γ ss)
  (x : Proofs.Autograd.Algebra.TList ℝ Γ) (d0 : Δ)
  (seed : Proofs.Autograd.Algebra.TList ℝ (Γ ++ ss))
  (hg :
    Proofs.Autograd.GraphFDerivCorrectAt (g.toReal d0)
      (Proofs.Autograd.flattenCtx x)) :
  (g.compileAux x d0).1.backwardDenseFrom seed.toAnyArray =
      Except.ok (g.backpropAllCtx x d0 seed).toAnyArray ∧
    Proofs.Autograd.flattenCtx (g.backpropAllCtx x d0 seed).takeLeft =
      (ContinuousLinearMap.adjoint
          (fderiv ℝ (g.toReal d0).evalVec
            (Proofs.Autograd.flattenCtx x)))
        (Proofs.Autograd.flattenCtx seed)
    theorem Proofs.Autograd.Algebra.Graph.backwardDenseFrom_compileAux_adjoint_fderiv_at
  {Δ : Type} {Γ : List Spec.Shape}
  [DecidableEq Spec.Shape]
  {ss : List Spec.Shape}
  (g :
    Proofs.Autograd.Algebra.Graph Δ Γ ss)
  (x : Proofs.Autograd.Algebra.TList ℝ Γ)
  (d0 : Δ)
  (seed :
    Proofs.Autograd.Algebra.TList ℝ
      (Γ ++ ss))
  (hg :
    Proofs.Autograd.GraphFDerivCorrectAt
      (g.toReal d0)
      (Proofs.Autograd.flattenCtx x)) :
  (g.compileAux x d0).1.backwardDenseFrom
        seed.toAnyArray =
      Except.ok
        (g.backpropAllCtx x d0
            seed).toAnyArray ∧
    Proofs.Autograd.flattenCtx
        (g.backpropAllCtx x d0
            seed).takeLeft =
      (ContinuousLinearMap.adjoint
          (fderiv ℝ (g.toReal d0).evalVec
            (Proofs.Autograd.flattenCtx
              x)))
        (Proofs.Autograd.flattenCtx seed)
    Pointwise variant of `backwardDenseFrom_compileAux_adjoint_fderiv`.
Proof for Theorem 8.5.11
uses 1

The real, environment-free algebraic graph and the analytic graph convert in both directions while preserving evaluation, JVPs, and reverse accumulation. The compiled-tape correctness theorem gives the full cotangent context; prefix extraction identifies its input block with analytic backprop, and the analytic graph theorem identifies that value with the adjoint Fréchet derivative.

Definition8.5.12
Group: The proved forward compiler from typed TorchLean programs to verifier IR. (3)
Group member previews
Preview
Definition 8.5.13
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0
Used by 3
Reverse dependency previews
Preview
Definition 8.5.13
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The verified source language is a typed sequence of supported tensor operations with one input and shape-indexed intermediate values.

Lean code for Definition8.5.12●1 definition
  • abbrevdefined in NN/Verification/TorchLean/Proved/Syntax.lean
    complete
    abbrev NN.Verification.TorchLean.Proved.Program (α : Type)
  (paramShapes : List Spec.Shape) (inShape outShape : Spec.Shape) : Type
    abbrev NN.Verification.TorchLean.Proved.Program
  (α : Type)
  (paramShapes : List Spec.Shape)
  (inShape outShape : Spec.Shape) : Type
    A closed forward program from input `inShape` to output `outShape`.
Definition8.5.13
Group: The proved forward compiler from typed TorchLean programs to verifier IR. (3)
Group member previews
Preview
Definition 8.5.12
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 8.5.14
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

compileForward lowers the verified source program to the shared IR while preserving its typed node order.

Lean code for Definition8.5.13●1 definition
  • abbrevdefined in NN/Verification/TorchLean/Proved/Public.lean
    complete
    abbrev NN.Verification.TorchLean.Proved.compileForward {α : Type} [Context α]
  {paramShapes : List Spec.Shape} {inShape outShape : Spec.Shape}
  (p :
    NN.Verification.TorchLean.Proved.Program α paramShapes inShape
      outShape)
  (params : Runtime.Autograd.Torch.TList α paramShapes) :
  NN.Verification.TorchLean.CompiledIR α
    abbrev NN.Verification.TorchLean.Proved.compileForward
  {α : Type} [Context α]
  {paramShapes : List Spec.Shape}
  {inShape outShape : Spec.Shape}
  (p :
    NN.Verification.TorchLean.Proved.Program
      α paramShapes inShape outShape)
  (params :
    Runtime.Autograd.Torch.TList α
      paramShapes) :
  NN.Verification.TorchLean.CompiledIR α
    Compile a verified single-input forward program into the verifier IR.
Theorem8.5.14
Group: The proved forward compiler from typed TorchLean programs to verifier IR. (3)
Group member previews
Preview
Definition 8.5.12
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 8.1.17
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

Every graph produced by the verified forward compiler passes the IR structural well-formedness predicate.

Lean code for Theorem8.5.14●1 theorem
  • theoremdefined in NN/Verification/TorchLean/Proved/Public.lean
    complete
    theorem NN.Verification.TorchLean.Proved.compileForward_wellFormed {α : Type}
  [Context α] {paramShapes : List Spec.Shape}
  {inShape outShape : Spec.Shape}
  (p :
    NN.Verification.TorchLean.Proved.Program α paramShapes inShape
      outShape)
  (params : Runtime.Autograd.Torch.TList α paramShapes) :
  (NN.Verification.TorchLean.Proved.compileForward p
          params).graph.wellFormed =
    true
    theorem NN.Verification.TorchLean.Proved.compileForward_wellFormed
  {α : Type} [Context α]
  {paramShapes : List Spec.Shape}
  {inShape outShape : Spec.Shape}
  (p :
    NN.Verification.TorchLean.Proved.Program
      α paramShapes inShape outShape)
  (params :
    Runtime.Autograd.Torch.TList α
      paramShapes) :
  (NN.Verification.TorchLean.Proved.compileForward
          p params).graph.wellFormed =
    true
    Graph structural safety for the concise compiler name.
Proof for Theorem 8.5.14
Proof uses 2
Proof dependency previews
Preview
Definition 8.5.12
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

Induction over the source program shows that the compiler preserves the node-index invariant at every append.

Theorem8.5.15
Group: The proved forward compiler from typed TorchLean programs to verifier IR. (3)
Group member previews
Preview
Definition 8.5.12
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 0✓L∃∀N

Running the output of the verified forward compiler with the IR semantics gives the same result as evaluating the source forward program.

Lean code for Theorem8.5.15●1 theorem
  • theoremdefined in NN/Verification/TorchLean/Proved/Public.lean
    complete
    theorem NN.Verification.TorchLean.Proved.runForwardIR_eq_evalForward {α : Type}
  [Context α] [DecidableEq Spec.Shape] {paramShapes : List Spec.Shape}
  {inShape outShape : Spec.Shape}
  (p :
    NN.Verification.TorchLean.Proved.Program α paramShapes inShape
      outShape)
  (params : Runtime.Autograd.Torch.TList α paramShapes)
  (x : Spec.Tensor α inShape) :
  NN.Verification.TorchLean.runForwardIR
      (NN.Verification.TorchLean.Proved.compileForward p params) x =
    NN.Verification.TorchLean.Proved.evalForward p params x
    theorem NN.Verification.TorchLean.Proved.runForwardIR_eq_evalForward
  {α : Type} [Context α]
  [DecidableEq Spec.Shape]
  {paramShapes : List Spec.Shape}
  {inShape outShape : Spec.Shape}
  (p :
    NN.Verification.TorchLean.Proved.Program
      α paramShapes inShape outShape)
  (params :
    Runtime.Autograd.Torch.TList α
      paramShapes)
  (x : Spec.Tensor α inShape) :
  NN.Verification.TorchLean.runForwardIR
      (NN.Verification.TorchLean.Proved.compileForward
        p params)
      x =
    NN.Verification.TorchLean.Proved.evalForward
      p params x
    Main end-to-end compiler correctness using the short name.
Proof for Theorem 8.5.15
Proof uses 2
Proof dependency previews
Preview
Definition 8.1.20
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

Induction over the source program relates each compiled step to its matching IR denotation rule.

Theorem8.5.16
Group: Interval and affine certificate soundness. (7)
Group member previews
Preview
Theorem 8.5.17
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 8.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

A topologically sorted supported graph over shape-indexed tensors and ordered real scalars encloses every computed node value when its local semantic and box certificates are sound.

Lean code for Theorem8.5.16●1 theorem
  • theoremdefined in NN/MLTheory/CROWN/Proofs/GraphCertSoundness/Main.lean
    complete
    theorem NN.MLTheory.CROWN.Graph.CertSoundness.cert_encloses_semantics
  (g : NN.MLTheory.CROWN.Graph)
  (ps : NN.MLTheory.CROWN.Graph.ParamStore ℝ)
  (cert : Array (Option (NN.MLTheory.CROWN.FlatBox ℝ)))
  (inputs : Std.HashMap ℕ NN.MLTheory.CROWN.Graph.CertSoundness.Val)
  (vals : Array (Option NN.MLTheory.CROWN.Graph.CertSoundness.Val))
  (htopo : NN.MLTheory.CROWN.Graph.CertSoundness.TopoSorted g)
  (hsupp : NN.MLTheory.CROWN.Graph.CertSoundness.Supported g)
  (hcert : NN.MLTheory.CROWN.Graph.CertSoundness.CertLocalOK g ps cert)
  (hsem :
    NN.MLTheory.CROWN.Graph.CertSoundness.SemLocalOK g ps inputs vals)
  (hinputs :
    NN.MLTheory.CROWN.Graph.CertSoundness.InputsEnclosed g ps inputs)
  (id : ℕ) :
  id < g.nodes.size →
    match cert[id]!, vals[id]! with
    | some B, some v =>
      NN.MLTheory.CROWN.Graph.CertSoundness.EnclosesBox B v
    | x, x_1 => True
    theorem NN.MLTheory.CROWN.Graph.CertSoundness.cert_encloses_semantics
  (g : NN.MLTheory.CROWN.Graph)
  (ps :
    NN.MLTheory.CROWN.Graph.ParamStore ℝ)
  (cert :
    Array
      (Option
        (NN.MLTheory.CROWN.FlatBox ℝ)))
  (inputs :
    Std.HashMap ℕ
      NN.MLTheory.CROWN.Graph.CertSoundness.Val)
  (vals :
    Array
      (Option
        NN.MLTheory.CROWN.Graph.CertSoundness.Val))
  (htopo :
    NN.MLTheory.CROWN.Graph.CertSoundness.TopoSorted
      g)
  (hsupp :
    NN.MLTheory.CROWN.Graph.CertSoundness.Supported
      g)
  (hcert :
    NN.MLTheory.CROWN.Graph.CertSoundness.CertLocalOK
      g ps cert)
  (hsem :
    NN.MLTheory.CROWN.Graph.CertSoundness.SemLocalOK
      g ps inputs vals)
  (hinputs :
    NN.MLTheory.CROWN.Graph.CertSoundness.InputsEnclosed
      g ps inputs)
  (id : ℕ) :
  id < g.nodes.size →
    match cert[id]!, vals[id]! with
    | some B, some v =>
      NN.MLTheory.CROWN.Graph.CertSoundness.EnclosesBox
        B v
    | x, x_1 => True
Proof for Theorem 8.5.16
Proof uses 2
Proof dependency previews
Preview
Definition 8.1.1
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

Topological induction follows the graph's tensor values and applies each local enclosure result using the order from the real scalar setting.

Theorem8.5.17
Group: Interval and affine certificate soundness. (7)
Group member previews
Preview
Theorem 8.5.16
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

The concrete real runIBP? pass supplies the certificates required by the local soundness theorem, so it encloses the recursive graph semantics whenever it succeeds.

Lean code for Theorem8.5.17●1 theorem
  • theoremdefined in NN/MLTheory/CROWN/Proofs/GraphRunibpEndToEnd.lean
    complete
    theorem NN.MLTheory.CROWN.Graph.CertSoundness.runIBP?_encloses_evalGraphRec
  (g : NN.MLTheory.CROWN.Graph)
  (ps : NN.MLTheory.CROWN.Graph.ParamStore ℝ)
  (inputs : Std.HashMap ℕ NN.MLTheory.CROWN.Graph.CertSoundness.Val)
  (htopo : NN.MLTheory.CROWN.Graph.CertSoundness.TopoSorted g)
  (hsupp : NN.MLTheory.CROWN.Graph.CertSoundness.Supported g)
  (hinputs :
    NN.MLTheory.CROWN.Graph.CertSoundness.InputsEnclosed g ps inputs)
  (id : ℕ) :
  id < g.nodes.size →
    match (NN.MLTheory.CROWN.Graph.CertSoundness.runIBP? g ps)[id]!,
      (NN.MLTheory.CROWN.Graph.CertSoundness.evalGraphRec g ps
          inputs)[id]! with
    | some B, some v =>
      NN.MLTheory.CROWN.Graph.CertSoundness.EnclosesBox B v
    | x, x_1 => True
    theorem NN.MLTheory.CROWN.Graph.CertSoundness.runIBP?_encloses_evalGraphRec
  (g : NN.MLTheory.CROWN.Graph)
  (ps :
    NN.MLTheory.CROWN.Graph.ParamStore ℝ)
  (inputs :
    Std.HashMap ℕ
      NN.MLTheory.CROWN.Graph.CertSoundness.Val)
  (htopo :
    NN.MLTheory.CROWN.Graph.CertSoundness.TopoSorted
      g)
  (hsupp :
    NN.MLTheory.CROWN.Graph.CertSoundness.Supported
      g)
  (hinputs :
    NN.MLTheory.CROWN.Graph.CertSoundness.InputsEnclosed
      g ps inputs)
  (id : ℕ) :
  id < g.nodes.size →
    match
      (NN.MLTheory.CROWN.Graph.CertSoundness.runIBP?
          g ps)[id]!,
      (NN.MLTheory.CROWN.Graph.CertSoundness.evalGraphRec
          g ps inputs)[id]! with
    | some B, some v =>
      NN.MLTheory.CROWN.Graph.CertSoundness.EnclosesBox
        B v
    | x, x_1 => True
Proof for Theorem 8.5.17
uses 1

The executable pass is shown to produce the local certificates required by the generic soundness theorem.

Definition8.5.18
Group: Interval and affine certificate soundness. (7)
Group member previews
Preview
Theorem 8.5.16
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0
Used by 3
Reverse dependency previews
Preview
Theorem 8.5.19
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

An affine transfer implementation satisfies this contract when each backward transfer preserves the represented lower and upper bounds.

Lean code for Definition8.5.18●1 definition
  • defdefined in NN/MLTheory/CROWN/Proofs/GraphCrownCertSoundness.lean
    complete
    def NN.MLTheory.CROWN.Graph.CrownCertSoundness.CrownTransferSound
  (g : NN.MLTheory.CROWN.Graph)
  (_ps : NN.MLTheory.CROWN.Graph.ParamStore ℝ)
  (_inputs :
    Std.HashMap ℕ NN.MLTheory.CROWN.Graph.CrownCertSoundness.Val)
  (vals : Array (Option NN.MLTheory.CROWN.Graph.CrownCertSoundness.Val))
  (ctx : NN.MLTheory.CROWN.Graph.AffineCtx)
  (x : Spec.Tensor ℝ (Spec.Shape.dim ctx.inputDim Spec.Shape.scalar))
  (step :
    Array (Option (NN.MLTheory.CROWN.Graph.FlatAffineBounds ℝ)) →
      ℕ → Option (NN.MLTheory.CROWN.Graph.FlatAffineBounds ℝ))
  (cert : Array (Option (NN.MLTheory.CROWN.Graph.FlatAffineBounds ℝ))) :
  Prop
    def NN.MLTheory.CROWN.Graph.CrownCertSoundness.CrownTransferSound
  (g : NN.MLTheory.CROWN.Graph)
  (_ps :
    NN.MLTheory.CROWN.Graph.ParamStore ℝ)
  (_inputs :
    Std.HashMap ℕ
      NN.MLTheory.CROWN.Graph.CrownCertSoundness.Val)
  (vals :
    Array
      (Option
        NN.MLTheory.CROWN.Graph.CrownCertSoundness.Val))
  (ctx :
    NN.MLTheory.CROWN.Graph.AffineCtx)
  (x :
    Spec.Tensor ℝ
      (Spec.Shape.dim ctx.inputDim
        Spec.Shape.scalar))
  (step :
    Array
        (Option
          (NN.MLTheory.CROWN.Graph.FlatAffineBounds
            ℝ)) →
      ℕ →
        Option
          (NN.MLTheory.CROWN.Graph.FlatAffineBounds
            ℝ))
  (cert :
    Array
      (Option
        (NN.MLTheory.CROWN.Graph.FlatAffineBounds
          ℝ))) :
  Prop
Theorem8.5.19
Group: Interval and affine certificate soundness. (7)
Group member previews
Preview
Theorem 8.5.16
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

A locally consistent real affine certificate encloses graph semantics when its transfer step satisfies CrownTransferSound.

Lean code for Theorem8.5.19●1 theorem
  • theoremdefined in NN/MLTheory/CROWN/Proofs/GraphCrownCertSoundness.lean
    complete
    theorem NN.MLTheory.CROWN.Graph.CrownCertSoundness.crown_checker_encloses_semantics
  (g : NN.MLTheory.CROWN.Graph)
  (ps : NN.MLTheory.CROWN.Graph.ParamStore ℝ)
  (step :
    Array (Option (NN.MLTheory.CROWN.Graph.FlatAffineBounds ℝ)) →
      ℕ → Option (NN.MLTheory.CROWN.Graph.FlatAffineBounds ℝ))
  (cert : Array (Option (NN.MLTheory.CROWN.Graph.FlatAffineBounds ℝ)))
  (inputs :
    Std.HashMap ℕ NN.MLTheory.CROWN.Graph.CrownCertSoundness.Val)
  (vals : Array (Option NN.MLTheory.CROWN.Graph.CrownCertSoundness.Val))
  (ctx : NN.MLTheory.CROWN.Graph.AffineCtx)
  (x : Spec.Tensor ℝ (Spec.Shape.dim ctx.inputDim Spec.Shape.scalar))
  (htopo : NN.MLTheory.CROWN.Graph.CrownCertSoundness.TopoSorted g)
  (hsem :
    NN.MLTheory.CROWN.Graph.CrownCertSoundness.SemLocalOK g ps inputs
      vals)
  (hcert :
    NN.MLTheory.CROWN.Graph.CrownCertSoundness.CrownCertLocalOK g step
      cert)
  (hsound :
    NN.MLTheory.CROWN.Graph.CrownCertSoundness.CrownTransferSound g ps
      inputs vals ctx x step cert)
  (id : ℕ) :
  id < g.nodes.size →
    ∀ (b : NN.MLTheory.CROWN.Graph.FlatAffineBounds ℝ)
      (v : NN.MLTheory.CROWN.Graph.CrownCertSoundness.Val),
      cert[id]! = some b →
        vals[id]! = some v →
          NN.MLTheory.CROWN.Graph.CrownCertSoundness.EnclosesAtInput ctx
            x b v
    theorem NN.MLTheory.CROWN.Graph.CrownCertSoundness.crown_checker_encloses_semantics
  (g : NN.MLTheory.CROWN.Graph)
  (ps :
    NN.MLTheory.CROWN.Graph.ParamStore ℝ)
  (step :
    Array
        (Option
          (NN.MLTheory.CROWN.Graph.FlatAffineBounds
            ℝ)) →
      ℕ →
        Option
          (NN.MLTheory.CROWN.Graph.FlatAffineBounds
            ℝ))
  (cert :
    Array
      (Option
        (NN.MLTheory.CROWN.Graph.FlatAffineBounds
          ℝ)))
  (inputs :
    Std.HashMap ℕ
      NN.MLTheory.CROWN.Graph.CrownCertSoundness.Val)
  (vals :
    Array
      (Option
        NN.MLTheory.CROWN.Graph.CrownCertSoundness.Val))
  (ctx :
    NN.MLTheory.CROWN.Graph.AffineCtx)
  (x :
    Spec.Tensor ℝ
      (Spec.Shape.dim ctx.inputDim
        Spec.Shape.scalar))
  (htopo :
    NN.MLTheory.CROWN.Graph.CrownCertSoundness.TopoSorted
      g)
  (hsem :
    NN.MLTheory.CROWN.Graph.CrownCertSoundness.SemLocalOK
      g ps inputs vals)
  (hcert :
    NN.MLTheory.CROWN.Graph.CrownCertSoundness.CrownCertLocalOK
      g step cert)
  (hsound :
    NN.MLTheory.CROWN.Graph.CrownCertSoundness.CrownTransferSound
      g ps inputs vals ctx x step cert)
  (id : ℕ) :
  id < g.nodes.size →
    ∀
      (b :
        NN.MLTheory.CROWN.Graph.FlatAffineBounds
          ℝ)
      (v :
        NN.MLTheory.CROWN.Graph.CrownCertSoundness.Val),
      cert[id]! = some b →
        vals[id]! = some v →
          NN.MLTheory.CROWN.Graph.CrownCertSoundness.EnclosesAtInput
            ctx x b v
Proof for Theorem 8.5.19
uses 1

Reverse topological induction composes the certified affine forms and discharges each node with the transfer-soundness premise.

Theorem8.5.20
Group: Interval and affine certificate soundness. (7)
Group member previews
Preview
Theorem 8.5.16
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N

The concrete real α-CROWN transfer step satisfies the generic transfer contract.

Lean code for Theorem8.5.20●1 theorem
  • theoremdefined in NN/MLTheory/CROWN/Proofs/GraphAlphaCrownTransferSoundness/Alpha.lean
    complete
    theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.alphaCrown_transfer_sound
  (g : NN.MLTheory.CROWN.Graph)
  (ps : NN.MLTheory.CROWN.Graph.ParamStore ℝ)
  (ibp : Array (Option (NN.MLTheory.CROWN.FlatBox ℝ)))
  (alpha : Array (Option (NN.MLTheory.CROWN.Graph.FlatVec ℝ)))
  (cert : Array (Option (NN.MLTheory.CROWN.Graph.FlatAffineBounds ℝ)))
  (inputs :
    Std.HashMap ℕ
      NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Val)
  (vals :
    Array
      (Option NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Val))
  (ctx : NN.MLTheory.CROWN.Graph.AffineCtx)
  (x : Spec.Tensor ℝ (Spec.Shape.dim ctx.inputDim Spec.Shape.scalar))
  (htopo :
    NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.TopoSorted g)
  (hsem :
    NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.SemLocalOK g ps
      inputs vals)
  (hinputs :
    NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.InputsMatch
      inputs ctx x)
  (hibp :
    NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.IBPEnclosesVals
      ibp vals)
  (halpha :
    NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.AlphaOK alpha) :
  NN.MLTheory.CROWN.Graph.CrownCertSoundness.CrownTransferSound g ps
    inputs vals ctx x
    (NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.stepAlpha g ps
      ibp alpha ctx)
    cert
    theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.alphaCrown_transfer_sound
  (g : NN.MLTheory.CROWN.Graph)
  (ps :
    NN.MLTheory.CROWN.Graph.ParamStore ℝ)
  (ibp :
    Array
      (Option
        (NN.MLTheory.CROWN.FlatBox ℝ)))
  (alpha :
    Array
      (Option
        (NN.MLTheory.CROWN.Graph.FlatVec
          ℝ)))
  (cert :
    Array
      (Option
        (NN.MLTheory.CROWN.Graph.FlatAffineBounds
          ℝ)))
  (inputs :
    Std.HashMap ℕ
      NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Val)
  (vals :
    Array
      (Option
        NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Val))
  (ctx :
    NN.MLTheory.CROWN.Graph.AffineCtx)
  (x :
    Spec.Tensor ℝ
      (Spec.Shape.dim ctx.inputDim
        Spec.Shape.scalar))
  (htopo :
    NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.TopoSorted
      g)
  (hsem :
    NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.SemLocalOK
      g ps inputs vals)
  (hinputs :
    NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.InputsMatch
      inputs ctx x)
  (hibp :
    NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.IBPEnclosesVals
      ibp vals)
  (halpha :
    NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.AlphaOK
      alpha) :
  NN.MLTheory.CROWN.Graph.CrownCertSoundness.CrownTransferSound
    g ps inputs vals ctx x
    (NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.stepAlpha
      g ps ibp alpha ctx)
    cert
    Pointwise soundness of the graph-dialect α-CROWN transfer rule.

Fix a graph `g`, parameters `ps`, an input point `x`, and a locally-consistent value semantics
array `vals` (i.e. `vals[id]` agrees with evaluating node `id` from its parents’ values).

Assume:

- the designated input node in `inputs` matches `x` (`InputsMatch`),
- the IBP boxes `ibp` enclose the semantic values in `vals` (`IBPEnclosesVals`), and
- the α parameters are well-formed (`AlphaOK`).

Then the concrete step function `alphaCrownStepNode?` satisfies the abstract
`CrownTransferSound` requirement: whenever every parent `p` is enclosed by its certificate entry,
the current node `id` is enclosed by the step-produced certificate entry as well.

This is the key lemma that lets `alphaCrownStepNode?` plug into the generic end-to-end checker
theorem in `NN.MLTheory.CROWN.Proofs.GraphCrownCertSoundness`.
Proof for Theorem 8.5.20
uses 1

The proof checks the affine relaxation chosen for each supported operation against the generic transfer contract.

Theorem8.5.21
Group: Interval and affine certificate soundness. (7)
Group member previews
Preview
Theorem 8.5.16
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 8.5.18
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

The α/β-CROWN transfer step satisfies the transfer contract. Unchanged nodes reduce to the α-CROWN transfer theorem.

Lean code for Theorem8.5.21●1 theorem
  • theoremdefined in NN/MLTheory/CROWN/Proofs/GraphAlphaCrownTransferSoundness/AlphaBeta.lean
    complete
    theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.alphaBetaCrown_transfer_sound
  (g : NN.MLTheory.CROWN.Graph)
  (ps : NN.MLTheory.CROWN.Graph.ParamStore ℝ)
  (ibp : Array (Option (NN.MLTheory.CROWN.FlatBox ℝ)))
  (alpha : Array (Option (NN.MLTheory.CROWN.Graph.FlatVec ℝ)))
  (beta : Array (Option (Array ℤ)))
  (cert : Array (Option (NN.MLTheory.CROWN.Graph.FlatAffineBounds ℝ)))
  (inputs :
    Std.HashMap ℕ
      NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Val)
  (vals :
    Array
      (Option NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Val))
  (ctx : NN.MLTheory.CROWN.Graph.AffineCtx)
  (x : Spec.Tensor ℝ (Spec.Shape.dim ctx.inputDim Spec.Shape.scalar))
  (htopo :
    NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.TopoSorted g)
  (hsem :
    NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.SemLocalOK g ps
      inputs vals)
  (hinputs :
    NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.InputsMatch
      inputs ctx x)
  (hibp :
    NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.IBPEnclosesVals
      ibp vals)
  (halpha :
    NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.AlphaOK alpha) :
  NN.MLTheory.CROWN.Graph.CrownCertSoundness.CrownTransferSound g ps
    inputs vals ctx x
    (NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.stepAlphaBeta g
      ps ibp alpha beta ctx)
    cert
    theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.alphaBetaCrown_transfer_sound
  (g : NN.MLTheory.CROWN.Graph)
  (ps :
    NN.MLTheory.CROWN.Graph.ParamStore ℝ)
  (ibp :
    Array
      (Option
        (NN.MLTheory.CROWN.FlatBox ℝ)))
  (alpha :
    Array
      (Option
        (NN.MLTheory.CROWN.Graph.FlatVec
          ℝ)))
  (beta : Array (Option (Array ℤ)))
  (cert :
    Array
      (Option
        (NN.MLTheory.CROWN.Graph.FlatAffineBounds
          ℝ)))
  (inputs :
    Std.HashMap ℕ
      NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Val)
  (vals :
    Array
      (Option
        NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Val))
  (ctx :
    NN.MLTheory.CROWN.Graph.AffineCtx)
  (x :
    Spec.Tensor ℝ
      (Spec.Shape.dim ctx.inputDim
        Spec.Shape.scalar))
  (htopo :
    NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.TopoSorted
      g)
  (hsem :
    NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.SemLocalOK
      g ps inputs vals)
  (hinputs :
    NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.InputsMatch
      inputs ctx x)
  (hibp :
    NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.IBPEnclosesVals
      ibp vals)
  (halpha :
    NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.AlphaOK
      alpha) :
  NN.MLTheory.CROWN.Graph.CrownCertSoundness.CrownTransferSound
    g ps inputs vals ctx x
    (NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.stepAlphaBeta
      g ps ibp alpha beta ctx)
    cert
    Pointwise soundness of the graph-dialect α/β-CROWN transfer rule.

This is the β-extended analog of `alphaCrown_transfer_sound`.

Compared to plain α-CROWN, the step function additionally receives a `beta` array encoding
per-ReLU phase constraints (active/inactive/unstable). When a phase is consistent with the IBP
pre-activation interval, the relaxation reduces to an exact affine rule for that unit; otherwise
the step falls back to the corresponding sound α-CROWN relaxation, or to an IBP-derived constant
enclosure for operators outside this affine-transfer subset.

The theorem states that this concrete step function satisfies `CrownTransferSound`, and thus can
be used as the trusted “checker semantics” in `graph_crown_cert_soundness`.
Proof for Theorem 8.5.21
uses 1

Split constraints are handled directly. The remaining operations reuse the α-CROWN transfer proof.

Definition8.5.22
Group: Interval and affine certificate soundness. (7)
Group member previews
Preview
Theorem 8.5.16
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N

The executable checker parses and replays an IEEE32Exec node certificate. Its final acceptance decision has a proved bridge to the proposition-level local replay condition. Connecting that binary32 condition to the real enclosure in Theorem 8.5.19 still requires the refinement assumptions for the operations in the graph.

Lean code for Definition8.5.22●1 definition
  • defdefined in NN/Verification/Cert/CROWNNodeCertAlphaBeta.lean
    complete
    def NN.Verification.CROWNNodeCertAlphaBeta.checkAlphaBetaCROWNNodeCertificate
  (g : NN.MLTheory.CROWN.Graph)
  (ps :
    NN.MLTheory.CROWN.Graph.ParamStore
      TorchLean.Floats.IEEE754.IEEE32Exec)
  (path : String) : IO Bool
    def NN.Verification.CROWNNodeCertAlphaBeta.checkAlphaBetaCROWNNodeCertificate
  (g : NN.MLTheory.CROWN.Graph)
  (ps :
    NN.MLTheory.CROWN.Graph.ParamStore
      TorchLean.Floats.IEEE754.IEEE32Exec)
  (path : String) : IO Bool
    Check a per-node α/β-CROWN certificate against Lean's propagation rules.

Returns `true` iff every supplied IBP box contains Lean's authoritative recomputation and every
node's affine replay data agrees exactly with Lean's α/β-CROWN step.
Theorem8.5.23
Group: Interval and affine certificate soundness. (7)
Group member previews
Preview
Theorem 8.5.16
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N

Acceptance of the in-memory α/β-CROWN decision implies CrownCertLocalOK for the exact IEEE32Exec replay step used by the checker.

Lean code for Theorem8.5.23●1 theorem
  • theoremdefined in NN/Verification/Cert/CROWNNodeCertAlphaBeta.lean
    complete
    theorem NN.Verification.CROWNNodeCertAlphaBeta.AlphaBetaCROWNNodeCertificate.accepts_eq_true
  (cert :
    NN.Verification.CROWNNodeCertAlphaBeta.AlphaBetaCROWNNodeCertificate)
  (g : NN.MLTheory.CROWN.Graph)
  (ps :
    NN.MLTheory.CROWN.Graph.ParamStore
      TorchLean.Floats.IEEE754.IEEE32Exec)
  (authoritativeIbp :
    Array
      (Option
        (NN.MLTheory.CROWN.FlatBox
          TorchLean.Floats.IEEE754.IEEE32Exec)))
  (diagnosticsOk : Bool)
  (haccept : cert.accepts g ps authoritativeIbp diagnosticsOk = true) :
  NN.MLTheory.CROWN.Graph.CrownCertSoundness.CrownCertLocalOK g
    (NN.Verification.CROWNNodeCertAlphaBeta.replayStep g ps
      authoritativeIbp cert)
    cert.crown
    theorem NN.Verification.CROWNNodeCertAlphaBeta.AlphaBetaCROWNNodeCertificate.accepts_eq_true
  (cert :
    NN.Verification.CROWNNodeCertAlphaBeta.AlphaBetaCROWNNodeCertificate)
  (g : NN.MLTheory.CROWN.Graph)
  (ps :
    NN.MLTheory.CROWN.Graph.ParamStore
      TorchLean.Floats.IEEE754.IEEE32Exec)
  (authoritativeIbp :
    Array
      (Option
        (NN.MLTheory.CROWN.FlatBox
          TorchLean.Floats.IEEE754.IEEE32Exec)))
  (diagnosticsOk : Bool)
  (haccept :
    cert.accepts g ps authoritativeIbp
        diagnosticsOk =
      true) :
  NN.MLTheory.CROWN.Graph.CrownCertSoundness.CrownCertLocalOK
    g
    (NN.Verification.CROWNNodeCertAlphaBeta.replayStep
      g ps authoritativeIbp cert)
    cert.crown
    Acceptance of the concrete α/β-CROWN decision supplies graph-level local consistency.
Proof for Theorem 8.5.23
uses 0

The checker compares every dependent affine record bit-for-bit. Soundness of the tensor, matrix, affine-vector, and optional-record comparisons turns the successful Boolean replay into equality at every graph node.

Definition8.5.24
Group: Selected end-to-end mathematical results and explicit assumptions. (6)
Group member previews
Preview
Theorem 8.5.25
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

A Lyapunov certificate is valid for a pair of functions when its two intervals enclose the function and orbital-derivative values throughout the stated region.

Lean code for Definition8.5.24●1 definition
  • structure(2 fields)defined in NN/MLTheory/CROWN/Lyapunov/Certificate.lean
    complete
    structure NN.MLTheory.CROWN.Lyapunov.LyapunovCert.ValidFor {α : Type} [Context α]
  {n : ℕ} (cert : NN.MLTheory.CROWN.Lyapunov.LyapunovCert α n)
  (lyap : NN.MLTheory.CROWN.Lyapunov.NeuralLyapunov α n) : Prop
    structure NN.MLTheory.CROWN.Lyapunov.LyapunovCert.ValidFor
  {α : Type} [Context α] {n : ℕ}
  (cert :
    NN.MLTheory.CROWN.Lyapunov.LyapunovCert
      α n)
  (lyap :
    NN.MLTheory.CROWN.Lyapunov.NeuralLyapunov
      α n) :
  Prop
    Proof object produced by a semantic certificate checker.

Parsing a certificate or checking the signs of its endpoints cannot construct this structure. Its
two fields require enclosure proofs for the actual functions named by `lyap` on the actual region
stored in `cert`.

    Fields

    valueBounds : ∀ (x : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)),
  cert.region.contains x → cert.vLower ≤ lyap.value x ∧ lyap.value x ≤ cert.vUpper
    The checked interval for the Lyapunov candidate. 
    orbitalDerivativeBounds : ∀ (x : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)),
  cert.region.contains x →
    cert.derivativeLower ≤ lyap.orbitalDerivative x ∧ lyap.orbitalDerivative x ≤ cert.derivativeUpper
    The checked interval for the orbital derivative.
Theorem8.5.25
Group: Selected end-to-end mathematical results and explicit assumptions. (6)
Group member previews
Preview
Definition 8.5.24
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

Certificate thresholds imply positive Lyapunov values and negative derivatives on the certified region, conditional on the certificate validity predicate.

Lean code for Theorem8.5.25●1 theorem
  • theoremdefined in NN/MLTheory/CROWN/Lyapunov/Verification.lean
    complete
    theorem NN.MLTheory.CROWN.Lyapunov.Real.lyapunov_conditions {n : ℕ}
  (lyap : NN.MLTheory.CROWN.Lyapunov.NeuralLyapunov ℝ n)
  (cert : NN.MLTheory.CROWN.Lyapunov.LyapunovCert ℝ n)
  (hcert : cert.ValidFor lyap) (h_V_pos : cert.vLower > 0)
  (h_Vdot_neg : cert.derivativeUpper < 0) :
  (∀ (x : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)),
      cert.region.contains x → lyap.value x > 0) ∧
    ∀ (x : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)),
      cert.region.contains x → lyap.orbitalDerivative x < 0
    theorem NN.MLTheory.CROWN.Lyapunov.Real.lyapunov_conditions
  {n : ℕ}
  (lyap :
    NN.MLTheory.CROWN.Lyapunov.NeuralLyapunov
      ℝ n)
  (cert :
    NN.MLTheory.CROWN.Lyapunov.LyapunovCert
      ℝ n)
  (hcert : cert.ValidFor lyap)
  (h_V_pos : cert.vLower > 0)
  (h_Vdot_neg :
    cert.derivativeUpper < 0) :
  (∀
      (x :
        Spec.Tensor ℝ
          (Spec.Shape.dim n
            Spec.Shape.scalar)),
      cert.region.contains x →
        lyap.value x > 0) ∧
    ∀
      (x :
        Spec.Tensor ℝ
          (Spec.Shape.dim n
            Spec.Shape.scalar)),
      cert.region.contains x →
        lyap.orbitalDerivative x < 0
    Positivity and decay follow from valid strict certificate margins.
Proof for Theorem 8.5.25
uses 1

The enclosures in the validity hypothesis are compared with the certificate thresholds and strengthened to strict sign conditions.

Theorem8.5.26
Group: Selected end-to-end mathematical results and explicit assumptions. (6)
Group member previews
Preview
Definition 8.5.24
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N

Under the stated strong-monotonicity, Lipschitz, and step-size hypotheses, the iterates satisfy

\left\lVert \operatorname{step}_{\eta}(g)^{\,k}(x)-x^\star\right\rVert^2 \leq q(\eta,\mu,L)^k\left\lVert x-x^\star\right\rVert^2.

Lean code for Theorem8.5.26●1 theorem
  • theoremdefined in NN/MLTheory/Optimization/StronglyConvexGD.lean
    complete
    theorem Optim.GD.dist_sq_iterate_le_of_q_nonneg {E : Type}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (η μ : ℝ) (hη : 0 ≤ η)
  {L : NNReal} (g : E → E) (hmono : Optim.GD.StrongMonotone μ g)
  (hlip : LipschitzWith L g) {xStar x : E} (hxStar : g xStar = 0)
  (hq : 0 ≤ Optim.GD.q η μ L) (k : ℕ) :
  ‖(Optim.GD.step η g)^[k] x - xStar‖ ^ 2 ≤
    Optim.GD.q η μ L ^ k * ‖x - xStar‖ ^ 2
    theorem Optim.GD.dist_sq_iterate_le_of_q_nonneg
  {E : Type} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (η μ : ℝ)
  (hη : 0 ≤ η) {L : NNReal} (g : E → E)
  (hmono : Optim.GD.StrongMonotone μ g)
  (hlip : LipschitzWith L g) {xStar x : E}
  (hxStar : g xStar = 0)
  (hq : 0 ≤ Optim.GD.q η μ L) (k : ℕ) :
  ‖(Optim.GD.step η g)^[k] x - xStar‖ ^
      2 ≤
    Optim.GD.q η μ L ^ k * ‖x - xStar‖ ^ 2
    Iterated contraction bound in squared norm.

If $q(\eta,\mu,L)\geq 0$, then after $k$ steps we have

$$
\left\lVert \operatorname{step}_\eta(g)^{\,k}(x)-x^\star\right\rVert^2
  \leq q(\eta,\mu,L)^k\lVert x-x^\star\rVert^2.
$$
Proof for Theorem 8.5.26
uses 0

The one-step contraction is iterated, and nonnegativity of q(\eta,\mu,L) controls multiplication by the geometric factor.

Theorem8.5.27
Group: Selected end-to-end mathematical results and explicit assumptions. (6)
Group member previews
Preview
Definition 8.5.24
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N

Measurable post-processing preserves (\varepsilon,\delta)-differential privacy.

Lean code for Theorem8.5.27●1 theorem
  • theoremdefined in NN/MLTheory/LearningTheory/DifferentialPrivacy/Core.lean
    complete
    theorem NN.MLTheory.LearningTheory.differentialPrivacy_postprocess
  {α β γ : Type} {Adj : α → α → Prop} [MeasurableSpace β]
  [MeasurableSpace γ] {M : NN.MLTheory.LearningTheory.Mechanism α β}
  {ε : ℝ} {δ : ENNReal} {f : β → γ} (hf : Measurable f) :
  NN.MLTheory.LearningTheory.DifferentialPrivacy Adj M ε δ →
    NN.MLTheory.LearningTheory.DifferentialPrivacy Adj
      (NN.MLTheory.LearningTheory.postprocess M f hf) ε δ
    theorem NN.MLTheory.LearningTheory.differentialPrivacy_postprocess
  {α β γ : Type} {Adj : α → α → Prop}
  [MeasurableSpace β] [MeasurableSpace γ]
  {M :
    NN.MLTheory.LearningTheory.Mechanism α
      β}
  {ε : ℝ} {δ : ENNReal} {f : β → γ}
  (hf : Measurable f) :
  NN.MLTheory.LearningTheory.DifferentialPrivacy
      Adj M ε δ →
    NN.MLTheory.LearningTheory.DifferentialPrivacy
      Adj
      (NN.MLTheory.LearningTheory.postprocess
        M f hf)
      ε δ
    Post-processing theorem: measurable mappings of outputs preserve DP.

Proof idea (the standard one):

- the probability of an event `S` under the mapped output is the probability of the preimage
  `f ⁻¹' S` under the original output;
- apply DP for `M` to the measurable set `f ⁻¹' S`.
Proof for Theorem 8.5.27
uses 0

The proof rewrites measurable preimages through the post-processing map and reuses the original privacy inequality.

Theorem8.5.28
Group: Selected end-to-end mathematical results and explicit assumptions. (6)
Group member previews
Preview
Definition 8.5.24
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

Assuming real approximation, parameter quantization, and IEEE32 execution budgets for a two-layer ReLU network, the total error is bounded by their sum.

Lean code for Theorem8.5.28●1 theorem
  • theoremdefined in NN/MLTheory/Proofs/Approximation/Universal/UniversalApproximationIEEE32ExecTwoLayerMlp.lean
    complete
    theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecTwoLayerMLP.relu_twoLayerMlp_ieee32exec_threeTerm
  {n hidDim : ℕ}
  (D :
    Set
      (Spec.Tensor TorchLean.Floats.IEEE754.IEEE32Exec
        (Spec.Shape.dim n Spec.Shape.scalar)))
  (f : NN.MLTheory.Proofs.ReLUMlpBridge.TensorVec n → ℝ)
  (l1R : Spec.LinearSpec ℝ n hidDim) (l2R : Spec.LinearSpec ℝ hidDim 1)
  (l1I : Spec.LinearSpec TorchLean.Floats.IEEE754.IEEE32Exec n hidDim)
  (l2I : Spec.LinearSpec TorchLean.Floats.IEEE754.IEEE32Exec hidDim 1)
  (εApprox εQ εR : ℝ)
  (hApprox :
    ∀ xI ∈ D,
      have xR :=
        NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecCore.tensorToReal
          xI;
      |f xR - NN.MLTheory.Proofs.ReLUMlpBridge.mlpEvalNd l1R l2R xR| ≤
        εApprox)
  (hQ :
    ∀ xI ∈ D,
      have xR :=
        NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecCore.tensorToReal
          xI;
      |NN.MLTheory.Proofs.ReLUMlpBridge.mlpEvalNd l1R l2R xR -
            NN.MLTheory.Proofs.ReLUMlpBridge.mlpEvalNd
              (NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecCore.linearSpecToReal
                l1I)
              (NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecCore.linearSpecToReal
                l2I)
              xR| ≤
        εQ)
  (hR :
    ∀ xI ∈ D,
      have xR :=
        NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecCore.tensorToReal
          xI;
      |(NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecCore.mlpEvalNdIeee32exec
                l1I l2I xI).toReal -
            NN.MLTheory.Proofs.ReLUMlpBridge.mlpEvalNd
              (NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecCore.linearSpecToReal
                l1I)
              (NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecCore.linearSpecToReal
                l2I)
              xR| ≤
        εR)
  (xI :
    Spec.Tensor TorchLean.Floats.IEEE754.IEEE32Exec
      (Spec.Shape.dim n Spec.Shape.scalar)) :
  xI ∈ D →
    have xR :=
      NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecCore.tensorToReal
        xI;
    |f xR -
          (NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecCore.mlpEvalNdIeee32exec
              l1I l2I xI).toReal| ≤
      εApprox + εQ + εR
    theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecTwoLayerMLP.relu_twoLayerMlp_ieee32exec_threeTerm
  {n hidDim : ℕ}
  (D :
    Set
      (Spec.Tensor
        TorchLean.Floats.IEEE754.IEEE32Exec
        (Spec.Shape.dim n
          Spec.Shape.scalar)))
  (f :
    NN.MLTheory.Proofs.ReLUMlpBridge.TensorVec
        n →
      ℝ)
  (l1R : Spec.LinearSpec ℝ n hidDim)
  (l2R : Spec.LinearSpec ℝ hidDim 1)
  (l1I :
    Spec.LinearSpec
      TorchLean.Floats.IEEE754.IEEE32Exec
      n hidDim)
  (l2I :
    Spec.LinearSpec
      TorchLean.Floats.IEEE754.IEEE32Exec
      hidDim 1)
  (εApprox εQ εR : ℝ)
  (hApprox :
    ∀ xI ∈ D,
      have xR :=
        NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecCore.tensorToReal
          xI;
      |f xR -
            NN.MLTheory.Proofs.ReLUMlpBridge.mlpEvalNd
              l1R l2R xR| ≤
        εApprox)
  (hQ :
    ∀ xI ∈ D,
      have xR :=
        NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecCore.tensorToReal
          xI;
      |NN.MLTheory.Proofs.ReLUMlpBridge.mlpEvalNd
              l1R l2R xR -
            NN.MLTheory.Proofs.ReLUMlpBridge.mlpEvalNd
              (NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecCore.linearSpecToReal
                l1I)
              (NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecCore.linearSpecToReal
                l2I)
              xR| ≤
        εQ)
  (hR :
    ∀ xI ∈ D,
      have xR :=
        NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecCore.tensorToReal
          xI;
      |(NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecCore.mlpEvalNdIeee32exec
                l1I l2I xI).toReal -
            NN.MLTheory.Proofs.ReLUMlpBridge.mlpEvalNd
              (NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecCore.linearSpecToReal
                l1I)
              (NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecCore.linearSpecToReal
                l2I)
              xR| ≤
        εR)
  (xI :
    Spec.Tensor
      TorchLean.Floats.IEEE754.IEEE32Exec
      (Spec.Shape.dim n
        Spec.Shape.scalar)) :
  xI ∈ D →
    have xR :=
      NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecCore.tensorToReal
        xI;
    |f xR -
          (NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecCore.mlpEvalNdIeee32exec
              l1I l2I xI).toReal| ≤
      εApprox + εQ + εR
Proof for Theorem 8.5.28
uses 1

After interpreting the IEEE32 result as a real value, two triangle inequalities split the target error into the three assumed budgets.

Theorem8.5.29
Group: Selected end-to-end mathematical results and explicit assumptions. (6)
Group member previews
Preview
Definition 8.5.24
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N

A comparison argument encloses a clamped scalar ODE solution with constant extension outside the integration interval.

Lean code for Theorem8.5.29●1 theorem
  • theoremdefined in NN/Proofs/Verification/ODE/Enclosure.lean
    complete
    theorem NN.Proofs.Verification.ODE.Enclosure.extendedSolutionEnclosed_fromClampedDynamics
  {T τ : ℝ} (hT : 0 ≤ T) (hτ : T ≤ τ) {f : ℝ → ℝ → ℝ}
  {u uL uU uL' uU' : ℝ → ℝ} {a : ℝ}
  (hu_cont : ContinuousOn u (Set.Icc 0 τ))
  (hu_der :
    ∀ t ∈ Set.Ico 0 τ,
      HasDerivWithinAt u
        (f t
          (NN.Proofs.Verification.ODE.Enclosure.clampToCorridor
            (NN.Proofs.Verification.ODE.Enclosure.constantExtensionAfter
              T uL)
            (NN.Proofs.Verification.ODE.Enclosure.constantExtensionAfter
              T uU)
            t (u t)))
        (Set.Ici t) t)
  (hu0 : u 0 = a) (hL_cont : ContinuousOn uL (Set.Icc 0 T))
  (hL_der :
    ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt uL (uL' t) (Set.Ici t) t)
  (hL_sub : ∀ t ∈ Set.Ico 0 T, uL' t ≤ f t (uL t)) (hL0 : uL 0 ≤ a)
  (hU_cont : ContinuousOn uU (Set.Icc 0 T))
  (hU_der :
    ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt uU (uU' t) (Set.Ici t) t)
  (hU_sup : ∀ t ∈ Set.Ico 0 T, f t (uU t) ≤ uU' t) (hU0 : a ≤ uU 0)
  (hLU : ∀ t ∈ Set.Icc 0 T, uL t ≤ uU t)
  (hLower : ∀ (t : ℝ), T < t → 0 ≤ f T (uL T) ∧ f T (uL T) ≤ f t (uL T))
  (hUpper :
    ∀ (t : ℝ), T < t → f t (uU T) ≤ f T (uU T) ∧ f T (uU T) ≤ 0) :
  (∀ t ∈ Set.Icc 0 τ,
      NN.Proofs.Verification.ODE.Enclosure.constantExtensionAfter T uL
            t ≤
          u t ∧
        u t ≤
          NN.Proofs.Verification.ODE.Enclosure.constantExtensionAfter T
            uU t) ∧
    ∀ t ∈ Set.Ico 0 τ, HasDerivWithinAt u (f t (u t)) (Set.Ici t) t
    theorem NN.Proofs.Verification.ODE.Enclosure.extendedSolutionEnclosed_fromClampedDynamics
  {T τ : ℝ} (hT : 0 ≤ T) (hτ : T ≤ τ)
  {f : ℝ → ℝ → ℝ}
  {u uL uU uL' uU' : ℝ → ℝ} {a : ℝ}
  (hu_cont : ContinuousOn u (Set.Icc 0 τ))
  (hu_der :
    ∀ t ∈ Set.Ico 0 τ,
      HasDerivWithinAt u
        (f t
          (NN.Proofs.Verification.ODE.Enclosure.clampToCorridor
            (NN.Proofs.Verification.ODE.Enclosure.constantExtensionAfter
              T uL)
            (NN.Proofs.Verification.ODE.Enclosure.constantExtensionAfter
              T uU)
            t (u t)))
        (Set.Ici t) t)
  (hu0 : u 0 = a)
  (hL_cont :
    ContinuousOn uL (Set.Icc 0 T))
  (hL_der :
    ∀ t ∈ Set.Ico 0 T,
      HasDerivWithinAt uL (uL' t)
        (Set.Ici t) t)
  (hL_sub :
    ∀ t ∈ Set.Ico 0 T, uL' t ≤ f t (uL t))
  (hL0 : uL 0 ≤ a)
  (hU_cont :
    ContinuousOn uU (Set.Icc 0 T))
  (hU_der :
    ∀ t ∈ Set.Ico 0 T,
      HasDerivWithinAt uU (uU' t)
        (Set.Ici t) t)
  (hU_sup :
    ∀ t ∈ Set.Ico 0 T, f t (uU t) ≤ uU' t)
  (hU0 : a ≤ uU 0)
  (hLU : ∀ t ∈ Set.Icc 0 T, uL t ≤ uU t)
  (hLower :
    ∀ (t : ℝ),
      T < t →
        0 ≤ f T (uL T) ∧
          f T (uL T) ≤ f t (uL T))
  (hUpper :
    ∀ (t : ℝ),
      T < t →
        f t (uU T) ≤ f T (uU T) ∧
          f T (uU T) ≤ 0) :
  (∀ t ∈ Set.Icc 0 τ,
      NN.Proofs.Verification.ODE.Enclosure.constantExtensionAfter
            T uL t ≤
          u t ∧
        u t ≤
          NN.Proofs.Verification.ODE.Enclosure.constantExtensionAfter
            T uU t) ∧
    ∀ t ∈ Set.Ico 0 τ,
      HasDerivWithinAt u (f t (u t))
        (Set.Ici t) t
    Constant-extension enclosure theorem:

Assume we have `uL,uU` on `[0,T]` satisfying the local corridor hypotheses, and assume the paper's
extra sign/monotonicity conditions for `f` beyond `T`. Then for any `τ ≥ T`, any solution `u` of
the clamped ODE built from the constant extensions is enclosed on `[0,τ]` and is a genuine solution
of `u' = f(t,u)` on `[0,τ]`.

This is the reusable Lean form of the paper's global-in-time step: after the verified horizon, the
walls stop moving, and the vector field points inward at those frozen walls.
Proof for Theorem 8.5.29
uses 0

The proof combines the in-interval differential inequality with the two constant-extension cases.

Theorem8.5.30
Group: Selected end-to-end mathematical results and explicit assumptions. (6)
Group member previews
Preview
Definition 8.5.24
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

Acceptance by the boolean 3D box and camera checker over shape-indexed inputs yields a Verified3DBox certificate.

Lean code for Theorem8.5.30●1 theorem
  • theoremdefined in NN/Verification/Geometry3D/Box3D.lean
    complete
    theorem NN.Verification.Geometry3D.Box3D.checkCert_sound {α : Type} [OfNat α 0]
  [OfNat α 1] [Add α] [Sub α] [Mul α] [Div α] [LE α] [LT α]
  [DecidableRel fun x1 x2 => x1 ≤ x2]
  [DecidableRel fun x1 x2 => x1 < x2]
  {cert : NN.Verification.Geometry3D.Box3D.BoxCameraCert α}
  (h : NN.Verification.Geometry3D.Box3D.checkCert cert = true) :
  NN.Verification.Geometry3D.Box3D.Verified3DBox cert
    theorem NN.Verification.Geometry3D.Box3D.checkCert_sound
  {α : Type} [OfNat α 0] [OfNat α 1]
  [Add α] [Sub α] [Mul α] [Div α] [LE α]
  [LT α]
  [DecidableRel fun x1 x2 => x1 ≤ x2]
  [DecidableRel fun x1 x2 => x1 < x2]
  {cert :
    NN.Verification.Geometry3D.Box3D.BoxCameraCert
      α}
  (h :
    NN.Verification.Geometry3D.Box3D.checkCert
        cert =
      true) :
  NN.Verification.Geometry3D.Box3D.Verified3DBox
    cert
    Soundness of the executable checker.

This is the main theorem for the implementation: if the Boolean checker accepts an artifact, the
artifact satisfies the mathematical `Verified3DBox` predicate.
Proof for Theorem 8.5.30
uses 1

Each boolean guard over the tensor inputs is reflected into its proposition and assembled into the certificate structure.