TorchLean

8.6. Models and Mathematical Examples🔗

The model API provides seeded architecture builders, while the proof library also studies compact mathematical models directly. The examples include an implemented MLP, reference specifications, and theorem families for approximation, diffusion, associative memory, reinforcement learning, attention, state-space models, and self-supervised objectives.

The links below identify the model semantics used by each result. An approximation theorem constructs parameters, a transition theorem describes a probability law, and a causality theorem compares executions with shared prefixes. Their conclusions answer different questions even when the surrounding application uses all three ideas.

Definition8.6.1
groupuses 0used by 1✓L∃∀N

nn.Builder is the state monad used by seeded builders. It threads an explicit SeedStream through a pure construction and yields the same result whenever nn.build starts from the same seed.

Lean code for Definition8.6.1●1 definition
  • abbrevdefined in NN/API/Seeded.lean
    complete
    abbrev TorchLean.nn.Builder.{u_1} (α : Type u_1) : Type u_1
    abbrev TorchLean.nn.Builder.{u_1}
  (α : Type u_1) : Type u_1
    Deterministic model builder that threads an explicit initialization seed stream.
Definition8.6.2
groupuses 1used by 0✓L∃∀N

This seeded builder constructs one batched, single-hidden-layer MLP: a linear layer, ReLU, and a second linear layer.

Lean code for Definition8.6.2●1 definition
  • defdefined in NN/API/Seeded.lean
    complete
    def TorchLean.nn.mlp (inputWidth outputWidth : ℕ)
  (config : TorchLean.nn.MLP.Config := { })
  (batchShape : Spec.Shape := []) :
  TorchLean.nn.Builder
    (TorchLean.nn.Sequential (batchShape.appendDim inputWidth)
      (batchShape.appendDim outputWidth))
    def TorchLean.nn.mlp
  (inputWidth outputWidth : ℕ)
  (config : TorchLean.nn.MLP.Config :=
    { })
  (batchShape : Spec.Shape := []) :
  TorchLean.nn.Builder
    (TorchLean.nn.Sequential
      (batchShape.appendDim inputWidth)
      (batchShape.appendDim outputWidth))
    Build a multilayer perceptron over any `batchShape`.

Each hidden width contributes a linear layer followed by the configured activation and optional
dropout. Initialization seeds come from the surrounding `Builder` seed stream.

Example:
```lean
-- `16 -> 32 -> 32 -> 1`, ReLU between hidden layers, dropout after each one.
def model : nn.Builder (nn.Sequential [16] [1]) :=
  nn.mlp 16 1 { hiddenWidths := [32, 32], activation := .relu, dropout? := some 0.1 }
```
Definition8.6.3
Group: Reference definitions used by the mathematical examples below. (2)
Group member previews
Preview
Definition 8.6.4
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

A k-nearest-neighbor model stores k together with a list of fixed-length feature vectors and their labels or regression targets. The structure itself does not assert any statistical property.

Lean code for Definition8.6.3●1 definition
  • structure(2 fields)defined in NN/Spec/Models/Knn.lean
    complete
    structure Spec.KNN (α : Type) [TorchLean.Storage α] (β : Type) (n : ℕ) : Type
    structure Spec.KNN (α : Type) [TorchLean.Storage α]
  (β : Type) (n : ℕ) : Type
    A small kNN model container (parameters + stored dataset).

This is a *lazy* model: inference consults the stored `dataset` at query time, rather than learning
weights.

    Fields

    k : ℕ
    Number of neighbors to consult. 
    dataset : Array (TorchLean.Tensor α [n] × β)
    Training data: feature vectors paired with labels/targets.
Definition8.6.4
Group: Reference definitions used by the mathematical examples below. (2)
Group member previews
Preview
Definition 8.6.3
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

A Hopfield state is a Boolean vector. Given a weight matrix and one threshold per coordinate, this update applies the threshold rule at one index, with ties sent to the active state.

