M11 — Restart equivalence

{'text': '{\n "readback": "Setting. Fix natural numbers $d$ (logical parameter dimension) and $m$ (shared-state dimension) and a type $\\\\iota$ (the occurrence-index type, possibly empty or infinite) on which equality is decidable. Write $\\\\mathbb{R}^d$, $\\\\mathbb{R}^m$ for the Euclidean coordinate spaces with the usual Euclidean norm $\\\\|\\\\cdot\\\\|$.\n\nAssertion (M11 restart equivalence). For every $d, m \\\\in \\\\mathbb{N}$, every type $\\\\iota$ with decidable equality, and all of the following data:\n\n- a frame schedule $\\\\xi = (\\\\xi_k)_{k \\\\in \\\\mathbb{N}}$: each frame $\\\\xi_k$ consists of a shared map $h_k : \\\\mathbb{R}^d \\\\to \\\\mathbb{R}^m$, per-occurrence loss maps $f_{k,i} : \\\\mathbb{R}^d \\\\times \\\\mathbb{R}^m \\\\to \\\\mathbb{R}$, real coefficients $\\\\alpha_{k,i} \\\\in \\\\mathbb{R}$ (no sign constraint), and a finite occurrence set $I_k \\\\subseteq \\\\iota$;\n- a tile 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 finite set $T \\\\subseteq \\\\{0,\\\\dots,d-1\\\\}$ of trainable coordinates;\n- a real number $c$ (clipping radius; no sign hypothesis);\n- an arbitrary map $U : \\\\text{state} \\\\to \\\\mathbb{R}^d \\\\to \\\\text{state}$ (the optimizer; no assumption on it — it need not use the direction, advance any counter, or be continuous);\n- an initial state $S_0$;\n- natural numbers $n$ (total steps) and $a$ (checkpoint step);\n\nsubject to the three hypotheses below, the following equality of training states holds:\n\n

\n\nHypotheses.\n\n1. $a \\\\le n$ (so the natural-number subtraction $n - a$ is untruncated and equals the ordinary difference).\n2. Tile partition, for every $k \\\\in \\\\mathbb{N}$ (not just $k < n$): the union of the tiles in the list $\\\\mathfrak{B}_k$ is exactly $I_k$, and any two tiles at distinct positions of the list are disjoint. Empty tiles are allowed (also repeated, since $\\\\varnothing$ is disjoint from itself), tile sizes may be uneven; an empty list is allowed exactly when $I_k = \\\\varnothing$, and if $I_k = \\\\varnothing$ every tile must be empty.\n3. Derivative certificates, for every $k \\\\in \\\\mathbb{N}$ and every state $S$ (including states never reached by any run): a package $D_{k,S}$ for the frame $\\\\xi_k$ at the pre-update point $S.w$, consisting of:\n - a continuous linear map h\'_{k,S} : \\\\mathbb{R}^d \\\\to \\\\mathbb{R}^m together with a certificate that it is the Fréchet derivative of $h_k$ at $S.w$;\n - per-occurrence values $\\\\mathrm{val}_{k,S}(i) \\\\in \\\\mathbb{R}$, certified — for $i \\\\in I_k$ only — by the field hval: $\\\\mathrm{val}_{k,S}(i) = f_{k,i}\\\\big(S.w,\\\\; h_k(S.w)\\\\big)$;\n - per-occurrence direct gradients $\\\\mathrm{direct}_{k,S}(i) \\\\in \\\\mathbb{R}^d$, certified for $i \\\\in I_k$ to be the gradient at $S.w$ of $w \\\\mapsto f_{k,i}\\\\big(w,\\\\, h_k(S.w)\\\\big)$ — note the shared map is frozen at its pre-update value here, not composed;\n - per-occurrence shared cotangents $\\\\mathrm{shared}_{k,S}(i) \\\\in \\\\mathbb{R}^m$, certified for $i \\\\in I_k$ to be the gradient at $h_k(S.w)$ of $v \\\\mapsto f_{k,i}(S.w, v)$;\n - for $i \\\\in I_k$, differentiability of $f_{k,i}$ at $(S.w,\\\\, h_k(S.w))$.\n \n For $i \\\\notin I_k$ the three families $\\\\mathrm{val}, \\\\mathrm{direct}, \\\\mathrm{shared}$ carry arbitrary, unconstrained values.\n\nStates. A training state is a quadruple $S = (w, \\\\mu_1, \\\\mu_2, t)$: parameter vector $w \\\\in \\\\mathbb{R}^d$, first-moment vector $\\\\mu_1 \\\\in \\\\mathbb{R}^d$, second-moment vector $\\\\mu_2 \\\\in \\\\mathbb{R}^d$, and a natural-number step counter $t$. The asserted equality is equality of whole states, i.e. all four components agree.\n\nThe tiled step (index $k$, state $S$). Everything is read once at the fixed pre-update point $S.w$; no parameter changes between tiles. The gradient is\n\n

\n\nwhere $(\\\\cdot)^{*}$ is the adjoint (transpose) of the certified derivative h\'_{k,S}, and the sums accumulate tile by tile through the list $\\\\mathfrak{B}_k$ from zero. (The accumulator also maintains a running weighted loss $\\\\sum_B \\\\sum_{i\\\\in B} \\\\alpha_{k,i}\\\\,\\\\mathrm{val}_{k,S}(i)$, but that slot is not read by the step — so $\\\\mathrm{val}$, and hence its hval certificate, has no influence on the tiled trajectory.) The new state is\n\n

\n\nwhere $P_T$ is the coordinate projection keeping coordinates $j \\\\in T$ and zeroing $j \\\\notin T$, and $\\\\operatorname{clip}_c(g) = g$ if $\\\\|g\\\\| \\\\le c$, otherwise $\\\\tfrac{c}{\\\\|g\\\\|}\\\\, g$. The clip is a total function: at $g = 0$ both branches return $0$; for negative $c$ the second branch reverses direction and rescales to norm $|c|$.\n\nThe monolithic step (index $k$, state $S$). Let $L_k(w) = \\\\sum_{i \\\\in I_k} \\\\alpha_{k,i}\\\\, f_{k,i}\\\\big(w, h_k(w)\\\\big)$ be the whole logical objective of frame $k$. Its gradient is taken as\n\n

\n\nthe Riesz-representation vector of the Fréchet differential of $L_k$ at $S.w$. The derivative operation is total: where $L_k$ is not differentiable it returns a junk value, and the statement contains no hypothesis directly asserting this derivative is genuine. The new state is $U\\\\big(S,\\\\, \\\\operatorname{clip}_c(P_T\\\\, g^{\\\\mathrm{mono}}_k(S))\\\\big)$ — same projection, same clipping, same single application of $U$ as in the tiled step.\n\nRunning $k$ steps. $\\\\operatorname{runFrom}(\\\\text{step}, 0, S) = S$ and $\\\\operatorname{runFrom}(\\\\text{step}, k+1, S) = \\\\operatorname{runFrom}(\\\\text{step}, k, \\\\text{step}(S, k))$. Hence $\\\\operatorname{runFrom}(\\\\text{step}, k, S)$ applies the step function $k$ times, the first application carrying step index $k-1$, the next $k-2$, …, the last carrying index $0$: the step index counts down from $k-1$ to $0$.\n\nSnapshot and restore. $\\\\operatorname{snap}$ serializes a state as the tuple of coordinate lists (each of $w, \\\\mu_1, \\\\mu_2$ becomes its list of exactly $d$ real coordinates) together with the counter $t$. $\\\\operatorname{restore}$ rebuilds each vector by reading coordinate $j$ from the $j$-th list entry, defaulting missing entries to $0$ — a default that never fires on a snapshot, since each list has length exactly $d$. Hence $\\\\operatorname{restore}(\\\\operatorname{snap}(S)) = S$ exactly: an idealized, infinite-precision real-valued round trip (no finite-byte codec is modeled).\n\nThe two sides compared.\n\n- Left: run $a$ tiled steps from $S_0$, consuming step indices $a-1, a-2, \\\\ldots, 0$ in that order; snapshot the resulting state and restore it (recovering exactly the same state); then run a further $n - a$ tiled steps, consuming step indices $n-a-1, n-a-2, \\\\ldots, 0$ in that order.\n- Right: run $n$ monolithic steps from $S_0$, consuming step indices $n-1, n-2, \\\\ldots, 0$ in that order.\n\nNote the index bookkeeping this implies: the left side's full sequence of frame indices is $a-1,\\\\ldots,0$ followed by $n-a-1,\\\\ldots,0$ (index $0$ is consumed twice whenever $a > 0$ and $n - a > 0$, and no index $\\\\ge n-a$ is consumed by the second segment), while the right side consumes each of $n-1, \\\\ldots, 0$ exactly once.\n\nDegenerate and edge cases.\n\n- $a = 0$: the first segment is empty and $n - 0 = n$; since $\\\\operatorname{restore}(\\\\operatorname{snap}(S_0)) = S_0$, the claim becomes: $n$ tiled steps from $S_0$ equal $n$ monolithic steps from $S_0$ — the full tiled-vs-monolithic equivalence.\n- $a = n$: the continuation is empty ($n - n = 0$); the claim becomes $\\\\operatorname{restore}(\\\\operatorname{snap}(\\\\text{state after } n \\\\text{ tiled steps})) = \\\\text{state after } n \\\\text{ monolithic steps}$.\n- $n = 0$: forces $a = 0$; the claim reduces to $\\\\operatorname{restore}(\\\\operatorname{snap}(S_0)) = S_0$.\n- $T = \\\\varnothing$: every gradient is masked to $0$ before clipping, so every step (both evaluators) applies $U(S, 0)$. $T$ = all coordinates: the mask is the identity.\n- No sign or positivity assumption on $c$ or on the coefficients $\\\\alpha_{k,i}$.\n- If $I_k = \\\\varnothing$ for some $k$: every tile of $\\\\mathfrak{B}_k$ is then empty, the tiled gradient is 0 + (h\'_{k,S})^{*}(0) = 0, and the monolithic objective is the empty sum, identically $0$.\n- $d = 0$ or $m = 0$ are permitted; the corresponding vector spaces are trivial (all vectors are $0$).\n- $U$ is universally quantified with no restriction, and the hypotheses of tile-partition and certificates are demanded at every $k \\\\in \\\\mathbb{N}$ and (for certificates) every state, not merely along the run."\n}', 'details': {'resolvedPath': '/home/ajax/.omp/agent/sessions/-math/2026-09-22T19-31-08-510Z_01a0ca99-be5e-7000-93c6-dac7c74cc004/RB2-M11.md', 'contentType': 'text/markdown', 'totalLines': 3, 'displayContent': {'text': '{\n "readback": "Setting. Fix natural numbers $d$ (logical parameter dimension) and $m$ (shared-state dimension) and a type $\\\\iota$ (the occurrence-index type, possibly empty or infinite) on which equality is decidable. Write $\\\\mathbb{R}^d$, $\\\\mathbb{R}^m$ for the Euclidean coordinate spaces with the usual Euclidean norm $\\\\|\\\\cdot\\\\|$.\n\nAssertion (M11 restart equivalence). For every $d, m \\\\in \\\\mathbb{N}$, every type $\\\\iota$ with decidable equality, and all of the following data:\n\n- a frame schedule $\\\\xi = (\\\\xi_k)_{k \\\\in \\\\mathbb{N}}$: each frame $\\\\xi_k$ consists of a shared map $h_k : \\\\mathbb{R}^d \\\\to \\\\mathbb{R}^m$, per-occurrence loss maps $f_{k,i} : \\\\mathbb{R}^d \\\\times \\\\mathbb{R}^m \\\\to \\\\mathbb{R}$, real coefficients $\\\\alpha_{k,i} \\\\in \\\\mathbb{R}$ (no sign constraint), and a finite occurrence set $I_k \\\\subseteq \\\\iota$;\n- a tile 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 finite set $T \\\\subseteq \\\\{0,\\\\dots,d-1\\\\}$ of trainable coordinates;\n- a real number $c$ (clipping radius; no sign hypothesis);\n- an arbitrary map $U : \\\\text{state} \\\\to \\\\mathbb{R}^d \\\\to \\\\text{state}$ (the optimizer; no assumption on it — it need not use the direction, advance any counter, or be continuous);\n- an initial state $S_0$;\n- natural numbers $n$ (total steps) and $a$ (checkpoint step);\n\nsubject to the three hypotheses below, the following equality of training states holds:\n\n

\n\nHypotheses.\n\n1. $a \\\\le n$ (so the natural-number subtraction $n - a$ is untruncated and equals the ordinary difference).\n2. Tile partition, for every $k \\\\in \\\\mathbb{N}$ (not just $k < n$): the union of the tiles in the list $\\\\mathfrak{B}_k$ is exactly $I_k$, and any two tiles at distinct positions of the list are disjoint. Empty tiles are allowed (also repeated, since $\\\\varnothing$ is disjoint from itself), tile sizes may be uneven; an empty list is allowed exactly when $I_k = \\\\varnothing$, and if $I_k = \\\\varnothing$ every tile must be empty.\n3. Derivative certificates, for every $k \\\\in \\\\mathbb{N}$ and every state $S$ (including states never reached by any run): a package $D_{k,S}$ for the frame $\\\\xi_k$ at the pre-update point $S.w$, consisting of:\n - a continuous linear map h\'_{k,S} : \\\\mathbb{R}^d \\\\to \\\\mathbb{R}^m together with a certificate that it is the Fréchet derivative of $h_k$ at $S.w$;\n - per-occurrence values $\\\\mathrm{val}_{k,S}(i) \\\\in \\\\mathbb{R}$, certified — for $i \\\\in I_k$ only — by the field hval: $\\\\mathrm{val}_{k,S}(i) = f_{k,i}\\\\big(S.w,\\\\; h_k(S.w)\\\\big)$;\n - per-occurrence direct gradients $\\\\mathrm{direct}_{k,S}(i) \\\\in \\\\mathbb{R}^d$, certified for $i \\\\in I_k$ to be the gradient at $S.w$ of $w \\\\mapsto f_{k,i}\\\\big(w,\\\\, h_k(S.w)\\\\big)$ — note the shared map is frozen at its pre-update value here, not composed;\n - per-occurrence shared cotangents $\\\\mathrm{shared}_{k,S}(i) \\\\in \\\\mathbb{R}^m$, certified for $i \\\\in I_k$ to be the gradient at $h_k(S.w)$ of $v \\\\mapsto f_{k,i}(S.w, v)$;\n - for $i \\\\in I_k$, differentiability of $f_{k,i}$ at $(S.w,\\\\, h_k(S.w))$.\n \n For $i \\\\notin I_k$ the three families $\\\\mathrm{val}, \\\\mathrm{direct}, \\\\mathrm{shared}$ carry arbitrary, unconstrained values.\n\nStates. A training state is a quadruple $S = (w, \\\\mu_1, \\\\mu_2, t)$: parameter vector $w \\\\in \\\\mathbb{R}^d$, first-moment vector $\\\\mu_1 \\\\in \\\\mathbb{R}^d$, second-moment vector $\\\\mu_2 \\\\in \\\\mathbb{R}^d$, and a natural-number step counter $t$. The asserted equality is equality of whole states, i.e. all four components agree.\n\nThe tiled step (index $k$, state $S$). Everything is read once at the fixed pre-update point $S.w$; no parameter changes between tiles. The gradient is\n\n

\n\nwhere $(\\\\cdot)^{*}$ is the adjoint (transpose) of the certified derivative h\'_{k,S}, and the sums accumulate tile by tile through the list $\\\\mathfrak{B}_k$ from zero. (The accumulator also maintains a running weighted loss $\\\\sum_B \\\\sum_{i\\\\in B} \\\\alpha_{k,i}\\\\,\\\\mathrm{val}_{k,S}(i)$, but that slot is not read by the step — so $\\\\mathrm{val}$, and hence its hval certificate, has no influence on the tiled trajectory.) The new state is\n\n

\n\nwhere $P_T$ is the coordinate projection keeping coordinates $j \\\\in T$ and zeroing $j \\\\notin T$, and $\\\\operatorname{clip}_c(g) = g$ if $\\\\|g\\\\| \\\\le c$, otherwise $\\\\tfrac{c}{\\\\|g\\\\|}\\\\, g$. The clip is a total function: at $g = 0$ both branches return $0$; for negative $c$ the second branch reverses direction and rescales to norm $|c|$.\n\nThe monolithic step (index $k$, state $S$). Let $L_k(w) = \\\\sum_{i \\\\in I_k} \\\\alpha_{k,i}\\\\, f_{k,i}\\\\big(w, h_k(w)\\\\big)$ be the whole logical objective of frame $k$. Its gradient is taken as\n\n

\n\nthe Riesz-representation vector of the Fréchet differential of $L_k$ at $S.w$. The derivative operation is total: where $L_k$ is not differentiable it returns a junk value, and the statement contains no hypothesis directly asserting this derivative is genuine. The new state is $U\\\\big(S,\\\\, \\\\operatorname{clip}_c(P_T\\\\, g^{\\\\mathrm{mono}}_k(S))\\\\big)$ — same projection, same clipping, same single application of $U$ as in the tiled step.\n\nRunning $k$ steps. $\\\\operatorname{runFrom}(\\\\text{step}, 0, S) = S$ and $\\\\operatorname{runFrom}(\\\\text{step}, k+1, S) = \\\\operatorname{runFrom}(\\\\text{step}, k, \\\\text{step}(S, k))$. Hence $\\\\operatorname{runFrom}(\\\\text{step}, k, S)$ applies the step function $k$ times, the first application carrying step index $k-1$, the next $k-2$, …, the last carrying index $0$: the step index counts down from $k-1$ to $0$.\n\nSnapshot and restore. $\\\\operatorname{snap}$ serializes a state as the tuple of coordinate lists (each of $w, \\\\mu_1, \\\\mu_2$ becomes its list of exactly $d$ real coordinates) together with the counter $t$. $\\\\operatorname{restore}$ rebuilds each vector by reading coordinate $j$ from the $j$-th list entry, defaulting missing entries to $0$ — a default that never fires on a snapshot, since each list has length exactly $d$. Hence $\\\\operatorname{restore}(\\\\operatorname{snap}(S)) = S$ exactly: an idealized, infinite-precision real-valued round trip (no finite-byte codec is modeled).\n\nThe two sides compared.\n\n- Left: run $a$ tiled steps from $S_0$, consuming step indices $a-1, a-2, \\\\ldots, 0$ in that order; snapshot the resulting state and restore it (recovering exactly the same state); then run a further $n - a$ tiled steps, consuming step indices $n-a-1, n-a-2, \\\\ldots, 0$ in that order.\n- Right: run $n$ monolithic steps from $S_0$, consuming step indices $n-1, n-2, \\\\ldots, 0$ in that order.\n\nNote the index bookkeeping this implies: the left side's full sequence of frame indices is $a-1,\\\\ldots,0$ followed by $n-a-1,\\\\ldots,0$ (index $0$ is consumed twice whenever $a > 0$ and $n - a > 0$, and no index $\\\\ge n-a$ is consumed by the second segment), while the right side consumes each of $n-1, \\\\ldots, 0$ exactly once.\n\nDegenerate and edge cases.\n\n- $a = 0$: the first segment is empty and $n - 0 = n$; since $\\\\operatorname{restore}(\\\\operatorname{snap}(S_0)) = S_0$, the claim becomes: $n$ tiled steps from $S_0$ equal $n$ monolithic steps from $S_0$ — the full tiled-vs-monolithic equivalence.\n- $a = n$: the continuation is empty ($n - n = 0$); the claim becomes $\\\\operatorname{restore}(\\\\operatorname{snap}(\\\\text{state after } n \\\\text{ tiled steps})) = \\\\text{state after } n \\\\text{ monolithic steps}$.\n- $n = 0$: forces $a = 0$; the claim reduces to $\\\\operatorname{restore}(\\\\operatorname{snap}(S_0)) = S_0$.\n- $T = \\\\varnothing$: every gradient is masked to $0$ before clipping, so every step (both evaluators) applies $U(S, 0)$. $T$ = all coordinates: the mask is the identity.\n- No sign or positivity assumption on $c$ or on the coefficients $\\\\alpha_{k,i}$.\n- If $I_k = \\\\varnothing$ for some $k$: every tile of $\\\\mathfrak{B}_k$ is then empty, the tiled gradient is 0 + (h\'_{k,S})^{*}(0) = 0, and the monolithic objective is the empty sum, identically $0$.\n- $d = 0$ or $m = 0$ are permitted; the corresponding vector spaces are trivial (all vectors are $0$).\n- $U$ is universally quantified with no restriction, and the hypotheses of tile-partition and certificates are demanded at every $k \\\\in \\\\mathbb{N}$ and (for certificates) every state, not merely along the run."\n}', 'startLine': 1, 'lineNumbers': [1, 2, 3]}, 'meta': {'source': {'type': 'internal', 'value': 'agent://RB2-M11'}}}}