M09 — Trajectory equivalence

{'text': '{\n "readback": "Theorem M09_trajectory_equivalence. Fix arbitrary natural numbers $d$ and $m$, and write $W = \\\\mathbb{R}^d$ and $V = \\\\mathbb{R}^m$ for the corresponding Euclidean spaces. Fix an arbitrary type $\\\\iota$ (an index type for \"occurrences\"; it may be finite, infinite, or empty), assumed to carry decidable equality. The theorem asserts, for every choice of:\n\n- a frame schedule $\\\\xi = (\\\\xi_k)_{k \\\\in \\\\mathbb{N}}$, where each frame $\\\\xi_k$ is a quadruple $\\\\big(h_k,\\\\, f_k,\\\\, \\\\alpha_k,\\\\, I_k\\\\big)$ consisting of an arbitrary map $h_k : W \\\\to V$ (the shared computation; no regularity is part of the data), per-occurrence loss maps $f_{k,i} : W \\\\times V \\\\to \\\\mathbb{R}$, coefficients $\\\\alpha_k : \\\\iota \\\\to \\\\mathbb{R}$, and a finite occurrence set $I_k \\\\subseteq \\\\iota$;\n- a tile-partition schedule $\\\\mathfrak{B} = (\\\\mathfrak{B}_k)_{k \\\\in \\\\mathbb{N}}$, each $\\\\mathfrak{B}_k$ being a finite list of finite subsets (\"tiles\") of $\\\\iota$;\n- the hypothesis $h_{\\\\mathrm{part}}$: for every $k$, the tiles of $\\\\mathfrak{B}_k$ are pairwise disjoint and their union is exactly $I_k$ (so every tile is a subset of $I_k$; tiles may be empty, and the empty list is permitted only in that its union is $\\\\varnothing$, which forces $I_k = \\\\varnothing$);\n- the hypothesis $D_{\\\\mathrm{of}}$: for every step index $k \\\\in \\\\mathbb{N}$ and every training state $S$, a derivative-certificate bundle for the frame $\\\\xi_k$ at the point $S.w$ (its contents are listed in full below);\n- a finite set $T \\\\subseteq \\\\{0, \\\\dots, d-1\\\\}$ of \"trainable\" coordinates;\n- a real number $c$ (no sign hypothesis);\n- an arbitrary deterministic optimizer $U : \\\\text{State} \\\\to W \\\\to \\\\text{State}$;\n- an initial state $S_0$ and a step count $n \\\\in \\\\mathbb{N}$;\n\nthat\n\n

\n\nan equality of complete training states, where \"tiled\" and \"mono\" are the two transition systems defined below. Both sides use the same $\\\\xi$, $T$, $c$, $U$, $S_0$ and $n$; only the tiled side additionally depends on $\\\\mathfrak{B}$ and $D_{\\\\mathrm{of}}$.\n\nTraining states. A state $S \\\\in \\\\text{State}$ is a quadruple $(w, \\\\mu_1, \\\\mu_2, t)$ with $w, \\\\mu_1, \\\\mu_2 \\\\in \\\\mathbb{R}^d$ (logical parameters, first-moment slots, second-moment slots) and a step counter $t \\\\in \\\\mathbb{N}$. The asserted equality is equality of the entire state after $n$ steps — parameters, both moment vectors, and the counter — not just of the parameters.\n\nWhat $\\\\operatorname{runFrom}(\\\\text{step}, n, S_0)$ asserts. For a transition $\\\\operatorname{step} : \\\\text{State} \\\\to \\\\mathbb{N} \\\\to \\\\text{State}$,\n\n

\n\nUnrolling, $n$ transitions are applied, consuming the schedule index $n-1$ first and index $0$ last: $\\\\operatorname{runFrom}(\\\\operatorname{step}, n, S_0) = \\\\operatorname{step}(\\\\cdots \\\\operatorname{step}(\\\\operatorname{step}(S_0,\\\\, n-1),\\\\, n-2) \\\\cdots,\\\\, 0)$. Only the frames, partitions, and certificates at indices $0, \\\\dots, n-1$ are ever read; the hypotheses $h_{\\\\mathrm{part}}$ and $D_{\\\\mathrm{of}}$ are nonetheless demanded at every index $k \\\\in \\\\mathbb{N}$, including indices no $n$-step run reaches. At $n = 0$ both sides of the theorem are literally $S_0$, so the statement includes the degenerate case $n = 0$ in which it reduces to $S_0 = S_0$.\n\nThe two transitions. Both take a current state $S$ and a schedule index $k$, compute a gradient vector $g \\\\in \\\\mathbb{R}^d$, and return $U\\\\big(S,\\\\, \\\\operatorname{clip}_c(P_T\\\\, g)\\\\big)$ — the optimizer $U$ is applied exactly once per step, to the pre-update state $S$. Here $P_T$ is the coordinate mask $(P_T\\\\, g)_j = g_j$ if $j \\\\in T$ and $0$ otherwise, and\n\n

\n\ntaken verbatim as a total function: no sign is assumed on $c$, and division is total, so both branches are defined for every $g$ (including $g = 0$). The two transitions differ only in how $g$ is produced:\n\n- Monolithic gradient. $g = g^{\\\\mathrm{mono}}_k(S)$ is the vector representing the derivative of the logical objective\n

\nat $S.w$ — literally, the image of $1 \\\\in \\\\mathbb{R}$ under the adjoint of the Fréchet derivative $D L_k(S.w)$, i.e. its Riesz vector. The derivative operator is total: at a point where $L_k$ fails to be differentiable it is defined to be the zero map, so $g^{\\\\mathrm{mono}}_k(S) = 0$ there; the monolithic transition is thus defined for completely arbitrary frames, with no differentiability assumed.\n\n- Tiled gradient. g = g^{\\\\mathrm{tile}}_k(S) = A + (h\'_k)^{*}(C), where h\'_k is the continuous linear map supplied by the certificate bundle $D_{\\\\mathrm{of}}(k, S)$, (h\'_k)^{*} : V \\\\to W is its adjoint, and\n$$A \\;=\\; \\sum_{B \\in \\mathfrak{B}k}\\, \\sum{i \\in B} \\alpha_k(i)\\, \\mathbf{a}i \\;\\in\\; W, \\qquad C \\;=\\; \\sum{B \\in \\mathfrak{B}k}\\, \\sum{i \\in B} \\alpha_k(i)\\, \\mathbf{c}i \\;\\in\\; V,$\\n$\\mathbf{a}$and$\\mathbf{c}$being the direct/shared tables of$D{\\mathrm{of}}(k, S)$; this is computed by folding the tile list left-to-right from a zero accumulator, each tile$B$adding$\\sum_{i \\in B} \\alpha_k(i)\\,\\mathbf{a}i$to the direct slot and$\\sum{i \\in B} \\alpha_k(i)\\,\\mathbf{c}i$to the shared slot. (The fold also maintains a running loss$\\sum \\alpha_k(i)\\,\\mathrm{val}(i)$, which the tiled gradient discards: the value table — and hence its certificate — does not enter$g^{\\mathrm{tile}}k$.)\\n\\n**The certificate bundle$D{\\mathrm{of}}(k, S)$(at$w_0 = S.w$, for the frame$\\xi_k$).** The hypothesis supplies all of the following:\\n\\n- a continuous linear map$h'k : W \\to V$, certified to be the Fréchet derivative of$h_k$at$w_0$;\\n- a value table$\\mathrm{val} : \\iota \\to \\mathbb{R}$, certified by:$\\mathrm{val}(i) = f{k,i}\\big(w_0,\\, h_k(w_0)\\big)$for every occurrence$i \\in I_k$;\\n- a direct table$\\mathbf{a} : \\iota \\to W$, certified by:$\\mathbf{a}(i)$is the gradient at$w_0$of the map$w \\mapsto f{k,i}\\big(w,\\, h_k(w_0)\\big)$(shared slot frozen at its pre-update value) for every$i \\in I_k$;\\n- a shared table$\\mathbf{c} : \\iota \\to V$, certified by:$\\mathbf{c}(i)$is the gradient at$h_k(w_0)$of the map$v \\mapsto f_{k,i}(w_0, v)$for every$i \\in I_k$;\\n- differentiability of$f_{k,i}$at the point$\\big(w_0, h_k(w_0)\\big)$for every$i \\in I_k$.\\n\\n(Gradient of a real-valued function on Euclidean space$=$the vector representing its derivative.) All per-occurrence certificates are demanded only for$i \\in I_k$; if$I_k = \\varnothing$they are vacuous. The derivative certificate for$h_k$at$w_0$, however, is demanded unconditionally.\\n\\n**Fine print on the quantifiers and degenerate cases.**\\n\\n-$D_{\\mathrm{of}}$ranges over **all** states$S$, not only states reachable from$S_0$; since every$w \\in \\mathbb{R}^d$is$S.w$for some state, the hypothesis in effect requires each$h_k$to admit a Fréchet derivative at **every** point of$\\mathbb{R}^d$, and the occurrence-wise value/gradient/differentiability data to exist at every$w_0$(at the points$(w_0, h_k(w_0))$). A schedule containing a frame whose$h_k$is not everywhere differentiable makes the hypothesis unsatisfiable, and the theorem is vacuous for that schedule.\\n-$n$ranges over all of$\\mathbb{N}$including$n = 0$(both sides then equal$S_0$).\\n-$T$may be empty: then$P_T$sends every gradient to$0$, and both transitions reduce to the same map$S \\mapsto U\\big(S, \\operatorname{clip}c(0)\\big)$, identical on the two sides regardless of$\\xi$,$\\mathfrak{B}$,$D{\\mathrm{of}}$. (Likewise$d = 0$forces$T = \\varnothing$,$\\mathbb{R}^d$being the trivial space.)\\n- If$I_k = \\varnothing$for some$k$(in particular if$\\iota$is empty), then$A = 0$and$C = 0$while$L_k \\equiv 0$, so both gradient formulas yield$0$at every state for that index.\\n-$c$is an arbitrary real; for$c < 0$the branch$\\|g\\| \\le cnever applies and the second branch, with its negative scalar, is used.\\n"\n}', 'details': {'resolvedPath': '/home/ajax/.omp/agent/sessions/-math/2026-09-22T19-31-08-510Z_01a0ca99-be5e-7000-93c6-dac7c74cc004/RB2-M09.md', 'contentType': 'text/markdown', 'totalLines': 3, 'displayContent': {'text': '{\n "readback": "**Theorem `M09_trajectory_equivalence`.** Fix arbitrary natural numbersd$and$m$, and write$W = \\mathbb{R}^d$and$V = \\mathbb{R}^m$for the corresponding Euclidean spaces. Fix an arbitrary type$\\iota$(an index type for \\"occurrences\\"; it may be finite, infinite, or empty), assumed to carry decidable equality. The theorem asserts, for **every** choice of:\\n\\n- a **frame schedule**$\\xi = (\\xi_k){k \\in \\mathbb{N}}$, where each frame$\\xi_k$is a quadruple$\\big(h_k,\\, f_k,\\, \\alpha_k,\\, I_k\\big)$consisting of an arbitrary map$h_k : W \\to V$(the shared computation; no regularity is part of the data), per-occurrence loss maps$f{k,i} : W \\times V \\to \\mathbb{R}$, coefficients$\\alpha_k : \\iota \\to \\mathbb{R}$, and a finite occurrence set$I_k \\subseteq \\iota$;\\n- a **tile-partition schedule**$\\mathfrak{B} = (\\mathfrak{B}k){k \\in \\mathbb{N}}$, each$\\mathfrak{B}k$being a finite list of finite subsets (\\"tiles\\") of$\\iota$;\\n- the hypothesis$h{\\mathrm{part}}$: for **every**$k$, the tiles of$\\mathfrak{B}k$are pairwise disjoint and their union is exactly$I_k$(so every tile is a subset of$I_k$; tiles may be empty, and the empty list is permitted only in that its union is$\\varnothing$, which forces$I_k = \\varnothing$);\\n- the hypothesis$D{\\mathrm{of}}$: for **every** step index$k \\in \\mathbb{N}$and **every** training state$S$, a derivative-certificate bundle for the frame$\\xi_k$at the point$S.w$(its contents are listed in full below);\\n- a finite set$T \\subseteq \\{0, \\dots, d-1\\}$of \\"trainable\\" coordinates;\\n- a real number$c$(no sign hypothesis);\\n- an arbitrary deterministic optimizer$U : \\text{State} \\to W \\to \\text{State}$;\\n- an initial state$S_0$and a step count$n \\in \\mathbb{N}$;\n\nthat\n\n

\n\nan equality of complete training states, where \"tiled\" and \"mono\" are the two transition systems defined below. Both sides use the same $\\\\xi$, $T$, $c$, $U$, $S_0$ and $n$; only the tiled side additionally depends on $\\\\mathfrak{B}$ and $D_{\\\\mathrm{of}}$.\n\nTraining states. A state $S \\\\in \\\\text{State}$ is a quadruple $(w, \\\\mu_1, \\\\mu_2, t)$ with $w, \\\\mu_1, \\\\mu_2 \\\\in \\\\mathbb{R}^d$ (logical parameters, first-moment slots, second-moment slots) and a step counter $t \\\\in \\\\mathbb{N}$. The asserted equality is equality of the entire state after $n$ steps — parameters, both moment vectors, and the counter — not just of the parameters.\n\nWhat $\\\\operatorname{runFrom}(\\\\text{step}, n, S_0)$ asserts. For a transition $\\\\operatorname{step} : \\\\text{State} \\\\to \\\\mathbb{N} \\\\to \\\\text{State}$,\n\n

\n\nUnrolling, $n$ transitions are applied, consuming the schedule index $n-1$ first and index $0$ last: $\\\\operatorname{runFrom}(\\\\operatorname{step}, n, S_0) = \\\\operatorname{step}(\\\\cdots \\\\operatorname{step}(\\\\operatorname{step}(S_0,\\\\, n-1),\\\\, n-2) \\\\cdots,\\\\, 0)$. Only the frames, partitions, and certificates at indices $0, \\\\dots, n-1$ are ever read; the hypotheses $h_{\\\\mathrm{part}}$ and $D_{\\\\mathrm{of}}$ are nonetheless demanded at every index $k \\\\in \\\\mathbb{N}$, including indices no $n$-step run reaches. At $n = 0$ both sides of the theorem are literally $S_0$, so the statement includes the degenerate case $n = 0$ in which it reduces to $S_0 = S_0$.\n\nThe two transitions. Both take a current state $S$ and a schedule index $k$, compute a gradient vector $g \\\\in \\\\mathbb{R}^d$, and return $U\\\\big(S,\\\\, \\\\operatorname{clip}_c(P_T\\\\, g)\\\\big)$ — the optimizer $U$ is applied exactly once per step, to the pre-update state $S$. Here $P_T$ is the coordinate mask $(P_T\\\\, g)_j = g_j$ if $j \\\\in T$ and $0$ otherwise, and\n\n

\n\ntaken verbatim as a total function: no sign is assumed on $c$, and division is total, so both branches are defined for every $g$ (including $g = 0$). The two transitions differ only in how $g$ is produced:\n\n- Monolithic gradient. $g = g^{\\\\mathrm{mono}}_k(S)$ is the vector representing the derivative of the logical objective\n

\nat $S.w$ — literally, the image of $1 \\\\in \\\\mathbb{R}$ under the adjoint of the Fréchet derivative $D L_k(S.w)$, i.e. its Riesz vector. The derivative operator is total: at a point where $L_k$ fails to be differentiable it is defined to be the zero map, so $g^{\\\\mathrm{mono}}_k(S) = 0$ there; the monolithic transition is thus defined for completely arbitrary frames, with no differentiability assumed.\n\n- Tiled gradient. g = g^{\\\\mathrm{tile}}_k(S) = A + (h\'_k)^{*}(C), where h\'_k is the continuous linear map supplied by the certificate bundle $D_{\\\\mathrm{of}}(k, S)$, (h\'_k)^{*} : V \\\\to W is its adjoint, and\n$$A \\;=\\; \\sum_{B \\in \\mathfrak{B}k}\\, \\sum{i \\in B} \\alpha_k(i)\\, \\mathbf{a}i \\;\\in\\; W, \\qquad C \\;=\\; \\sum{B \\in \\mathfrak{B}k}\\, \\sum{i \\in B} \\alpha_k(i)\\, \\mathbf{c}i \\;\\in\\; V,$\\n$\\mathbf{a}$and$\\mathbf{c}$being the direct/shared tables of$D{\\mathrm{of}}(k, S)$; this is computed by folding the tile list left-to-right from a zero accumulator, each tile$B$adding$\\sum_{i \\in B} \\alpha_k(i)\\,\\mathbf{a}i$to the direct slot and$\\sum{i \\in B} \\alpha_k(i)\\,\\mathbf{c}i$to the shared slot. (The fold also maintains a running loss$\\sum \\alpha_k(i)\\,\\mathrm{val}(i)$, which the tiled gradient discards: the value table — and hence its certificate — does not enter$g^{\\mathrm{tile}}k$.)\\n\\n**The certificate bundle$D{\\mathrm{of}}(k, S)$(at$w_0 = S.w$, for the frame$\\xi_k$).** The hypothesis supplies all of the following:\\n\\n- a continuous linear map$h'k : W \\to V$, certified to be the Fréchet derivative of$h_k$at$w_0$;\\n- a value table$\\mathrm{val} : \\iota \\to \\mathbb{R}$, certified by:$\\mathrm{val}(i) = f{k,i}\\big(w_0,\\, h_k(w_0)\\big)$for every occurrence$i \\in I_k$;\\n- a direct table$\\mathbf{a} : \\iota \\to W$, certified by:$\\mathbf{a}(i)$is the gradient at$w_0$of the map$w \\mapsto f{k,i}\\big(w,\\, h_k(w_0)\\big)$(shared slot frozen at its pre-update value) for every$i \\in I_k$;\\n- a shared table$\\mathbf{c} : \\iota \\to V$, certified by:$\\mathbf{c}(i)$is the gradient at$h_k(w_0)$of the map$v \\mapsto f_{k,i}(w_0, v)$for every$i \\in I_k$;\\n- differentiability of$f_{k,i}$at the point$\\big(w_0, h_k(w_0)\\big)$for every$i \\in I_k$.\\n\\n(Gradient of a real-valued function on Euclidean space$=$the vector representing its derivative.) All per-occurrence certificates are demanded only for$i \\in I_k$; if$I_k = \\varnothing$they are vacuous. The derivative certificate for$h_k$at$w_0$, however, is demanded unconditionally.\\n\\n**Fine print on the quantifiers and degenerate cases.**\\n\\n-$D_{\\mathrm{of}}$ranges over **all** states$S$, not only states reachable from$S_0$; since every$w \\in \\mathbb{R}^d$is$S.w$for some state, the hypothesis in effect requires each$h_k$to admit a Fréchet derivative at **every** point of$\\mathbb{R}^d$, and the occurrence-wise value/gradient/differentiability data to exist at every$w_0$(at the points$(w_0, h_k(w_0))$). A schedule containing a frame whose$h_k$is not everywhere differentiable makes the hypothesis unsatisfiable, and the theorem is vacuous for that schedule.\\n-$n$ranges over all of$\\mathbb{N}$including$n = 0$(both sides then equal$S_0$).\\n-$T$may be empty: then$P_T$sends every gradient to$0$, and both transitions reduce to the same map$S \\mapsto U\\big(S, \\operatorname{clip}c(0)\\big)$, identical on the two sides regardless of$\\xi$,$\\mathfrak{B}$,$D{\\mathrm{of}}$. (Likewise$d = 0$forces$T = \\varnothing$,$\\mathbb{R}^d$being the trivial space.)\\n- If$I_k = \\varnothing$for some$k$(in particular if$\\iota$is empty), then$A = 0$and$C = 0$while$L_k \\equiv 0$, so both gradient formulas yield$0$at every state for that index.\\n-$c$is an arbitrary real; for$c < 0$the branch$\\|g\\| \\le c$ never applies and the second branch, with its negative scalar, is used.\n"\n}', 'startLine': 1, 'lineNumbers': [1, 2, 3]}, 'meta': {'source': {'type': 'internal', 'value': 'agent://RB2-M09'}}}}