Lean code for Definition8.6.4●1 definition
  • defdefined in NN/Spec/Models/Hopfield.lean
    complete
    def Spec.Hopfield.updateAt {α : Type} [AddCommMonoid α] [Mul α] [One α]
  [Neg α] [LE α] [DecidableRel fun x1 x2 => x1 ≤ x2] {n : ℕ}
  (p : Spec.Hopfield.Params α n) (s : Spec.Hopfield.State n)
  (u : Fin n) : Spec.Hopfield.State n
    def Spec.Hopfield.updateAt {α : Type}
  [AddCommMonoid α] [Mul α] [One α]
  [Neg α] [LE α]
  [DecidableRel fun x1 x2 => x1 ≤ x2]
  {n : ℕ} (p : Spec.Hopfield.Params α n)
  (s : Spec.Hopfield.State n)
  (u : Fin n) : Spec.Hopfield.State n
    Asynchronous update at a single coordinate `u`.

We implement the standard thresholded sign rule:

`s[u] := (θ_u ≤ net_u)`

Interpreting `true ↦ +1` and `false ↦ -1`, this corresponds to:

`x_u := +1` if `net_u ≥ θ_u`, otherwise `x_u := -1`.

Tie-handling (`net_u = θ_u`) matters for formal convergence arguments; we pick the convention
"ties go to `+1`" via `≤`.
Definition8.6.5
Group: Reference definitions used by the mathematical examples below. (2)
Group member previews
Preview
Definition 8.6.3
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

Over a field, Hopfield energy is the usual quadratic weight term plus the linear threshold term on the Boolean state's \{-1,1\} encoding.

Lean code for Definition8.6.5●1 definition
  • defdefined in NN/Spec/Models/Hopfield.lean
    complete
    def Spec.Hopfield.energy {α : Type} [Field α] {n : ℕ}
  (p : Spec.Hopfield.Params α n) (s : Spec.Hopfield.State n) : α
    def Spec.Hopfield.energy {α : Type} [Field α]
  {n : ℕ} (p : Spec.Hopfield.Params α n)
  (s : Spec.Hopfield.State n) : α
    The classical Hopfield energy for a state `s` (quadratic term + linear threshold term).

With `x = actVec s` the `±1` encoding, the energy is:

`E(s) = -1/2 * Σ_i Σ_j W_ij x_i x_j + Σ_i θ_i x_i`.

When `W` is symmetric and has a zero diagonal, asynchronous updates are known to monotonically
decrease (or not increase) `E`, which is the classic Lyapunov-style argument for convergence.
Theorem8.6.6
Group: Representative mathematical results attached to model semantics. (12)
Group member previews
Preview
Definition 8.6.7
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

Let a<b and L>0. If a real function is L-Lipschitz on [a,b], then for every positive error tolerance there is a two-layer ReLU MLP that stays within that tolerance throughout the interval. This uses the real instance of the scalar context.

Lean code for Theorem8.6.6●1 theorem
  • theoremdefined in NN/MLTheory/Proofs/Approximation/Universal/UniversalApproximation.lean
    complete
    theorem NN.MLTheory.Proofs.UniversalApproximation.relu_universal_approximation_Icc
  {f : ℝ → ℝ} {a b L : ℝ} (h_ab : a < b) (hL : 0 < L)
  (h_lip :
    ∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Icc a b, |f x - f y| ≤ L * |x - y|)
  (ε : ℝ) :
  ε > 0 →
    ∃ hidDim l1 l2,
      ∀ x ∈ Set.Icc a b,
        |f x -
              NN.MLTheory.Proofs.UniversalApproximation.mlpEvalScalar
                hidDim l1 l2 x| <
          ε
    theorem NN.MLTheory.Proofs.UniversalApproximation.relu_universal_approximation_Icc
  {f : ℝ → ℝ} {a b L : ℝ} (h_ab : a < b)
  (hL : 0 < L)
  (h_lip :
    ∀ x ∈ Set.Icc a b,
      ∀ y ∈ Set.Icc a b,
        |f x - f y| ≤ L * |x - y|)
  (ε : ℝ) :
  ε > 0 →
    ∃ hidDim l1 l2,
      ∀ x ∈ Set.Icc a b,
        |f x -
              NN.MLTheory.Proofs.UniversalApproximation.mlpEvalScalar
                hidDim l1 l2 x| <
          ε
    1D Universal Approximation (ReLU, one hidden layer), stated as an existence theorem for a 2-layer
  MLP.

