Vathek training frame, derivative certificates, state, and runs

{'text': '{\n "type": "result",\n "data": "Throughout, $\\\\mathbb{R}^d$ denotes $d$-dimensional real coordinate space with the standard Euclidean inner product $\\\\langle\\\\cdot,\\\\cdot\\\\rangle$ and norm $\\\\lVert\\\\cdot\\\\rVert$; a vector $x \\\\in \\\\mathbb{R}^d$ is viewed as its coordinate function $j \\\\mapsto x_j$ on $j \\\\in \\\\{0,\\\\dots,d-1\\\\}$. A derivative is always a Fréchet derivative: $L$ is the derivative of $h$ at $x$ means $h(x+u) = h(x) + L(u) + o(\\\\lVert u\\\\rVert)$ with $L$ a continuous linear map. For real-valued $\\\\varphi : \\\\mathbb{R}^d \\\\to \\\\mathbb{R}$, \"$g \\\\in \\\\mathbb{R}^d$ is the gradient of $\\\\varphi$ at $x$\" means $\\\\varphi(x+u) = \\\\varphi(x) + \\\\langle g, u\\\\rangle + o(\\\\lVert u\\\\rVert)$.\n\n**Frame.** For arbitrary natural numbers $d, m$ and an arbitrary type $\\\\iota$ (a type of occurrence labels; no assumption of any kind is placed on $\\\\iota$), a frame is a record with four data fields:\n\n- a map $h : \\\\mathbb{R}^d \\\\to \\\\mathbb{R}^m$;\n- an $\\\\iota$-indexed family of loss maps $f_i : \\\\mathbb{R}^d \\\\times \\\\mathbb{R}^m \\\\to \\\\mathbb{R}$, one for each $i \\\\in \\\\iota$;\n- an $\\\\iota$-indexed family of real coefficients $\\\\alpha_i \\\\in \\\\mathbb{R}$ — no sign or other condition is imposed (negative and zero coefficients are permitted);\n- a finite occurrence set $I \\\\subseteq \\\\iota$.\n\nNo regularity (continuity, differentiability) is required of $h$ or of any $f_i$. The quantification silently includes the degenerate cases $d = 0$ or $m = 0$ (the corresponding space is a single point), $I = \\\\emptyset$, and $\\\\iota$ infinite (only $I$ is required finite).\n\n**FrameDeriv.** For arbitrary $d, m \\\\in \\\\mathbb{N}$, an arbitrary type $\\\\iota$, a frame $\\\\xi = (h, f, \\\\alpha, I)$ as above, and a point $w_0 \\\\in \\\\mathbb{R}^d$, a frame-derivative certificate at $w_0$ is a record with the following data fields and proof fields (all must be supplied to give an element):\n\n- data: a continuous linear map h\' : \\\\mathbb{R}^d \\\\to \\\\mathbb{R}^m;\n- certificate hh (unconditional): h\' is the derivative of $h$ at $w_0$;\n- data: a function $\\\\mathrm{val} : \\\\iota \\\\to \\\\mathbb{R}$;\n- certificate hval: for every $i \\\\in I$, $\\\\mathrm{val}(i) = f_i\\\\big(w_0,\\\\, h(w_0)\\\\big)$;\n- data: a function $\\\\mathrm{direct} : \\\\iota \\\\to \\\\mathbb{R}^d$;\n- data: a function $\\\\mathrm{shared} : \\\\iota \\\\to \\\\mathbb{R}^m$;\n- certificate hdirect: for every $i \\\\in I$, $\\\\mathrm{direct}(i)$ is the gradient at $w_0$ of the partially applied map $w \\\\mapsto f_i\\\\big(w,\\\\, h(w_0)\\\\big)$ (second argument frozen at the pre-update shared state $h(w_0)$);\n- certificate hshared: for every $i \\\\in I$, $\\\\mathrm{shared}(i)$ is the gradient at $h(w_0)$ of the map $v \\\\mapsto f_i(w_0, v)$ (first argument frozen at $w_0$);\n- certificate hdiff: for every $i \\\\in I$, $f_i$ is differentiable (as a map on the product $\\\\mathbb{R}^d \\\\times \\\\mathbb{R}^m$) at the single point $\\\\big(w_0, h(w_0)\\\\big)$.\n\nAll certificates except hh quantify only over $i \\\\in I$: outside $I$ the functions $\\\\mathrm{val}$, $\\\\mathrm{direct}$, $\\\\mathrm{shared}$ are unconstrained arbitrary data. If $I = \\\\emptyset$ these four conditions are vacuous, and the only substantive requirement is that $h$ be differentiable at $w_0$ (so the existence of such a record always forces differentiability of $h$ at $w_0$, but forces nothing about the $f_i$ when $I = \\\\emptyset$).\n\n**TrainState.** For every $d \\\\in \\\\mathbb{N}$, a training state is a record of four data fields: three vectors $w, \\\\mathrm{mom1}, \\\\mathrm{mom2} \\\\in \\\\mathbb{R}^d$ and a step counter $t \\\\in \\\\mathbb{N}$. No conditions are imposed on any field.\n\n**TrainSnap.** For every $d \\\\in \\\\mathbb{N}$, a training snapshot is a record of four data fields: three lists of reals $w, \\\\mathrm{mom1}, \\\\mathrm{mom2}$ and a step counter $t \\\\in \\\\mathbb{N}$. The lengths of the lists are in no way tied to $d$; snapshots with empty, short, or long lists are all legitimate elements.\n\n**listOfVec.** For every $d$ (implicit) and every $x \\\\in \\\\mathbb{R}^d$, this is the list of reals of length exactly $d$ whose $j$-th entry is the coordinate $x_j$, for $j = 0, \\\\dots, d-1$. For $d = 0$ it is the empty list.\n\n**vecOfList.** For every $d$ (implicit) and every list $l$ of reals, this is the vector in $\\\\mathbb{R}^d$ whose $j$-th coordinate is the $j$-th entry of $l$ if the list has an entry at position $j$, and $0$ otherwise. The function is total: a list shorter than $d$ is padded with zeros in the missing coordinates, and entries at positions $\\\\ge d$ are ignored.\n\n**snap.** For every $d$ (implicit), this maps a training state $S$ to its snapshot: each of the three vectors $S.w, S.\\\\mathrm{mom1}, S.\\\\mathrm{mom2}$ is encoded by listOfVec (so each list has length exactly $d$), and the counter $S.t$ is copied unchanged.\n\n**restore.** For every $d$ (implicit), this maps a snapshot $P$ back to a training state: each of the three lists is decoded by vecOfList (with the zero-padding / entry-ignoring behavior above when a list's length differs from $d$), and $P.t$ is copied unchanged.\n\n**monoGrad.** For all $d, m \\\\in \\\\mathbb{N}$, all types $\\\\iota$ (implicit), every frame $\\\\xi = (h, f, \\\\alpha, I)$, and every $w_0 \\\\in \\\\mathbb{R}^d$, this defines a vector in $\\\\mathbb{R}^d$. Write the monolithic objective\n

