Sparse VJP Contexts

Shape-indexed context builders used by the NF reverse-mode proofs. These helpers write only the positions touched by a local VJP rule and leave every other component at zero, which lets the sparse cases avoid unnecessary rounded additions.

Sparse Contexts For Local VJPs

def Proofs.RuntimeApprox.SparseContext.zeros {α : Type} [TorchLean.Storage α] [Zero α] {ss : List Spec.Shape} : TorchLean.TensorPack α ss

A TorchLean.TensorPack filled with zeros (shape-wise), used to build sparse contexts for local VJPs.

def Proofs.RuntimeApprox.SparseContext.setIdx {α : Type} [TorchLean.Storage α] [Zero α] {Γ : List Spec.Shape} {s : Spec.Shape} : Idx Γ s → TorchLean.Tensor α s → TorchLean.TensorPack α Γ

Set a single Idx position in a TorchLean.TensorPack, filling all other entries with zeros.

def Proofs.RuntimeApprox.SparseContext.set2Idx {α : Type} [TorchLean.Storage α] [Zero α] [Add α] {Γ : List Spec.Shape} {s₁ s₂ : Spec.Shape} : Idx Γ s₁ → TorchLean.Tensor α s₁ → Idx Γ s₂ → TorchLean.Tensor α s₂ → TorchLean.TensorPack α Γ

Set two indices; if they coincide, add the contributions at that position.

def Proofs.RuntimeApprox.EList.zeros {ss : List Spec.Shape} : EList ss

An EList filled with zeros, used for sparse error-bound contexts.

def Proofs.RuntimeApprox.EList.setIdx {Γ : List Spec.Shape} {s : Spec.Shape} : Idx Γ s → ℝ → EList Γ

Set a single Idx position in an EList, filling all other entries with zeros.

def Proofs.RuntimeApprox.EList.set2Idx {Γ : List Spec.Shape} {s₁ s₂ : Spec.Shape} : Idx Γ s₁ → ℝ → Idx Γ s₂ → ℝ → ℝ → EList Γ

Set two indices in an EList; if they coincide, use the supplied combined value eBoth.

def Proofs.RuntimeApprox.SparseContext.set3IdxNe {α : Type} [TorchLean.Storage α] [Zero α] [Add α] {Γ : List Spec.Shape} {s₁ s₂ s₃ : Spec.Shape} (a : Idx Γ s₁) : TorchLean.Tensor α s₁ → (b : Idx Γ s₂) → TorchLean.Tensor α s₂ → (c : Idx Γ s₃) → TorchLean.Tensor α s₃ → a.i ≠ b.i → a.i ≠ c.i → b.i ≠ c.i → TorchLean.TensorPack α Γ

Set three indices when the positions are pairwise distinct.

This avoids any context-wise addition: only the three targeted positions are written, and all others are 0. This is important for NF, where even x + 0 would incur rounding.

def Proofs.RuntimeApprox.EList.set3IdxNe {Γ : List Spec.Shape} {s₁ s₂ s₃ : Spec.Shape} (a : Idx Γ s₁) : ℝ → (b : Idx Γ s₂) → ℝ → (c : Idx Γ s₃) → ℝ → a.i ≠ b.i → a.i ≠ c.i → b.i ≠ c.i → EList Γ

Error list matching SparseContext.set3IdxNe: set three positions and use 0 elsewhere.