This is a wrapper around `relu_universal_approximation_Icc_hinge` that instantiates the linear
  layers
as the explicit hinge construction.
Proof for Theorem 8.6.6
uses 1

A uniform grid gives a piecewise-linear approximation. Its slope changes become shifted ReLU hinges, and the shape-indexed tensor semantics show that the explicit two-layer MLP computes the resulting hinge sum exactly. The hidden units encode changes of slope, so their number depends on the grid needed for the requested tolerance. This constructs suitable parameters; it does not say that a particular training run finds them.

Definition8.6.7
Group: Representative mathematical results attached to model semantics. (12)
Group member previews
Preview
Theorem 8.6.6
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

A forward diffusion step scales the current value and adds independent Gaussian noise according to the schedule.

Lean code for Definition8.6.7●1 definition
  • defdefined in NN/Proofs/Probability/DiffusionForward.lean
    complete
    def NN.Proofs.Probability.forwardKernel.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] (a b : ℝ) : ProbabilityTheory.Kernel E E
    def NN.Proofs.Probability.forwardKernel.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] (a b : ℝ) :
  ProbabilityTheory.Kernel E E
    Forward noising kernel for a diffusion step, as a Markov kernel.
Theorem8.6.8
Group: Representative mathematical results attached to model semantics. (12)
Group member previews
Preview
Theorem 8.6.6
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

On a finite-dimensional real inner-product space with its Borel structure, each measure returned by the forward diffusion kernel is Gaussian.

Lean code for Theorem8.6.8●1 theorem
  • theoremdefined in NN/Proofs/Probability/DiffusionForward.lean
    complete
    theorem NN.Proofs.Probability.isGaussian_forwardKernel.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] (a b : ℝ) (x : E) :
  ProbabilityTheory.IsGaussian
    ((NN.Proofs.Probability.forwardKernel a b) x)
    theorem NN.Proofs.Probability.isGaussian_forwardKernel.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (a b : ℝ) (x : E) :
  ProbabilityTheory.IsGaussian
    ((NN.Proofs.Probability.forwardKernel
        a b)
      x)
    Each transition distribution of the forward kernel is Gaussian.
Proof for Theorem 8.6.8
uses 1

The forward kernel is identified with the affine image of a standard Gaussian, and affine images preserve Gaussianity. The state is held fixed when describing this transition law. The result explains the forward corruption distribution used in diffusion; it does not identify the law produced by a learned reverse denoiser.

Theorem8.6.9
Group: Representative mathematical results attached to model semantics. (12)
Group member previews
Preview
Theorem 8.6.6
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 8.6.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

For symmetric Hopfield weights with a zero diagonal, a state-changing sweep of asynchronous coordinate updates either lowers the energy or leaves it unchanged while strictly increasing the number of active coordinates.

Lean code for Theorem8.6.9●1 theorem
  • theoremdefined in NN/MLTheory/Proofs/Hopfield/Progress.lean
    complete
    theorem NN.MLTheory.Proofs.Hopfield.cycleUpdate_progress {n : ℕ}
  (p : Spec.Hopfield.Params ℝ n)
  (hsym : NN.MLTheory.Proofs.Hopfield.SymmetricW p)
  (hdiag : NN.MLTheory.Proofs.Hopfield.DiagonalZero p)
  (s : Spec.Hopfield.State n)
  (hchange : NN.MLTheory.Proofs.Hopfield.cycleUpdate p s ≠ s) :
  Spec.Hopfield.energy p (NN.MLTheory.Proofs.Hopfield.cycleUpdate p s) <
      Spec.Hopfield.energy p s ∨
    Spec.Hopfield.energy p
          (NN.MLTheory.Proofs.Hopfield.cycleUpdate p s) =
        Spec.Hopfield.energy p s ∧
      Spec.Hopfield.pluses
          (NN.MLTheory.Proofs.Hopfield.cycleUpdate p s) >
        Spec.Hopfield.pluses s
    theorem NN.MLTheory.Proofs.Hopfield.cycleUpdate_progress
  {n : ℕ} (p : Spec.Hopfield.Params ℝ n)
  (hsym :
    NN.MLTheory.Proofs.Hopfield.SymmetricW
      p)
  (hdiag :
    NN.MLTheory.Proofs.Hopfield.DiagonalZero
      p)
  (s : Spec.Hopfield.State n)
  (hchange :
    NN.MLTheory.Proofs.Hopfield.cycleUpdate
        p s ≠
      s) :
  Spec.Hopfield.energy p
        (NN.MLTheory.Proofs.Hopfield.cycleUpdate
          p s) <
      Spec.Hopfield.energy p s ∨
    Spec.Hopfield.energy p
          (NN.MLTheory.Proofs.Hopfield.cycleUpdate
            p s) =
        Spec.Hopfield.energy p s ∧
      Spec.Hopfield.pluses
          (NN.MLTheory.Proofs.Hopfield.cycleUpdate
            p s) >
        Spec.Hopfield.pluses s
    Every sweep that changes the state makes progress: either the energy strictly drops, or it stays