L_\\\\xi(w) \\\\;=\\\\; \\\\sum_{i \\\\in I} \\\\alpha_i \\\\, f_i\\\\big(w, h(w)\\\\big).

\nThen $\\\\mathrm{monoGrad}(\\\\xi, w_0)$ is obtained by taking the Fréchet derivative of L_\\\\xi at $w_0$ — read through the total derivative operator, which returns the zero map at any point where L_\\\\xi fails to be differentiable — and applying its adjoint (Riesz representation) to the scalar $1$. Equivalently, \\\\mathrm{monoGrad}(\\\\xi, w_0) = \\\\big(DL_\\\\xi(w_0)\\\\big)^{T} \\\\cdot 1: it is the gradient \\\\nabla L_\\\\xi(w_0) wherever L_\\\\xi is differentiable at $w_0$, and the zero vector at every point where it is not. The definition itself assumes no differentiability; it is total for every frame, including frames with non-differentiable $h$ or $f_i$.\n\n**tiledRun.** For all $d, m \\\\in \\\\mathbb{N}$ and every type $\\\\iota$ carrying decidable equality, given\n\n- a frame schedule $\\\\xi = (\\\\xi_k)_{k \\\\in \\\\mathbb{N}}$, one frame $\\\\xi_k = (h_k, f_k, \\\\alpha_k, I_k)$ per logical step $k$;\n- a tiling schedule $\\\\mathfrak{B} = (\\\\mathfrak{B}_k)_{k \\\\in \\\\mathbb{N}}$, each $\\\\mathfrak{B}_k$ a finite list of finite subsets (\"tiles\") of $\\\\iota$;\n- a certificate oracle assigning to every step $k$ and every training state $S$ a full frame-derivative certificate for the frame $\\\\xi_k$ at the point $S.w$;\n- a finite set $T \\\\subseteq \\\\{0,\\\\dots,d-1\\\\}$ of trainable coordinates;\n- a real clipping radius $c$;\n- an optimizer map $U$ from states and vectors to states,\n\nthis defines a one-step transition on (state, step index): the state $S$ at logical step $k$ is sent to $U\\\\big(S,\\\\; \\\\mathrm{clip}_c\\\\,(P_T\\\\, g)\\\\big)$, where the gradient $g \\\\in \\\\mathbb{R}^d$ is computed as follows. Unfolding the tiled gradient: with \\\\mathrm{val}, \\\\mathrm{direct}, \\\\mathrm{shared}, h\' the data fields of the certificate at $(k, S)$, an accumulator $(A, C) \\\\in \\\\mathbb{R}^d \\\\times \\\\mathbb{R}^m$ is built by traversing the tile list $\\\\mathfrak{B}_k$ from left to right starting from $(0,0)$, each tile $B$ adding\n

$$A \\\\;\\\\mathrel{+}=\\\\; \\\\sum_{i \\\\in B} \\\\alpha^{(k)}_i \\\\,\\\\mathrm{direct}(i), \\\\qquad C \\\\;\\\\mathrel{+}=\\\\; \\\\sum_{i \\\\in B} \\\\alpha^{(k)}_i \\\\,\\\\mathrm{shared}(i)$$

\n(the same fold also maintains a running scalar loss $\\\\sum_{i\\\\in B}\\\\alpha^{(k)}_i\\\\,\\\\mathrm{val}(i)$ per tile, which the gradient does not read), and then\n

$$g \\\\;=\\\\; A \\\\;+\\\\; (h\')^{T} C,$$

\n$(h\')^{T}$ denoting the adjoint of the shared-derivative certificate h\'. Next, $P_T$ is the coordinate projection keeping $g_j$ for $j \\\\in T$ and zeroing $g_j$ for $j \\\\notin T$; finally $\\\\mathrm{clip}_c$ is\n

\\\\mathrm{clip}_c(g) = \\\\begin{cases} g, & \\\\lVert g\\\\rVert \\\\le c,\\\\\\\\[2pt] \\\\dfrac{c}{\\\\lVert g\\\\rVert}\\\\, g, & \\\\lVert g\\\\rVert > c.\\\\end{cases}

\nThe optimizer $U$ is applied exactly once, to the pre-update state $S$ and the processed gradient; a single certificate, at the point $S.w$, supplies every tile's data. The definition imposes no relation between the tile lists $\\\\mathfrak{B}_k$ and the frame's occurrence set $I_k$: tiles may be empty, overlap, repeat (a repeated tile contributes twice), or contain indices outside $I_k$, and the certificate data are only certified on $I_k$ while the sums run over the tiles as given; an empty tile list yields $g = 0$. The clipping is total for every real $c$ (real division satisfies $x/0 = 0$); note $c = 0$ sends every $g$ to $0$, and negative $c$ makes the branch condition fail for every $g$, producing $(c/\\\\lVert g\\\\rVert)\\\\,g$ — a vector of norm $|c|$ pointing opposite to $g$ (and $0$ when $g = 0$). Note also that supplying the certificate oracle at all states $S$ entails, through the unconditional hh field, differentiability of each $h_k$ at every parameter vector $w \\\\in \\\\mathbb{R}^d$.\n\n**monoRun.** For all $d, m \\\\in \\\\mathbb{N}$ and every type $\\\\iota$ (no decidable-equality assumption here), given a frame schedule $\\\\xi = (\\\\xi_k)_k$, a finite trainable-coordinate set $T \\\\subseteq \\\\{0,\\\\dots,d-1\\\\}$, a real clipping radius $c$, and an optimizer $U$, this defines the one-step transition sending the state $S$ at logical step $k$ to\n

$$U\\\\Big(S,\\\\; \\\\mathrm{clip}_c\\\\big(P_T\\\\,(\\\\mathrm{monoGrad}(\\\\xi_k, S.w))\\\\big)\\\\Big),$$

\nthat is: the monolithic gradient of $L_{\\\\xi_k}$ at the current parameters $S.w$ (zero by convention wherever $L_{\\\\xi_k}$ is not differentiable there), followed by the same coordinate projection $P_T$ and the same clipping $\\\\mathrm{clip}_c$ as in tiledRun, then a single application of $U$. No certificates, tiles, or differentiability hypotheses are involved; the definition is total for every schedule.\n\n**runFrom.** For an arbitrary type $\\\\sigma$ (implicit) and an arbitrary step function $\\\\mathrm{step} : \\\\sigma \\\\to \\\\mathbb{N} \\\\to \\\\sigma$ (a map taking a state and a natural step index to a new state), this defines a function $\\\\mathbb{N} \\\\to \\\\sigma \\\\to \\\\sigma$ by recursion on the number of steps:\n\n- $\\\\mathrm{runFrom}\\\\; \\\\mathrm{step}\\\\; 0\\\\; S = S$;\n- $\\\\mathrm{runFrom}\\\\; \\\\mathrm{step}\\\\; (n+1)\\\\; S = \\\\mathrm{runFrom}\\\\; \\\\mathrm{step}\\\\; n\\\\; \\\\big(\\\\mathrm{step}\\\\; S\\\\; n\\\\big)$.\n\nThus $\\\\mathrm{runFrom}\\\\; \\\\mathrm{step}\\\\; n\\\\; S$ applies $\\\\mathrm{step}$ exactly $n$ times, the applications receiving the step indices $n-1, n-2, \\\\dots, 1, 0$ in that order:\n

$$\\\\mathrm{runFrom}\\\\; \\\\mathrm{step}\\\\; n\\\\; S \\\\;=\\\\; \\\\mathrm{step}\\\\big(\\\\dots \\\\mathrm{step}\\\\big(\\\\mathrm{step}(S,\\\\, n-1),\\\\, n-2\\\\big) \\\\dots,\\\\, 0\\\\big).$$

\nAt $n = 0$ the state is returned unchanged. The definition is generic in $\\\\sigma$; it is not tied to training states, frames, or any particular step function."\n}', 'details': {'resolvedPath': '/home/ajax/.omp/agent/sessions/-math/2026-09-22T19-31-08-510Z_01a0ca99-be5e-7000-93c6-dac7c74cc004/RB2-VathekState.md', 'contentType': 'text/markdown', 'totalLines': 4, 'displayContent': {'text': '{\n "type": "result",\n "data": "Throughout, $\\\\mathbb{R}^d$ denotes $d$-dimensional real coordinate space with the standard Euclidean inner product $\\\\langle\\\\cdot,\\\\cdot\\\\rangle$ and norm $\\\\lVert\\\\cdot\\\\rVert$; a vector $x \\\\in \\\\mathbb{R}^d$ is viewed as its coordinate function $j \\\\mapsto x_j$ on $j \\\\in \\\\{0,\\\\dots,d-1\\\\}$. A derivative is always a Fréchet derivative: $L$ is the derivative of $h$ at $x$ means $h(x+u) = h(x) + L(u) + o(\\\\lVert u\\\\rVert)$ with $L$ a continuous linear map. For real-valued $\\\\varphi : \\\\mathbb{R}^d \\\\to \\\\mathbb{R}$, \"$g \\\\in \\\\mathbb{R}^d$ is the gradient of $\\\\varphi$ at $x$\" means $\\\\varphi(x+u) = \\\\varphi(x) + \\\\langle g, u\\\\rangle + o(\\\\lVert u\\\\rVert)$.\n\n**Frame.** For arbitrary natural numbers $d, m$ and an arbitrary type $\\\\iota$ (a type of occurrence labels; no assumption of any kind is placed on $\\\\iota$), a frame is a record with four data fields:\n\n- a map $h : \\\\mathbb{R}^d \\\\to \\\\mathbb{R}^m$;\n- an $\\\\iota$-indexed family of loss maps $f_i : \\\\mathbb{R}^d \\\\times \\\\mathbb{R}^m \\\\to \\\\mathbb{R}$, one for each $i \\\\in \\\\iota$;\n- an $\\\\iota$-indexed family of real coefficients $\\\\alpha_i \\\\in \\\\mathbb{R}$ — no sign or other condition is imposed (negative and zero coefficients are permitted);\n- a finite occurrence set $I \\\\subseteq \\\\iota$.\n\nNo regularity (continuity, differentiability) is required of $h$ or of any $f_i$. The quantification silently includes the degenerate cases $d = 0$ or $m = 0$ (the corresponding space is a single point), $I = \\\\emptyset$, and $\\\\iota$ infinite (only $I$ is required finite).\n\n**FrameDeriv.** For arbitrary $d, m \\\\in \\\\mathbb{N}$, an arbitrary type $\\\\iota$, a frame $\\\\xi = (h, f, \\\\alpha, I)$ as above, and a point $w_0 \\\\in \\\\mathbb{R}^d$, a frame-derivative certificate at $w_0$ is a record with the following data fields and proof fields (all must be supplied to give an element):\n\n- data: a continuous linear map h\' : \\\\mathbb{R}^d \\\\to \\\\mathbb{R}^m;\n- certificate hh (unconditional): h\' is the derivative of $h$ at $w_0$;\n- data: a function $\\\\mathrm{val} : \\\\iota \\\\to \\\\mathbb{R}$;\n- certificate hval: for every $i \\\\in I$, $\\\\mathrm{val}(i) = f_i\\\\big(w_0,\\\\, h(w_0)\\\\big)$;\n- data: a function $\\\\mathrm{direct} : \\\\iota \\\\to \\\\mathbb{R}^d$;\n- data: a function $\\\\mathrm{shared} : \\\\iota \\\\to \\\\mathbb{R}^m$;\n- certificate hdirect: for every $i \\\\in I$, $\\\\mathrm{direct}(i)$ is the gradient at $w_0$ of the partially applied map $w \\\\mapsto f_i\\\\big(w,\\\\, h(w_0)\\\\big)$ (second argument frozen at the pre-update shared state $h(w_0)$);\n- certificate hshared: for every $i \\\\in I$, $\\\\mathrm{shared}(i)$ is the gradient at $h(w_0)$ of the map $v \\\\mapsto f_i(w_0, v)$ (first argument frozen at $w_0$);\n- certificate hdiff: for every $i \\\\in I$, $f_i$ is differentiable (as a map on the product $\\\\mathbb{R}^d \\\\times \\\\mathbb{R}^m$) at the single point $\\\\big(w_0, h(w_0)\\\\big)$.\n\nAll certificates except hh quantify only over $i \\\\in I$: outside $I$ the functions $\\\\mathrm{val}$, $\\\\mathrm{direct}$, $\\\\mathrm{shared}$ are unconstrained arbitrary data. If $I = \\\\emptyset$ these four conditions are vacuous, and the only substantive requirement is that $h$ be differentiable at $w_0$ (so the existence of such a record always forces differentiability of $h$ at $w_0$, but forces nothing about the $f_i$ when $I = \\\\emptyset$).\n\n**TrainState.** For every $d \\\\in \\\\mathbb{N}$, a training state is a record of four data fields: three vectors $w, \\\\mathrm{mom1}, \\\\mathrm{mom2} \\\\in \\\\mathbb{R}^d$ and a step counter $t \\\\in \\\\mathbb{N}$. No conditions are imposed on any field.\n\n**TrainSnap.** For every $d \\\\in \\\\mathbb{N}$, a training snapshot is a record of four data fields: three lists of reals $w, \\\\mathrm{mom1}, \\\\mathrm{mom2}$ and a step counter $t \\\\in \\\\mathbb{N}$. The lengths of the lists are in no way tied to $d$; snapshots with empty, short, or long lists are all legitimate elements.\n\n**listOfVec.** For every $d$ (implicit) and every $x \\\\in \\\\mathbb{R}^d$, this is the list of reals of length exactly $d$ whose $j$-th entry is the coordinate $x_j$, for $j = 0, \\\\dots, d-1$. For $d = 0$ it is the empty list.\n\n**vecOfList.** For every $d$ (implicit) and every list $l$ of reals, this is the vector in $\\\\mathbb{R}^d$ whose $j$-th coordinate is the $j$-th entry of $l$ if the list has an entry at position $j$, and $0$ otherwise. The function is total: a list shorter than $d$ is padded with zeros in the missing coordinates, and entries at positions $\\\\ge d$ are ignored.\n\n**snap.** For every $d$ (implicit), this maps a training state $S$ to its snapshot: each of the three vectors $S.w, S.\\\\mathrm{mom1}, S.\\\\mathrm{mom2}$ is encoded by listOfVec (so each list has length exactly $d$), and the counter $S.t$ is copied unchanged.\n\n**restore.** For every $d$ (implicit), this maps a snapshot $P$ back to a training state: each of the three lists is decoded by vecOfList (with the zero-padding / entry-ignoring behavior above when a list's length differs from $d$), and $P.t$ is copied unchanged.\n\n**monoGrad.** For all $d, m \\\\in \\\\mathbb{N}$, all types $\\\\iota$ (implicit), every frame $\\\\xi = (h, f, \\\\alpha, I)$, and every $w_0 \\\\in \\\\mathbb{R}^d$, this defines a vector in $\\\\mathbb{R}^d$. Write the monolithic objective\n

L_\\\\xi(w) \\\\;=\\\\; \\\\sum_{i \\\\in I} \\\\alpha_i \\\\, f_i\\\\big(w, h(w)\\\\big).

\nThen $\\\\mathrm{monoGrad}(\\\\xi, w_0)$ is obtained by taking the Fréchet derivative of L_\\\\xi at $w_0$ — read through the total derivative operator, which returns the zero map at any point where L_\\\\xi fails to be differentiable — and applying its adjoint (Riesz representation) to the scalar $1$. Equivalently, \\\\mathrm{monoGrad}(\\\\xi, w_0) = \\\\big(DL_\\\\xi(w_0)\\\\big)^{T} \\\\cdot 1: it is the gradient \\\\nabla L_\\\\xi(w_0) wherever L_\\\\xi is differentiable at $w_0$, and the zero vector at every point where it is not. The definition itself assumes no differentiability; it is total for every frame, including frames with non-differentiable $h$ or $f_i$.\n\n**tiledRun.** For all $d, m \\\\in \\\\mathbb{N}$ and every type $\\\\iota$ carrying decidable equality, given\n\n- a frame schedule $\\\\xi = (\\\\xi_k)_{k \\\\in \\\\mathbb{N}}$, one frame $\\\\xi_k = (h_k, f_k, \\\\alpha_k, I_k)$ per logical step $k$;\n- a tiling schedule $\\\\mathfrak{B} = (\\\\mathfrak{B}_k)_{k \\\\in \\\\mathbb{N}}$, each $\\\\mathfrak{B}_k$ a finite list of finite subsets (\"tiles\") of $\\\\iota$;\n- a certificate oracle assigning to every step $k$ and every training state $S$ a full frame-derivative certificate for the frame $\\\\xi_k$ at the point $S.w$;\n- a finite set $T \\\\subseteq \\\\{0,\\\\dots,d-1\\\\}$ of trainable coordinates;\n- a real clipping radius $c$;\n- an optimizer map $U$ from states and vectors to states,\n\nthis defines a one-step transition on (state, step index): the state $S$ at logical step $k$ is sent to $U\\\\big(S,\\\\; \\\\mathrm{clip}_c\\\\,(P_T\\\\, g)\\\\big)$, where the gradient $g \\\\in \\\\mathbb{R}^d$ is computed as follows. Unfolding the tiled gradient: with \\\\mathrm{val}, \\\\mathrm{direct}, \\\\mathrm{shared}, h\' the data fields of the certificate at $(k, S)$, an accumulator $(A, C) \\\\in \\\\mathbb{R}^d \\\\times \\\\mathbb{R}^m$ is built by traversing the tile list $\\\\mathfrak{B}_k$ from left to right starting from $(0,0)$, each tile $B$ adding\n

$$A \\\\;\\\\mathrel{+}=\\\\; \\\\sum_{i \\\\in B} \\\\alpha^{(k)}_i \\\\,\\\\mathrm{direct}(i), \\\\qquad C \\\\;\\\\mathrel{+}=\\\\; \\\\sum_{i \\\\in B} \\\\alpha^{(k)}_i \\\\,\\\\mathrm{shared}(i)$$

\n(the same fold also maintains a running scalar loss $\\\\sum_{i\\\\in B}\\\\alpha^{(k)}_i\\\\,\\\\mathrm{val}(i)$ per tile, which the gradient does not read), and then\n

$$g \\\\;=\\\\; A \\\\;+\\\\; (h\')^{T} C,$$

\n$(h\')^{T}$ denoting the adjoint of the shared-derivative certificate h\'. Next, $P_T$ is the coordinate projection keeping $g_j$ for $j \\\\in T$ and zeroing $g_j$ for $j \\\\notin T$; finally $\\\\mathrm{clip}_c$ is\n

\\\\mathrm{clip}_c(g) = \\\\begin{cases} g, & \\\\lVert g\\\\rVert \\\\le c,\\\\\\\\[2pt] \\\\dfrac{c}{\\\\lVert g\\\\rVert}\\\\, g, & \\\\lVert g\\\\rVert > c.\\\\end{cases}

\nThe optimizer $U$ is applied exactly once, to the pre-update state $S$ and the processed gradient; a single certificate, at the point $S.w$, supplies every tile's data. The definition imposes no relation between the tile lists $\\\\mathfrak{B}_k$ and the frame's occurrence set $I_k$: tiles may be empty, overlap, repeat (a repeated tile contributes twice), or contain indices outside $I_k$, and the certificate data are only certified on $I_k$ while the sums run over the tiles as given; an empty tile list yields $g = 0$. The clipping is total for every real $c$ (real division satisfies $x/0 = 0$); note $c = 0$ sends every $g$ to $0$, and negative $c$ makes the branch condition fail for every $g$, producing $(c/\\\\lVert g\\\\rVert)\\\\,g$ — a vector of norm $|c|$ pointing opposite to $g$ (and $0$ when $g = 0$). Note also that supplying the certificate oracle at all states $S$ entails, through the unconditional hh field, differentiability of each $h_k$ at every parameter vector $w \\\\in \\\\mathbb{R}^d$.\n\n**monoRun.** For all $d, m \\\\in \\\\mathbb{N}$ and every type $\\\\iota$ (no decidable-equality assumption here), given a frame schedule $\\\\xi = (\\\\xi_k)_k$, a finite trainable-coordinate set $T \\\\subseteq \\\\{0,\\\\dots,d-1\\\\}$, a real clipping radius $c$, and an optimizer $U$, this defines the one-step transition sending the state $S$ at logical step $k$ to\n

$$U\\\\Big(S,\\\\; \\\\mathrm{clip}_c\\\\big(P_T\\\\,(\\\\mathrm{monoGrad}(\\\\xi_k, S.w))\\\\big)\\\\Big),$$

\nthat is: the monolithic gradient of $L_{\\\\xi_k}$ at the current parameters $S.w$ (zero by convention wherever $L_{\\\\xi_k}$ is not differentiable there), followed by the same coordinate projection $P_T$ and the same clipping $\\\\mathrm{clip}_c$ as in tiledRun, then a single application of $U$. No certificates, tiles, or differentiability hypotheses are involved; the definition is total for every schedule.\n\n**runFrom.** For an arbitrary type $\\\\sigma$ (implicit) and an arbitrary step function $\\\\mathrm{step} : \\\\sigma \\\\to \\\\mathbb{N} \\\\to \\\\sigma$ (a map taking a state and a natural step index to a new state), this defines a function $\\\\mathbb{N} \\\\to \\\\sigma \\\\to \\\\sigma$ by recursion on the number of steps:\n\n- $\\\\mathrm{runFrom}\\\\; \\\\mathrm{step}\\\\; 0\\\\; S = S$;\n- $\\\\mathrm{runFrom}\\\\; \\\\mathrm{step}\\\\; (n+1)\\\\; S = \\\\mathrm{runFrom}\\\\; \\\\mathrm{step}\\\\; n\\\\; \\\\big(\\\\mathrm{step}\\\\; S\\\\; n\\\\big)$.\n\nThus $\\\\mathrm{runFrom}\\\\; \\\\mathrm{step}\\\\; n\\\\; S$ applies $\\\\mathrm{step}$ exactly $n$ times, the applications receiving the step indices $n-1, n-2, \\\\dots, 1, 0$ in that order:\n

$$\\\\mathrm{runFrom}\\\\; \\\\mathrm{step}\\\\; n\\\\; S \\\\;=\\\\; \\\\mathrm{step}\\\\big(\\\\dots \\\\mathrm{step}\\\\big(\\\\mathrm{step}(S,\\\\, n-1),\\\\, n-2\\\\big) \\\\dots,\\\\, 0\\\\big).$$

\nAt $n = 0$ the state is returned unchanged. The definition is generic in $\\\\sigma$; it is not tied to training states, frames, or any particular step function."\n}', 'startLine': 1, 'lineNumbers': [1, 2, 3, 4]}, 'meta': {'source': {'type': 'internal', 'value': 'agent://RB2-VathekState'}}}}