Vathek training frame: tile partitions, accumulator, tiled gradient

Definition

VathekFrame

by ajax · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

formal-verificationmachine-learning

The core vocabulary of the tiled-graft training frame. Parameter space is $W = \mathbb{R}^d$ (as EuclideanSpace ℝ (Fin d)) and shared-state space is $V = \mathbb{R}^m$ . A valid tile partition of a finite occurrence set $I$ is a finite list of pairwise-disjoint tiles whose union is exactly $I$ ; tiles may be empty or uneven. The streaming accumulator carries three slots — the running weighted loss, the running direct parameter-gradient contribution $A$ (directAccum), and the running shared-state cotangent contribution $C$ (sharedAccum) — updated by an executable left-to-right fold in which every tile reads the same fixed pre-update data. The monolithic objective is $L_\xi(w) = \sum_{i \in I} \alpha_i \, f_i(w, h(w))$ . The tiled gradient is $g_{\mathrm{tile}} = A + Dh(w_0)^{\top} C$ : accumulated direct contributions plus one reverse pass of the shared derivative applied to the summed cotangent. Radius- $c$ global clipping $C_c$ is a total function with both branches specified (the zero gradient is fixed). The trainable projection $P_T$ zeroes every frozen coordinate. The logical step applies the deterministic optimizer exactly once to the masked, clipped gradient.

Definition code

import Mathlib.Tactic
import Mathlib.Analysis.InnerProductSpace.Adjoint
import Mathlib.Analysis.Calculus.Gradient.Basic
import Mathlib.Data.List.Basic

/-!
# VathekProof — the tiled-graft training frame (white paper §4)

Shared vocabulary for the mission "Vathek I: Tiled graft training preserves the
mathematical update".  Parameter space is `W = EuclideanSpace ℝ (Fin d)` (the `d`
logical parameter coordinates, §4.1) and shared-state space is
`V = EuclideanSpace ℝ (Fin m)`.
-/

namespace VathekProof

/-- §4.4: a *valid tile partition* of a finite occurrence set `I` is a finite list of
pairwise-disjoint tiles whose union is exactly `I`.  Tiles may be empty or uneven; an
empty tile can be removed without changing the semantics. -/
def IsTilePartition {ι : Type*} [DecidableEq ι] (I : Finset ι) (ℬ : List (Finset ι)) : Prop :=
  ℬ.foldr (· ∪ ·) ∅ = I ∧ ℬ.Pairwise (fun B₁ B₂ => Disjoint B₁ B₂)

/-- §4.4: streaming accumulator state — the running weighted loss, the running direct
parameter-gradient contribution (`directAccum`), and the running shared-state cotangent
contribution (`sharedAccum`). -/
structure TileAccum (W V : Type*) where
  /-- running weighted loss over the occurrences visited so far -/
  loss : ℝ
  /-- running direct parameter-gradient contribution -/
  direct : W
  /-- running shared-state cotangent contribution -/
  shared : V

/-- §4.4: one step of the streaming accumulator over tile `B`.  Everything is read at
the fixed pre-update data (`val`, `a`, `c`); no parameter is updated between tiles. -/
def tileAccumStep {ι W V : Type*} [AddCommMonoid W] [AddCommMonoid V] [Module ℝ W] [Module ℝ V]
    (α : ι → ℝ) (val : ι → ℝ) (a : ι → W) (c : ι → V)
    (B : Finset ι) (acc : TileAccum W V) : TileAccum W V where
  loss := acc.loss + ∑ i ∈ B, α i * val i
  direct := acc.direct + ∑ i ∈ B, α i • a i
  shared := acc.shared + ∑ i ∈ B, α i • c i

/-- §4.4: the streaming fold itself, processing tiles left to right from an initial
empty accumulator. -/
def tileAccumFold {ι W V : Type*} [AddCommMonoid W] [AddCommMonoid V] [Module ℝ W] [Module ℝ V]
    (α : ι → ℝ) (val : ι → ℝ) (a : ι → W) (c : ι → V) :
    List (Finset ι) → TileAccum W V → TileAccum W V
  | [], acc => acc
  | B :: ℬ, acc => tileAccumFold α val a c ℬ (tileAccumStep α val a c B acc)

/-- §4.4: the tiled evaluator's accumulator after processing all tiles. -/
def tileAccum {ι W V : Type*} [AddCommMonoid W] [AddCommMonoid V] [Module ℝ W] [Module ℝ V]
    (α : ι → ℝ) (val : ι → ℝ) (a : ι → W) (c : ι → V) (ℬ : List (Finset ι)) : TileAccum W V :=
  tileAccumFold α val a c ℬ ⟨0, 0, 0⟩