equal and the number of active units strictly rises.

This lexicographic measure is what `Convergence.lean` turns into termination. Energy alone is not
enough, because a unit sitting exactly at its threshold can flip without changing the energy.
Proof for Theorem 8.6.9
Proof uses 2
Proof dependency previews
Preview
Definition 8.6.4
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

The proof folds the one-coordinate energy inequalities over the updates in one sweep. When the state changes without lowering energy, the tie rule forces the active-coordinate count to increase. Energy alone would allow a state-changing step on a flat level set. Counting active coordinates supplies the extra progress needed to rule out returning around such a level set.

Theorem8.6.10
Group: Representative mathematical results attached to model semantics. (12)
Group member previews
Preview
Theorem 8.6.6
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

Under the same symmetry and zero-diagonal assumptions, the cycle progress theorem shows that any state lying on a positive-period cycle is already fixed by one full sweep.

Lean code for Theorem8.6.10●1 theorem
  • theoremdefined in NN/MLTheory/Proofs/Hopfield/Convergence.lean
    complete
    theorem NN.MLTheory.Proofs.Hopfield.cycleUpdate_no_nontrivial_cycles {n : ℕ}
  (p : Spec.Hopfield.Params ℝ n)
  (hsym : NN.MLTheory.Proofs.Hopfield.SymmetricW p)
  (hdiag : NN.MLTheory.Proofs.Hopfield.DiagonalZero p) {k : ℕ}
  (hk : 0 < k) (s : Spec.Hopfield.State n)
  (hcyc : (NN.MLTheory.Proofs.Hopfield.f p)^[k] s = s) :
  NN.MLTheory.Proofs.Hopfield.f p s = s
    theorem NN.MLTheory.Proofs.Hopfield.cycleUpdate_no_nontrivial_cycles
  {n : ℕ} (p : Spec.Hopfield.Params ℝ n)
  (hsym :
    NN.MLTheory.Proofs.Hopfield.SymmetricW
      p)
  (hdiag :
    NN.MLTheory.Proofs.Hopfield.DiagonalZero
      p)
  {k : ℕ} (hk : 0 < k)
  (s : Spec.Hopfield.State n)
  (hcyc :
    (NN.MLTheory.Proofs.Hopfield.f p)^[k]
        s =
      s) :
  NN.MLTheory.Proofs.Hopfield.f p s = s
    With symmetric weights and zero diagonal, a periodic orbit of the sweep is a fixed point.

This is the heart of the Hopfield convergence argument: energy never increases along a sweep, so on
a cycle it must be constant, and then the active-unit count would have to strictly increase around
the cycle and return to its starting value, which is impossible.
Proof for Theorem 8.6.10
uses 1

By cycle progress, a non-fixed first step would force lexicographic progress in energy and active-coordinate count. That progress cannot return to its starting value after finitely many sweeps.

Definition8.6.11
Group: Representative mathematical results attached to model semantics. (12)
Group member previews
Preview
Theorem 8.6.6
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

The distance between two real value functions is the supremum of their pointwise absolute differences.

