T0 — Exact logical training and restart preservation

{'text': '{\n "readback": "Setting and hypotheses.\n\nLet $d, m$ be natural numbers; write $W = \\\\mathbb{R}^d$ and $V = \\\\mathbb{R}^m$ for the Euclidean spaces of logical parameters and shared state. Let $\\\\iota$ be an arbitrary type (of occurrence indices), assumed to carry decidable equality; it may be finite or infinite, empty or nonempty. The theorem fixes the following data:\n\n- a frame schedule $\\\\xi$: for each $k \\\\in \\\\mathbb{N}$, a frame $\\\\xi_k = (h_k,\\\\, f_k,\\\\, \\\\alpha_k,\\\\, I_k)$ consisting of a map $h_k : W \\\\to V$ (the shared computation), a family of loss maps $f_k(\\\\cdot) : \\\\iota \\\\to (W \\\\times V \\\\to \\\\mathbb{R})$, a family of real reduction coefficients $\\\\alpha_k : \\\\iota \\\\to \\\\mathbb{R}$ (no sign condition is imposed — they may be zero or negative), and a finite occurrence set $I_k \\\\subseteq \\\\iota$;\n- a tile schedule $\\\\mathfrak{B}$: for each $k$, a finite list $\\\\mathcal{B}_k = (B_1, \\\\dots, B_r)$ of finite subsets (\"tiles\") of $\\\\iota$;\n- the training-state space: a state is a record $S = (w, \\\\mu_1, \\\\mu_2, t)$ with parameters $w \\\\in W$, two moment vectors $\\\\mu_1, \\\\mu_2 \\\\in W$, and a step counter $t \\\\in \\\\mathbb{N}$;\n- a set $T \\\\subseteq \\\\{0, \\\\dots, d-1\\\\}$ of trainable coordinates, a real number $c$ (clipping radius; no sign condition), an arbitrary deterministic optimizer map $U : \\\\text{state} \\\\times W \\\\to \\\\text{state}$, an initial state $S_0$, and a horizon $n \\\\in \\\\mathbb{N}$.\n\nTwo hypotheses are assumed:\n\n1. Valid tile partition at every step. For every $k$: the union of the tiles equals the occurrence set, $\\\\bigcup_{B \\\\in \\\\mathcal{B}_k} B = I_k$, and the tiles in the list are pairwise disjoint. Empty tiles are permitted (any number of them), as are uneven tiles.\n\n2. Derivative certificates at every pre-update point. For every $k \\\\in \\\\mathbb{N}$ and every state $S$ — not merely states reachable from $S_0$ — there is given a certificate for the frame $\\\\xi_k$ at the parameter vector $S.w$, comprising:\n - a continuous linear map $Dh_{k,S} : W \\\\to V$, certified to be the Fréchet derivative of $h_k$ at $S.w$;\n - numbers $v_i^{k,S} \\\\in \\\\mathbb{R}$ ($i \\\\in \\\\iota$), certified to satisfy $v_i^{k,S} = f_k(i)\\\\big(S.w,\\\\, h_k(S.w)\\\\big)$ for every $i \\\\in I_k$;\n - vectors $\\\\mathbf{a}_i^{k,S} \\\\in W$ ($i \\\\in \\\\iota$), certified (for $i \\\\in I_k$) to be the gradient, at $S.w$, of the map w\' \\\\mapsto f_k(i)\\\\big(w\',\\\\, h_k(S.w)\\\\big) with the shared value frozen;\n - vectors $\\\\mathbf{s}_i^{k,S} \\\\in V$ ($i \\\\in \\\\iota$), certified (for $i \\\\in I_k$) to be the gradient, at $h_k(S.w)$, of the map $u \\\\mapsto f_k(i)\\\\big(S.w,\\\\, u\\\\big)$ with the parameters frozen;\n - the assertion that each $f_k(i)$ is differentiable at the point $\\\\big(S.w,\\\\, h_k(S.w)\\\\big)$, for every $i \\\\in I_k$.\n\n The certificates pin down $Dh_{k,S}$ and the values of $v_i^{k,S}, \\\\mathbf{a}_i^{k,S}, \\\\mathbf{s}_i^{k,S}$ on $I_k$ exactly; outside $I_k$ the three families are unconstrained (such indices never enter the sums below, because the tiles cover exactly $I_k$).\n\nUnder these hypotheses, the theorem asserts a conjunction of three statements.\n\nFirst conjunct — the two evaluators agree at every state and every index. For every $k \\\\in \\\\mathbb{N}$ and every state $S$ (this conjunct involves none of $T, c, U, S_0, n$; the quantification over $k$ covers all natural numbers, not only $k < n$):\n\n**(a) Loss agreement.**\n\n

\n\nThe left side is the loss slot of a streaming fold that starts from the triple (running loss, running direct vector, running shared vector) $= (0, \\\\mathbf{0}, \\\\mathbf{0})$ and processes the tiles of $\\\\mathcal{B}_k$ in list order, each tile $B$ adding $\\\\sum_{i \\\\in B} \\\\alpha_k(i) v_i^{k,S}$, $\\\\sum_{i \\\\in B} \\\\alpha_k(i)\\\\, \\\\mathbf{a}_i^{k,S}$, and $\\\\sum_{i \\\\in B} \\\\alpha_k(i)\\\\, \\\\mathbf{s}_i^{k,S}$ to the three slots respectively. The right side is the monolithic loss of frame $k$, $L_k(w) := \\\\sum_{i \\\\in I_k} \\\\alpha_k(i)\\\\, f_k(i)\\\\big(w, h_k(w)\\\\big)$, evaluated at $w = S.w$.\n\n**(b) Gradient agreement.**\n\n

\n\nThe left side is the accumulated direct contributions plus one application of the transpose (adjoint) of the certified shared derivative to the accumulated shared cotangents. The right side, the monolithic gradient, is defined as the Riesz representation vector of the Fréchet derivative of $L_k$ at $S.w$ — a total definition: at a point where $L_k$ is not differentiable, the derivative operator is taken to be zero, so the \"gradient\" is $\\\\mathbf{0}$.\n\nSecond conjunct — equality of the two $n$-step runs, for the single fixed horizon $n$. Define two step maps on states:\n\n- tiled step at logical index $j$: $S \\\\;\\\\mapsto\\\\; U\\\\big(S,\\\\; \\\\mathrm{clip}_c(P_T(g^{\\\\mathrm{tile}}_{j,S}))\\\\big)$, where $g^{\\\\mathrm{tile}}_{j,S}$ is the tiled gradient of (b), computed from the certificates at the current state (all tiles read the same pre-update parameters $S.w$; no parameter changes between tiles) and the tile list $\\\\mathcal{B}_j$;\n- monolithic step at logical index $j$: $S \\\\;\\\\mapsto\\\\; U\\\\big(S,\\\\; \\\\mathrm{clip}_c(P_T(\\\\nabla L_j(S.w)))\\\\big)$.\n\nHere $P_T$ is the coordinate projection that keeps coordinate j\' when j\' \\\\in T and zeroes it otherwise, and the clipping $\\\\mathrm{clip}_c$ keeps $g$ when $\\\\lVert g \\\\rVert \\\\le c$ and otherwise replaces it by $\\\\tfrac{c}{\\\\lVert g \\\\rVert}\\\\, g$. In both maps the optimizer $U$ is applied exactly once per logical step.\n\nThe iteration convention is: a $0$-step run returns the state unchanged; a $(j{+}1)$-step run applies the step function once — passing it the logical index $j$ — and then iterates $j$ more times. Consequently an $n$-step run applies the step map with logical indices $n-1, n-2, \\\\dots, 0$ in that order: the first executed update consults frame $\\\\xi_{n-1}$ and tiles $\\\\mathcal{B}_{n-1}$, the last consults $\\\\xi_0$ and $\\\\mathcal{B}_0$.\n\nThe claim: the state reached after $n$ tiled steps from $S_0$ equals the state reached after $n$ monolithic steps from $S_0$ — an equality of complete records (parameters, both moment vectors, and step counter). Only the final states are asserted equal, and only at this one fixed $n$ (the theorem is universally quantified over $n$ from outside, so other horizons are obtained by re-instantiation).\n\nThird conjunct — checkpoint and restart preservation. The snapshot map replaces each of the three vectors of a state by its list of $d$ coordinates $[x_0, \\\\dots, x_{d-1}]$ (exact real coordinates, no rounding) and keeps the counter $t$. The reconstruction map rebuilds each vector from a coordinate list by taking the $j$-th entry if the list has one and $0$ otherwise — a total decoder (missing coordinates default to $0$), though for a snapshotted list of length exactly $d$ it is the exact coordinatewise inverse. For every checkpoint step $a$ with $0 \\\\le a \\\\le n$:\n\n

\n\nthat is: run the tiled evaluator $a$ steps from $S_0$, snapshot, reconstruct, then run the tiled evaluator the remaining $n - a$ steps (recall $n - a$ is ordinary natural-number subtraction, well defined since $a \\\\le n$); the resulting state equals the uninterrupted $n$-step monolithic run from $S_0$. The monolithic side is never interrupted. Note the effect of the countdown indexing convention: the left side consults the frame/tile schedule at indices $a-1, \\\\dots, 0$ (first segment) and then $n-a-1, \\\\dots, 0$ (second segment), whereas the right side consults $n-1, \\\\dots, 0$; for instance at $n = 2$, $a = 1$ the restarted run uses frame index $0$ twice while the monolithic run uses indices $1$ then $0$. The equality of resulting states is asserted as stated.\n\nWhat the quantifiers silently include (edge and degenerate cases).\n\n- $n = 0$: the second conjunct reads $S_0 = S_0$; the third conjunct admits only $a = 0$ (since $a \\\\le 0$) and asserts $\\\\mathrm{restore}(\\\\mathrm{snap}(S_0)) = S_0$. The first conjunct is unaffected by $n$ — it is asserted for every $k \\\\in \\\\mathbb{N}$ and every state $S$, including step indices far beyond any run's horizon.\n- Boundary checkpoints in the third conjunct: at $a = 0$ the checkpoint is the round-trip of $S_0$ itself and $n - a = n$ steps remain; at $a = n$ zero steps remain and the claim is that round-tripping the final tiled state already yields the final monolithic state.\n- The certificate hypothesis is global: it demands differentiability data for $h_k$ and every $f_k(i)$ at the parameter vector of every conceivable state, together with the values and gradients there. The theorem says nothing about when such certificates exist; they are assumed given.\n- Clipping is a two-branch total map: for $c \\\\ge 0$ it fixes $g$ when $\\\\lVert g\\\\rVert \\\\le c$ (in particular $g = \\\\mathbf 0$ is fixed) and otherwise rescales to norm exactly $c$. For $c < 0$ the condition $\\\\lVert g \\\\rVert \\\\le c$ can never hold (norms are $\\\\ge 0$), so every vector is sent to $\\\\tfrac{c}{\\\\lVert g\\\\rVert} g$ — a vector of norm $|c|$ pointing opposite to $g$; at $g = \\\\mathbf 0$ this uses the convention $c/0 = 0$ and returns $\\\\mathbf 0$.\n- $T$ may be empty (every update direction is masked to $\\\\mathbf 0$ before the optimizer is applied) or all of $\\\\{0,\\\\dots,d-1\\\\}$ (no masking).\n- If $I_k = \\\\emptyset$, the partition hypothesis forces every tile of $\\\\mathcal{B}_k$ to be empty; all sums in the first conjunct are empty sums, the monolithic loss is the constant $0$, and its gradient is $\\\\mathbf 0$.\n- All equalities are exact equalities of real numbers, vectors, and records; no rounding, tolerance, or floating-point notion appears anywhere in the statement. Nothing is asserted about loss decreasing, convergence, execution speed, or any property of $U$ beyond it being a fixed function applied identically in both evaluators."\n}', 'details': {'resolvedPath': '/home/ajax/.omp/agent/sessions/-math/2026-09-22T19-31-08-510Z_01a0ca99-be5e-7000-93c6-dac7c74cc004/RB2-T0.md', 'contentType': 'text/markdown', 'totalLines': 3, 'displayContent': {'text': '{\n "readback": "Setting and hypotheses.\n\nLet $d, m$ be natural numbers; write $W = \\\\mathbb{R}^d$ and $V = \\\\mathbb{R}^m$ for the Euclidean spaces of logical parameters and shared state. Let $\\\\iota$ be an arbitrary type (of occurrence indices), assumed to carry decidable equality; it may be finite or infinite, empty or nonempty. The theorem fixes the following data:\n\n- a frame schedule $\\\\xi$: for each $k \\\\in \\\\mathbb{N}$, a frame $\\\\xi_k = (h_k,\\\\, f_k,\\\\, \\\\alpha_k,\\\\, I_k)$ consisting of a map $h_k : W \\\\to V$ (the shared computation), a family of loss maps $f_k(\\\\cdot) : \\\\iota \\\\to (W \\\\times V \\\\to \\\\mathbb{R})$, a family of real reduction coefficients $\\\\alpha_k : \\\\iota \\\\to \\\\mathbb{R}$ (no sign condition is imposed — they may be zero or negative), and a finite occurrence set $I_k \\\\subseteq \\\\iota$;\n- a tile schedule $\\\\mathfrak{B}$: for each $k$, a finite list $\\\\mathcal{B}_k = (B_1, \\\\dots, B_r)$ of finite subsets (\"tiles\") of $\\\\iota$;\n- the training-state space: a state is a record $S = (w, \\\\mu_1, \\\\mu_2, t)$ with parameters $w \\\\in W$, two moment vectors $\\\\mu_1, \\\\mu_2 \\\\in W$, and a step counter $t \\\\in \\\\mathbb{N}$;\n- a set $T \\\\subseteq \\\\{0, \\\\dots, d-1\\\\}$ of trainable coordinates, a real number $c$ (clipping radius; no sign condition), an arbitrary deterministic optimizer map $U : \\\\text{state} \\\\times W \\\\to \\\\text{state}$, an initial state $S_0$, and a horizon $n \\\\in \\\\mathbb{N}$.\n\nTwo hypotheses are assumed:\n\n1. Valid tile partition at every step. For every $k$: the union of the tiles equals the occurrence set, $\\\\bigcup_{B \\\\in \\\\mathcal{B}_k} B = I_k$, and the tiles in the list are pairwise disjoint. Empty tiles are permitted (any number of them), as are uneven tiles.\n\n2. Derivative certificates at every pre-update point. For every $k \\\\in \\\\mathbb{N}$ and every state $S$ — not merely states reachable from $S_0$ — there is given a certificate for the frame $\\\\xi_k$ at the parameter vector $S.w$, comprising:\n - a continuous linear map $Dh_{k,S} : W \\\\to V$, certified to be the Fréchet derivative of $h_k$ at $S.w$;\n - numbers $v_i^{k,S} \\\\in \\\\mathbb{R}$ ($i \\\\in \\\\iota$), certified to satisfy $v_i^{k,S} = f_k(i)\\\\big(S.w,\\\\, h_k(S.w)\\\\big)$ for every $i \\\\in I_k$;\n - vectors $\\\\mathbf{a}_i^{k,S} \\\\in W$ ($i \\\\in \\\\iota$), certified (for $i \\\\in I_k$) to be the gradient, at $S.w$, of the map w\' \\\\mapsto f_k(i)\\\\big(w\',\\\\, h_k(S.w)\\\\big) with the shared value frozen;\n - vectors $\\\\mathbf{s}_i^{k,S} \\\\in V$ ($i \\\\in \\\\iota$), certified (for $i \\\\in I_k$) to be the gradient, at $h_k(S.w)$, of the map $u \\\\mapsto f_k(i)\\\\big(S.w,\\\\, u\\\\big)$ with the parameters frozen;\n - the assertion that each $f_k(i)$ is differentiable at the point $\\\\big(S.w,\\\\, h_k(S.w)\\\\big)$, for every $i \\\\in I_k$.\n\n The certificates pin down $Dh_{k,S}$ and the values of $v_i^{k,S}, \\\\mathbf{a}_i^{k,S}, \\\\mathbf{s}_i^{k,S}$ on $I_k$ exactly; outside $I_k$ the three families are unconstrained (such indices never enter the sums below, because the tiles cover exactly $I_k$).\n\nUnder these hypotheses, the theorem asserts a conjunction of three statements.\n\nFirst conjunct — the two evaluators agree at every state and every index. For every $k \\\\in \\\\mathbb{N}$ and every state $S$ (this conjunct involves none of $T, c, U, S_0, n$; the quantification over $k$ covers all natural numbers, not only $k < n$):\n\n**(a) Loss agreement.**\n\n

\n\nThe left side is the loss slot of a streaming fold that starts from the triple (running loss, running direct vector, running shared vector) $= (0, \\\\mathbf{0}, \\\\mathbf{0})$ and processes the tiles of $\\\\mathcal{B}_k$ in list order, each tile $B$ adding $\\\\sum_{i \\\\in B} \\\\alpha_k(i) v_i^{k,S}$, $\\\\sum_{i \\\\in B} \\\\alpha_k(i)\\\\, \\\\mathbf{a}_i^{k,S}$, and $\\\\sum_{i \\\\in B} \\\\alpha_k(i)\\\\, \\\\mathbf{s}_i^{k,S}$ to the three slots respectively. The right side is the monolithic loss of frame $k$, $L_k(w) := \\\\sum_{i \\\\in I_k} \\\\alpha_k(i)\\\\, f_k(i)\\\\big(w, h_k(w)\\\\big)$, evaluated at $w = S.w$.\n\n**(b) Gradient agreement.**\n\n

\n\nThe left side is the accumulated direct contributions plus one application of the transpose (adjoint) of the certified shared derivative to the accumulated shared cotangents. The right side, the monolithic gradient, is defined as the Riesz representation vector of the Fréchet derivative of $L_k$ at $S.w$ — a total definition: at a point where $L_k$ is not differentiable, the derivative operator is taken to be zero, so the \"gradient\" is $\\\\mathbf{0}$.\n\nSecond conjunct — equality of the two $n$-step runs, for the single fixed horizon $n$. Define two step maps on states:\n\n- tiled step at logical index $j$: $S \\\\;\\\\mapsto\\\\; U\\\\big(S,\\\\; \\\\mathrm{clip}_c(P_T(g^{\\\\mathrm{tile}}_{j,S}))\\\\big)$, where $g^{\\\\mathrm{tile}}_{j,S}$ is the tiled gradient of (b), computed from the certificates at the current state (all tiles read the same pre-update parameters $S.w$; no parameter changes between tiles) and the tile list $\\\\mathcal{B}_j$;\n- monolithic step at logical index $j$: $S \\\\;\\\\mapsto\\\\; U\\\\big(S,\\\\; \\\\mathrm{clip}_c(P_T(\\\\nabla L_j(S.w)))\\\\big)$.\n\nHere $P_T$ is the coordinate projection that keeps coordinate j\' when j\' \\\\in T and zeroes it otherwise, and the clipping $\\\\mathrm{clip}_c$ keeps $g$ when $\\\\lVert g \\\\rVert \\\\le c$ and otherwise replaces it by $\\\\tfrac{c}{\\\\lVert g \\\\rVert}\\\\, g$. In both maps the optimizer $U$ is applied exactly once per logical step.\n\nThe iteration convention is: a $0$-step run returns the state unchanged; a $(j{+}1)$-step run applies the step function once — passing it the logical index $j$ — and then iterates $j$ more times. Consequently an $n$-step run applies the step map with logical indices $n-1, n-2, \\\\dots, 0$ in that order: the first executed update consults frame $\\\\xi_{n-1}$ and tiles $\\\\mathcal{B}_{n-1}$, the last consults $\\\\xi_0$ and $\\\\mathcal{B}_0$.\n\nThe claim: the state reached after $n$ tiled steps from $S_0$ equals the state reached after $n$ monolithic steps from $S_0$ — an equality of complete records (parameters, both moment vectors, and step counter). Only the final states are asserted equal, and only at this one fixed $n$ (the theorem is universally quantified over $n$ from outside, so other horizons are obtained by re-instantiation).\n\nThird conjunct — checkpoint and restart preservation. The snapshot map replaces each of the three vectors of a state by its list of $d$ coordinates $[x_0, \\\\dots, x_{d-1}]$ (exact real coordinates, no rounding) and keeps the counter $t$. The reconstruction map rebuilds each vector from a coordinate list by taking the $j$-th entry if the list has one and $0$ otherwise — a total decoder (missing coordinates default to $0$), though for a snapshotted list of length exactly $d$ it is the exact coordinatewise inverse. For every checkpoint step $a$ with $0 \\\\le a \\\\le n$:\n\n

\n\nthat is: run the tiled evaluator $a$ steps from $S_0$, snapshot, reconstruct, then run the tiled evaluator the remaining $n - a$ steps (recall $n - a$ is ordinary natural-number subtraction, well defined since $a \\\\le n$); the resulting state equals the uninterrupted $n$-step monolithic run from $S_0$. The monolithic side is never interrupted. Note the effect of the countdown indexing convention: the left side consults the frame/tile schedule at indices $a-1, \\\\dots, 0$ (first segment) and then $n-a-1, \\\\dots, 0$ (second segment), whereas the right side consults $n-1, \\\\dots, 0$; for instance at $n = 2$, $a = 1$ the restarted run uses frame index $0$ twice while the monolithic run uses indices $1$ then $0$. The equality of resulting states is asserted as stated.\n\nWhat the quantifiers silently include (edge and degenerate cases).\n\n- $n = 0$: the second conjunct reads $S_0 = S_0$; the third conjunct admits only $a = 0$ (since $a \\\\le 0$) and asserts $\\\\mathrm{restore}(\\\\mathrm{snap}(S_0)) = S_0$. The first conjunct is unaffected by $n$ — it is asserted for every $k \\\\in \\\\mathbb{N}$ and every state $S$, including step indices far beyond any run's horizon.\n- Boundary checkpoints in the third conjunct: at $a = 0$ the checkpoint is the round-trip of $S_0$ itself and $n - a = n$ steps remain; at $a = n$ zero steps remain and the claim is that round-tripping the final tiled state already yields the final monolithic state.\n- The certificate hypothesis is global: it demands differentiability data for $h_k$ and every $f_k(i)$ at the parameter vector of every conceivable state, together with the values and gradients there. The theorem says nothing about when such certificates exist; they are assumed given.\n- Clipping is a two-branch total map: for $c \\\\ge 0$ it fixes $g$ when $\\\\lVert g\\\\rVert \\\\le c$ (in particular $g = \\\\mathbf 0$ is fixed) and otherwise rescales to norm exactly $c$. For $c < 0$ the condition $\\\\lVert g \\\\rVert \\\\le c$ can never hold (norms are $\\\\ge 0$), so every vector is sent to $\\\\tfrac{c}{\\\\lVert g\\\\rVert} g$ — a vector of norm $|c|$ pointing opposite to $g$; at $g = \\\\mathbf 0$ this uses the convention $c/0 = 0$ and returns $\\\\mathbf 0$.\n- $T$ may be empty (every update direction is masked to $\\\\mathbf 0$ before the optimizer is applied) or all of $\\\\{0,\\\\dots,d-1\\\\}$ (no masking).\n- If $I_k = \\\\emptyset$, the partition hypothesis forces every tile of $\\\\mathcal{B}_k$ to be empty; all sums in the first conjunct are empty sums, the monolithic loss is the constant $0$, and its gradient is $\\\\mathbf 0$.\n- All equalities are exact equalities of real numbers, vectors, and records; no rounding, tolerance, or floating-point notion appears anywhere in the statement. Nothing is asserted about loss decreasing, convergence, execution speed, or any property of $U$ beyond it being a fixed function applied identically in both evaluators."\n}', 'startLine': 1, 'lineNumbers': [1, 2, 3]}, 'meta': {'source': {'type': 'internal', 'value': 'agent://RB2-T0'}}}}