/-- §4.3 (1): the monolithic logical objective
`L_ξ(w) = ∑_{i ∈ I} αᵢ · fᵢ(w, h(w))`. -/
noncomputable def frameLoss {ι : Type*} {W V : Type*} (h : W → V) (f : ι → W × V → ℝ)
    (α : ι → ℝ) (I : Finset ι) (w : W) : ℝ :=
  ∑ i ∈ I, α i * f i (w, h w)

/-- §4.4 (3): the tiled gradient — the accumulated direct contributions `A`, plus one
reverse pass of the shared derivative applied to the summed shared cotangent `C`:
`g_tile = A + Dh(w₀)ᵀ C`. -/
noncomputable def tiledGrad {ι : Type*} {d m : ℕ} (α : ι → ℝ) (val : ι → ℝ)
    (a : ι → EuclideanSpace ℝ (Fin d)) (c : ι → EuclideanSpace ℝ (Fin m))
    (Dh : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin m))
    (ℬ : List (Finset ι)) : EuclideanSpace ℝ (Fin d) :=
  (tileAccum α val a c ℬ).direct + Dh.adjoint (tileAccum α val a c ℬ).shared

/-- §4.5: radius-`c` clipping of the whole (already masked) logical gradient.  Both
branches are total: at the zero gradient the clip fixes `0`. -/
noncomputable def clipVec {W : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
    (c : ℝ) (g : W) : W :=
  if ‖g‖ ≤ c then g else (c / ‖g‖) • g

/-- §4.1: `P_T` — the coordinate projection that zeroes every frozen coordinate
(`j ∉ T`) and keeps every trainable coordinate (`j ∈ T`). -/
def coordMask {d : ℕ} (T : Finset (Fin d)) (w : EuclideanSpace ℝ (Fin d)) :
    EuclideanSpace ℝ (Fin d) :=
  WithLp.toLp 2 (fun j => if j ∈ T then w j else 0)

/-- §4.5 (4): one logical optimizer application — project the accumulated gradient
onto trainable coordinates, clip globally, and apply the (deterministic) optimizer
exactly once. -/
noncomputable def logicalStep {d : ℕ} {σ : Type*} (T : Finset (Fin d)) (c : ℝ)
    (U : σ → EuclideanSpace ℝ (Fin d) → σ) (S : σ)
    (g : EuclideanSpace ℝ (Fin d)) : σ :=
  U S (clipVec c (coordMask T g))

end VathekProof

Source

Vathek Graft: A Proof and Evidence Programme, mission-source white paper v1.0, 22 September 2026 (Thomas Davis). Sections 4.1-4.5.

Read-back

What the Lean code literally says, in plain math · glm-5.3 (independent auditor subagent)

{"text": "{\n "readback": "IsTilePartition. For any type $\\\\iota$ equipped with decidable equality (the instance used to form finite-set unions), any finite set $I \\\\subseteq \\\\iota$ , and any finite list of finite sets $\\\\mathcal{B} = (B_1, B_2, \\\\ldots, B_k)$ of subsets of $\\\\iota$ , $\\\\mathrm{IsTilePartition}(I, \\\\mathcal{B})$ is the proposition asserting two things simultaneously:\n\n

B_1 \\\\cup B_2 \\\\cup \\\\cdots \\\\cup B_k = I \\\\qquad\\\\text{and}\\\\qquad B_p \\\\cap B_q = \\\\varnothing \\\\ \\\\text{for entries at distinct positions } p \\\\neq q.

\n\nThe union is the iterated binary union of the list, taken in order and starting from $\\\\varnothing$ , so an empty list gives $\\\\varnothing$ ; hence the empty list is a valid partition exactly when $I = \\\\varnothing$ . Disjointness is required pairwise between entries at distinct positions of the list; consequently, a tile occurring twice in the list must be disjoint from itself, which forces it to be empty \u2014 a repeated nonempty tile violates the predicate, while repeated empty tiles are allowed. Tiles may be empty and may be of arbitrary, unequal sizes; the union is required to equal $I$ exactly, not merely to cover it or be contained in it.\n\nTileAccum. For two arbitrary types $W$ and $V$ , with no algebraic structure assumed, $\\\\mathrm{TileAccum}(W, V)$ is the type of ordered triples $(L, A, C)$ whose first component $L$ is a real number (field loss), whose second component $A$ is an element of $W$ (field direct), and whose third component $C$ is an element of $V$ (field shared). It is pure data: the declaration provides the three projection maps selecting $L$ , $A$ , and $C$ , and nothing more.\n\ntileAccumStep. For any types $\\\\iota, W, V$ such that $W$ and $V$ are commutative additive monoids carrying the structure of real vector spaces (so each has a zero, an associative commutative addition, and a scalar multiplication by reals), given weight and value functions $\\\\alpha, \\\\mathrm{val} : \\\\iota \\\\to \\\\mathbb{R}$ , families $a : \\\\iota \\\\to W$ and $c : \\\\iota \\\\to V$ , a finite set $B \\\\subseteq \\\\iota$ , and an accumulator $(L, A, C) \\\\in \\\\mathrm{TileAccum}(W, V)$ , one step returns the new accumulator with components\n\n

L' = L + \\\\sum_{i \\\\in B} \\\\alpha_i \\\\, \\\\mathrm{val}(i), \\\\qquad A' = A + \\\\sum_{i \\\\in B} \\\\alpha_i \\\\cdot a_i, \\\\qquad C' = C + \\\\sum_{i \\\\in B} \\\\alpha_i \\\\cdot c_i,

\n\nwhere $\\\\alpha_i \\\\cdot a_i$ denotes the scalar action of $\\\\mathbb{R}$ on $W$ (similarly on $V$ ). Each component is the old one plus the $B$ -sum of $\\\\alpha$ -weighted contributions; the sums range over the finite set $B$ , so each index is counted once, and $B = \\\\varnothing$ makes the step the identity on the accumulator. The step is a total function: no hypothesis is imposed on $B$ , and the weights $\\\\alpha_i$ are arbitrary reals (possibly negative or larger than $1$ ). All four data functions are read at their given arguments; the step computes and returns a new record and modifies nothing.\n\ntileAccumFold. With the same type assumptions and the same arguments $\\\\alpha, \\\\mathrm{val}, a, c$ as the step, this is a total function of a list of tiles $\\\\mathcal{B} = (B_1, \\\\ldots, B_k)$ and an accumulator, defined by structural recursion on the list: on the empty list it returns the accumulator unchanged; on $B_1 :: (B_2, \\\\ldots, B_k)$ it applies one step at $B_1$ and recurses on the remaining list with the updated accumulator. Tiles are thus processed in list order, first to last, threading the accumulator through. The recursion is structural, so the function is defined for every list of finite sets: tiles may repeat or overlap, and the list need not satisfy any partition property.\n\ntileAccum. The accumulator after processing all tiles: the fold above applied to $\\\\mathcal{B} = (B_1, \\\\ldots, B_k)$ with the initial accumulator $(0, 0, 0)$ , the zeros being those of $\\\\mathbb{R}$ , $W$ , and $V$ . Unfolding the recursion, the three components are\n\n

L = \\\\sum_{p=1}^{k} \\\\sum_{i \\\\in B_p} \\\\alpha_i \\\\, \\\\mathrm{val}(i), \\\\qquad A = \\\\sum_{p=1}^{k} \\\\sum_{i \\\\in B_p} \\\\alpha_i \\\\cdot a_i, \\\\qquad C = \\\\sum_{p=1}^{k} \\\\sum_{i \\\\in B_p} \\\\alpha_i \\\\cdot c_i,

\n\nthe outer sums running over the positions of the list: an index $i$ belonging to several tiles, or a tile repeated in the list, contributes once per occurrence. For the empty list the result is $(0, 0, 0)$ . Because all additions involved are commutative, this final value does not depend on the order of the list, although the intermediate accumulator states do.\n\nframeLoss. For a type $\\\\iota$ and arbitrary types $W, V$ carrying no structure whatsoever, given an arbitrary map $h : W \\\\to V$ , a family $f : \\\\iota \\\\to (W \\\\times V \\\\to \\\\mathbb{R})$ , weights $\\\\alpha : \\\\iota \\\\to \\\\mathbb{R}$ , a finite set $I \\\\subseteq \\\\iota$ , and a point $w \\\\in W$ , this defines the real number\n\n

L(w) = \\\\sum_{i \\\\in I} \\\\alpha_i \\\\cdot f_i\\\\big(w,\\\\, h(w)\\\\big).

\n\nEach summand evaluates $f_i$ at the pair whose first component is $w$ itself and whose second component is $h(w)$ ; the shared value $h(w)$ is the same in every term of the sum. No assumption is placed on $h$ or on the $f_i$ (in particular no continuity or differentiability), none on the weights (arbitrary reals, possibly negative), and $I$ may be empty, in which case $L(w) = 0$ .\n\ntiledGrad. For a type $\\\\iota$ and natural numbers $d, m$ : given $\\\\alpha, \\\\mathrm{val} : \\\\iota \\\\to \\\\mathbb{R}$ , families $a : \\\\iota \\\\to \\\\mathbb{R}^d$ and $c : \\\\iota \\\\to \\\\mathbb{R}^m$ (Euclidean spaces of $d$ - and $m$ -tuples with the standard inner product), a continuous $\\\\mathbb{R}$ -linear map $Dh : \\\\mathbb{R}^d \\\\to \\\\mathbb{R}^m$ , and a list of finite sets $\\\\mathcal{B}$ , this defines the vector in $\\\\mathbb{R}^d$ \n\n

g_{\\\\mathrm{tile}} = A + Dh^{\\\\ast}(C),

\n\nwhere $(L, A, C) = \\\\mathrm{tileAccum}(\\\\alpha, \\\\mathrm{val}, a, c, \\\\mathcal{B})$ is the accumulator expanded above, and $Dh^{\\\\ast} : \\\\mathbb{R}^m \\\\to \\\\mathbb{R}^d$ is the adjoint of $Dh$ with respect to the standard inner products, i.e. the unique continuous linear map satisfying $\\\\langle Dh\\\\, x,\\\\, y \\\\rangle = \\\\langle x,\\\\, Dh^{\\\\ast} y \\\\rangle$ for all $x \\\\in \\\\mathbb{R}^d$ , $y \\\\in \\\\mathbb{R}^m$ (over the reals, the transpose). Only the components $A$ and $C$ of the accumulator enter the value: the loss component $L$ \u2014 and hence the entire argument $\\\\mathrm{val}$ \u2014 has no influence on the result. Furthermore, no hypothesis connects $\\\\mathcal{B}$ to a partition of any set: it is an arbitrary list, and indices occurring in several tiles are counted with multiplicity.\n\nclipVec. For a real number $c$ and a vector $g$ in a real normed space $W$ (a normed abelian group with a compatible scalar multiplication by $\\\\mathbb{R}$ ; in particular $\\\\|g\\\\| = 0$ exactly when $g = 0$ ), the clipped vector is defined by an if-then-else on the inclusive norm test $\\\\|g\\\\| \\\\le c$ :\n\n

\\\\mathrm{clip}_c(g) = \\\\begin{cases} g, & \\\\text{if } \\\\|g\\\\| \\\\le c, \\\\\\\\[4pt] \\\\dfrac{c}{\\\\|g\\\\|}\\\\, g, & \\\\text{if } \\\\|g\\\\| > c. \\\\end{cases}

\n\nThe function is total for every $c \\\\in \\\\mathbb{R}$ , and real division is total with the convention $x / 0 = 0$ . Consequences of the literal clauses: if $g \\\\neq 0$ and $0 \\\\le c < \\\\|g\\\\|$ , the result is $g$ rescaled by the positive factor $c/\\\\|g\\\\|$ , i.e. a vector of norm exactly $c$ pointing along $g$ (and $c = 0$ yields the zero vector); if $g \\\\neq 0$ and $c < 0$ , the test $\\\\|g\\\\| \\\\le c$ necessarily fails and the else-branch multiplies $g$ by the negative scalar $c/\\\\|g\\\\|$ , producing a vector of norm $|c|$ pointing opposite to $g$ ; if $g = 0$ , both branches return the zero vector \u2014 for $c \\\\ge 0$ via the then-branch, and for $c < 0$ via the else-branch, where $\\\\tfrac{c}{\\\\|g\\\\|} g = \\\\tfrac{c}{0} \\\\cdot 0 = 0 \\\\cdot 0 = 0$ under the stated division convention.\n\ncoordMask. For a natural number $d$ , a finite set $T$ of coordinates ( $T \\\\subseteq \\\\{0, \\\\ldots, d-1\\\\}$ , the index type of length $d$ ), and a vector $w \\\\in \\\\mathbb{R}^d$ , this is the coordinatewise mask $P_T$ defined by\n\n

(P_T\\\\, w)_j = \\\\begin{cases} w_j, & j \\\\in T, \\\\\\\\ 0, & j \\\\notin T, \\\\end{cases} \\\\qquad j = 0, \\\\ldots, d-1,

\n\ni.e. coordinates in $T$ are kept and all others are set to zero. (The code re-packages the coordinate function into the Euclidean-space type; on underlying coordinates this packaging is the identity, so the map is exactly the mask above.) The map is linear in $w$ ; if $T = \\\\varnothing$ it is the zero map, and if $T$ is the full set of all $d$ coordinates it is the identity.\n\nlogicalStep. For a natural number $d$ and an arbitrary type $\\\\sigma$ carrying no structure, given a finite set $T$ of coordinates, a real number $c$ , an arbitrary function $U : \\\\sigma \\\\to \\\\mathbb{R}^d \\\\to \\\\sigma$ , a state $S \\\\in \\\\sigma$ , and a direction $g \\\\in \\\\mathbb{R}^d$ , one logical step returns the state\n\n

U\\\\big(S,\\\\; \\\\mathrm{clip}_c(P_T\\\\, g)\\\\big),

\n\nthat is: the direction $g$ is first masked to the coordinates in $T$ by $P_T$ ; the masked vector is then clipped by $\\\\mathrm{clip}_c$ , so the radius test applies to $\\\\|P_T\\\\, g\\\\|$ \u2014 the norm of the already-masked vector, not of $g$ ; and finally $U$ is applied exactly once to the pair consisting of the starting state $S$ and the resulting clipped vector. No property whatsoever is assumed of $U$ : it is an arbitrary function of a state and a direction returning a state. Besides the clipping scalar $c/\\\\|{\\\\cdot}\\\\|$ above, no further scaling, normalization, or correction factor appears anywhere in the step, and $U$ is applied a single time, not iterated. The radius $c$ is an arbitrary real, so the negative-radius and zero-vector behavior of $\\\\mathrm{clip}_c$ described above carries over verbatim."\n}", "details": {"resolvedPath": "/home/ajax/.omp/agent/sessions/-math/2026-09-22T19-31-08-510Z_01a0ca99-be5e-7000-93c6-dac7c74cc004/RB-VathekFrame.md", "contentType": "text/markdown", "totalLines": 3, "displayContent": {"text": "{\n "readback": "IsTilePartition. For any type $\\\\iota$ equipped with decidable equality (the instance used to form finite-set unions), any finite set $I \\\\subseteq \\\\iota$ , and any finite list of finite sets $\\\\mathcal{B} = (B_1, B_2, \\\\ldots, B_k)$ of subsets of $\\\\iota$ , $\\\\mathrm{IsTilePartition}(I, \\\\mathcal{B})$ is the proposition asserting two things simultaneously:\n\n

B_1 \\\\cup B_2 \\\\cup \\\\cdots \\\\cup B_k = I \\\\qquad\\\\text{and}\\\\qquad B_p \\\\cap B_q = \\\\varnothing \\\\ \\\\text{for entries at distinct positions } p \\\\neq q.

L' = L + \\\\sum_{i \\\\in B} \\\\alpha_i \\\\, \\\\mathrm{val}(i), \\\\qquad A' = A + \\\\sum_{i \\\\in B} \\\\alpha_i \\\\cdot a_i, \\\\qquad C' = C + \\\\sum_{i \\\\in B} \\\\alpha_i \\\\cdot c_i,

L = \\\\sum_{p=1}^{k} \\\\sum_{i \\\\in B_p} \\\\alpha_i \\\\, \\\\mathrm{val}(i), \\\\qquad A = \\\\sum_{p=1}^{k} \\\\sum_{i \\\\in B_p} \\\\alpha_i \\\\cdot a_i, \\\\qquad C = \\\\sum_{p=1}^{k} \\\\sum_{i \\\\in B_p} \\\\alpha_i \\\\cdot c_i,

L(w) = \\\\sum_{i \\\\in I} \\\\alpha_i \\\\cdot f_i\\\\big(w,\\\\, h(w)\\\\big).

g_{\\\\mathrm{tile}} = A + Dh^{\\\\ast}(C),

\\\\mathrm{clip}_c(g) = \\\\begin{cases} g, & \\\\text{if } \\\\|g\\\\| \\\\le c, \\\\\\\\[4pt] \\\\dfrac{c}{\\\\|g\\\\|}\\\\, g, & \\\\text{if } \\\\|g\\\\| > c. \\\\end{cases}

(P_T\\\\, w)_j = \\\\begin{cases} w_j, & j \\\\in T, \\\\\\\\ 0, & j \\\\notin T, \\\\end{cases} \\\\qquad j = 0, \\\\ldots, d-1,

U\\\\big(S,\\\\; \\\\mathrm{clip}_c(P_T\\\\, g)\\\\big),

Human review

Endorsed by Shuze Chen · Sep 25, 2026
Endorsed by ajax · Sep 25, 2026
Confirmed by the mission captain (proposal self-audit).

View graph