Lean code for Definition8.6.11●1 definition
  • defdefined in NN/Proofs/RL/MarkovMDP.lean
    complete
    def Proofs.RL.Markov.valueSupDist {S : Type} [Nonempty S]
  (values₁ values₂ : Spec.RL.Markov.ValueFunction S) : ℝ
    def Proofs.RL.Markov.valueSupDist {S : Type}
  [Nonempty S]
  (values₁ values₂ :
    Spec.RL.Markov.ValueFunction S) :
  ℝ
    Sup distance on value functions, using `sSup` over pointwise absolute differences.
Theorem8.6.12
Group: Representative mathematical results attached to model semantics. (12)
Group member previews
Preview
Theorem 8.6.6
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N

For a valid MDP with a nonempty state space and a finite nonempty action space, the Bellman optimality operator contracts the sup distance between bounded measurable value functions by the discount factor.

Lean code for Theorem8.6.12●1 theorem
  • theoremdefined in NN/Proofs/RL/MarkovMDP.lean
    complete
    theorem Proofs.RL.Markov.bellmanOptimality_contraction {S A : Type}
  [MeasurableSpace S] [MeasurableSpace A] [Nonempty S]
  (mdp : Spec.RL.Markov.MDP S A) (valid : Spec.RL.Markov.Valid mdp)
  [Fintype A] [Nonempty A]
  (values₁ values₂ : Spec.RL.Markov.ValueFunction S)
  (hMeas₁ : Measurable values₁) (hMeas₂ : Measurable values₂)
  (hBdd₁ : BddAbove (Set.range fun s => |values₁ s|))
  (hBdd₂ : BddAbove (Set.range fun s => |values₂ s|)) :
  Proofs.RL.Markov.valueSupDist
      (Spec.RL.Markov.bellmanOptimality mdp values₁)
      (Spec.RL.Markov.bellmanOptimality mdp values₂) ≤
    mdp.discount * Proofs.RL.Markov.valueSupDist values₁ values₂
    theorem Proofs.RL.Markov.bellmanOptimality_contraction
  {S A : Type} [MeasurableSpace S]
  [MeasurableSpace A] [Nonempty S]
  (mdp : Spec.RL.Markov.MDP S A)
  (valid : Spec.RL.Markov.Valid mdp)
  [Fintype A] [Nonempty A]
  (values₁ values₂ :
    Spec.RL.Markov.ValueFunction S)
  (hMeas₁ : Measurable values₁)
  (hMeas₂ : Measurable values₂)
  (hBdd₁ :
    BddAbove
      (Set.range fun s => |values₁ s|))
  (hBdd₂ :
    BddAbove
      (Set.range fun s => |values₂ s|)) :
  Proofs.RL.Markov.valueSupDist
      (Spec.RL.Markov.bellmanOptimality
        mdp values₁)
      (Spec.RL.Markov.bellmanOptimality
        mdp values₂) ≤
    mdp.discount *
      Proofs.RL.Markov.valueSupDist
        values₁ values₂
    Bellman optimality is a `γ`-contraction in the sup metric (finite action space):

`valueSupDist (T* values₁) (T* values₂) ≤ γ * valueSupDist values₁ values₂`.
Proof for Theorem 8.6.12
uses 1

After unfolding the sup distance, the maximum over actions is nonexpansive, while integration scales the remaining pointwise difference by the discount factor.

Theorem8.6.13
Group: Representative mathematical results attached to model semantics. (12)
Group member previews
Preview
Theorem 8.6.6
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

For the same class of MDPs, the contraction bound shows that bounded measurable fixed points of the Bellman optimality operator coincide.

Lean code for Theorem8.6.13●1 theorem
  • theoremdefined in NN/Proofs/RL/MarkovMDP.lean
    complete
    theorem Proofs.RL.Markov.bellmanOptimality_fixedPoint_unique {S A : Type}
  [MeasurableSpace S] [MeasurableSpace A] [Nonempty S]
  (mdp : Spec.RL.Markov.MDP S A) (valid : Spec.RL.Markov.Valid mdp)
  [Fintype A] [Nonempty A] (v w : Spec.RL.Markov.ValueFunction S)
  (hv : Spec.RL.Markov.bellmanOptimality mdp v = v)
  (hw : Spec.RL.Markov.bellmanOptimality mdp w = w)
  (hMeasV : Measurable v) (hMeasW : Measurable w)
  (hBddV : BddAbove (Set.range fun s => |v s|))
  (hBddW : BddAbove (Set.range fun s => |w s|)) : v = w
    theorem Proofs.RL.Markov.bellmanOptimality_fixedPoint_unique
  {S A : Type} [MeasurableSpace S]
  [MeasurableSpace A] [Nonempty S]
  (mdp : Spec.RL.Markov.MDP S A)
  (valid : Spec.RL.Markov.Valid mdp)
  [Fintype A] [Nonempty A]
  (v w : Spec.RL.Markov.ValueFunction S)
  (hv :
    Spec.RL.Markov.bellmanOptimality mdp
        v =
      v)
  (hw :
    Spec.RL.Markov.bellmanOptimality mdp
        w =
      w)
  (hMeasV : Measurable v)
  (hMeasW : Measurable w)
  (hBddV :
    BddAbove (Set.range fun s => |v s|))
  (hBddW :
    BddAbove (Set.range fun s => |w s|)) :
  v = w
    If the Bellman optimality operator has a fixed point, it is unique (finite action space).
Proof for Theorem 8.6.13
uses 1

Applying the Bellman contraction to two fixed points gives d\le\gamma d. Since d\ge0 and \gamma<1, their sup distance is zero, forcing pointwise equality. Boundedness makes the distance a usable finite quantity, and the strict discount bound excludes the case where the inequality merely says d\le d. The result identifies a fixed point uniquely if one exists; it does not construct one here.

Theorem8.6.14
Group: Representative mathematical results attached to model semantics. (12)
Group member previews
Preview
Theorem 8.6.6
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N

For attention over shape-indexed tensors, the causal mask marks every strict-future key as blocked.

Lean code for Theorem8.6.14●1 theorem
  • theoremdefined in NN/Proofs/Models/Attention/CausalMask.lean
    complete
    theorem NN.Proofs.Models.Attention.causalMask_blocks_future {n : ℕ}
  (i j : Fin n) (hij : ↑i < ↑j) :
  Spec.get2 (Spec.causalMask n) i j = false
    theorem NN.Proofs.Models.Attention.causalMask_blocks_future
  {n : ℕ} (i j : Fin n) (hij : ↑i < ↑j) :
  Spec.get2 (Spec.causalMask n) i j =
    false
    A causal mask rejects every strict future key position.
Proof for Theorem 8.6.14
uses 1

The typed mask is read at the two indices, and the result follows from the comparison used to construct that entry.

Theorem8.6.15
Group: Representative mathematical results attached to model semantics. (12)
Group member previews
Preview
Theorem 8.6.6
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

Combined with the causal-mask result, exact hard-masked softmax assigns zero weight to every strict-future position.

Lean code for Theorem8.6.15●1 theorem
  • theoremdefined in NN/Proofs/Models/Attention/CausalMask.lean
    complete
    theorem NN.Proofs.Models.Attention.hardMaskedSoftmaxSpec_causal_future_zero
  {n : ℕ} (scores : TorchLean.Tensor ℝ [n, n]) (i j : Fin n)
  (hij : ↑i < ↑j) :
  Spec.get2 (Spec.hardMaskedSoftmaxSpec scores (Spec.causalMask n)) i
      j =
    0
    theorem NN.Proofs.Models.Attention.hardMaskedSoftmaxSpec_causal_future_zero
  {n : ℕ}
  (scores : TorchLean.Tensor ℝ [n, n])
  (i j : Fin n) (hij : ↑i < ↑j) :
  Spec.get2
      (Spec.hardMaskedSoftmaxSpec scores
        (Spec.causalMask n))
      i j =
    0
    In exact hard-masked causal softmax, every strict-future attention weight is exactly zero.
Proof for Theorem 8.6.15
uses 1

The causal-mask theorem selects the blocked branch, whose output is definitionally zero. The mask has shape [n,n], with rows representing queries and columns representing keys. Zero strict-future weights exclude those values from this attention mixture; causality of a complete model also depends on its other operations.

Theorem8.6.16
Group: Representative mathematical results attached to model semantics. (12)
Group member previews
Preview
Theorem 8.6.6
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

For compact Mamba runs over shape-indexed tensors, appending later inputs does not change the earlier output prefix.

Lean code for Theorem8.6.16●1 theorem
  • theoremdefined in NN/MLTheory/Proofs/StateSpace/MambaCausality.lean
    complete
    theorem NN.MLTheory.StateSpace.compactMamba_runArray_append_outputs_prefix
  {α : Type} [TorchLean.Storage α] [Context α]
  {inputDim stateDim outputDim : ℕ}
  (m : Models.MambaBlockSpec α inputDim stateDim outputDim)
  (h0 : TorchLean.Tensor α [stateDim])
  (xs ys : Array (TorchLean.Tensor α [inputDim])) :
  (m.runArray h0 (xs ++ ys)).2.take xs.size = (m.runArray h0 xs).2
    theorem NN.MLTheory.StateSpace.compactMamba_runArray_append_outputs_prefix
  {α : Type} [TorchLean.Storage α]
  [Context α]
  {inputDim stateDim outputDim : ℕ}
  (m :
    Models.MambaBlockSpec α inputDim
      stateDim outputDim)
  (h0 : TorchLean.Tensor α [stateDim])
  (xs ys :
    Array
      (TorchLean.Tensor α [inputDim])) :
  (m.runArray h0 (xs ++ ys)).2.take
      xs.size =
    (m.runArray h0 xs).2
    Compact Mamba prefix causality.

If a sequence `xs` has already been processed, appending future tokens `ys` cannot change the
outputs for `xs`.  This is the recurrent-model analogue of causal attention non-anticipation.
Proof for Theorem 8.6.16
uses 0

The generic array-scan prefix theorem shows that appending later inputs leaves every earlier step and state unchanged. The initial recurrent state is shared by both runs, so the comparison isolates appending inputs rather than restarting from a different memory. This is the property needed to reuse an already computed prefix when reasoning about a sequential implementation.

Definition8.6.17
Group: Representative mathematical results attached to model semantics. (12)
Group member previews
Preview
Theorem 8.6.6
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

This finite analogue of the VICReg variance term sums the natural-number hinge \gamma-v over already-computed coordinate summaries.

Lean code for Definition8.6.17●1 definition
  • defdefined in NN/MLTheory/SelfSupervised/VICReg.lean
    complete
    def NN.MLTheory.SelfSupervised.varianceTerm (gamma : ℕ)
  (variances : Array ℕ) : ℕ
    def NN.MLTheory.SelfSupervised.varianceTerm
  (gamma : ℕ) (variances : Array ℕ) : ℕ
    Sum of per-coordinate variance-floor penalties for one embedding branch.
Theorem8.6.18
Group: Representative mathematical results attached to model semantics. (12)
Group member previews
Preview
Theorem 8.6.6
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

If \gamma is positive, then the variance term is positive on any nonempty list in which every coordinate summary is zero. This finite arithmetic statement does not claim that an optimizer avoids collapse.

Lean code for Theorem8.6.18●1 theorem
  • theoremdefined in NN/MLTheory/SelfSupervised/VICReg.lean
    complete
    theorem NN.MLTheory.SelfSupervised.varianceTerm_collapsed_positive {gamma d : ℕ}
  (hγ : 0 < gamma) :
  0 <
    NN.MLTheory.SelfSupervised.varianceTerm gamma
      (Array.replicate (d + 1) 0)
    theorem NN.MLTheory.SelfSupervised.varianceTerm_collapsed_positive
  {gamma d : ℕ} (hγ : 0 < gamma) :
  0 <
    NN.MLTheory.SelfSupervised.varianceTerm
      gamma (Array.replicate (d + 1) 0)
    If $\gamma>0$ and there is at least one collapsed coordinate, the variance term is positive.
Proof for Theorem 8.6.18
uses 1

The variance sum on d+1 zeros is rewritten as (d+1)\gamma, whose factors are both positive. The nonempty condition matters because an empty summary has zero sum. Positivity assigns a cost to collapse; excluding a collapsed optimum would also require an attainable objective value below that cost and a link to the actual summaries.