M07 — Logical reduction and masked update

{"text": "{\n "data": "M07_masked_update_reduction. Let $d$ be an arbitrary natural number (implicit; $d = 0$ is allowed, in which case $\\\\mathbb{R}^d$ is the one-point zero space), let $c, \\\\beta_1, \\\\beta_2, \\\\eta, \\\\lambda, \\\\varepsilon$ be arbitrary real numbers \u2014 no sign or range hypotheses are imposed on any of them \u2014 and let $S = (w, m, v, t)$ be an arbitrary training state on $\\\\mathbb{R}^d$, i.e. a record with $w, m, v \\\\in \\\\mathbb{R}^d$ (the parameter vector, the first-moment vector, and the second-moment vector) and a step counter $t \\\\in \\\\mathbb{N}$. Throughout, $\\\\mathbb{R}^d$ denotes the space of real $d$-tuples indexed by $j \\\\in \\\\{0, \\\\dots, d-1\\\\}$ equipped with the Euclidean ($\\\\ell^2$) norm $\\\\|g\\\\| = \\\\bigl(\\\\sum_{j} g_j^2\\\\bigr)^{1/2}$, and $g_j$ is the $j$-th coordinate of $g$. The theorem has no hypotheses beyond these binders and asserts the conjunction of the following four statements; $c$ is used in (i)\u2013(iii), while $\\\\beta_1, \\\\beta_2, \\\\eta, \\\\lambda, \\\\varepsilon$ and the state $S$ are used only in (iv).\n\n**(i)** For every $g \\\\in \\\\mathbb{R}^d$: if $\\\\|g\\\\| \\\\le c$, then $\\\\operatorname{clip}_c(g) = g$. Here $\\\\operatorname{clip}_c$ is the global clip of a whole vector at radius $c$, defined by the two total branches\n

\\n\\\\operatorname{clip}_c(g) =\\n\\\\begin{cases}\\ng, & \\\\text{if } \\\\|g\\\\| \\\\le c, \\\\\\\\\\n\\\\dfrac{c}{\\\\|g\\\\|}\\\\, g, & \\\\text{if } \\\\|g\\\\| > c.\\n\\\\end{cases}\\n

\nWhen $c < 0$ the hypothesis $\\\\|g\\\\| \\\\le c$ is unsatisfiable (norms are nonnegative), so that instance is vacuously true; when $c \\\\ge 0$ the claim is that the clip acts as the identity on the closed ball of radius $c$ (at $c = 0$ this covers only $g = 0$).\n\n**(ii)** For the same radius $c$ (any real number): $\\\\operatorname{clip}_c(0) = 0$, where $0$ is the zero vector of $\\\\mathbb{R}^d$. Note the edge case: if $c < 0$, the zero vector fails the branch test $\\\\|0\\\\| = 0 \\\\le c$, so the assertion is that the second branch \u2014 which scales $0$ by the factor $c / \\\\|0\\\\|$, a division by the zero norm under the reals' total division \u2014 still returns the zero vector.\n\n**(iii)** For every type $\\\\sigma$ (arbitrary, possibly with no elements, in which case the inner quantification over $S'$ is vacuous), every finite set $T$ of coordinate indices (the trainable set; it may be empty or all of $\\\\{0,\\\\dots,d-1\\\\}$), every function $U : \\\\sigma \\\\to \\\\mathbb{R}^d \\\\to \\\\sigma$ (an arbitrary deterministic optimizer transition), every $S' \\\\in \\\\sigma$, and all vectors $g_1, g_2 \\\\in \\\\mathbb{R}^d$, the conditional equality\n

$$\\ng_1 = g_2 \\\\;\\\\Longrightarrow\\\\; \\\\operatorname{logicalStep}(T, c, U, S', g_1) = \\\\operatorname{logicalStep}(T, c, U, S', g_2)\\n$$

\nholds, where the logical step is the composite\n

\\n\\\\operatorname{logicalStep}(T, c, U, S', g) \\\\;:=\\\\; U\\\\bigl(S',\\\\, \\\\operatorname{clip}_c(P_T g)\\\\bigr),\\n\\\\qquad\\n(P_T g)_j =\\n\\\\begin{cases}\\ng_j, & j \\\\in T, \\\\\\\\\\n0, & j \\\\notin T,\\n\\\\end{cases}\\n

\ni.e. the gradient is first projected onto the trainable coordinates (every frozen coordinate $j \\\\notin T$ is zeroed), then globally clipped at radius $c$ by the same two-branch definition as in (i), and the map $U$ is then applied exactly once, to the fixed state $S'$ and the resulting clipped vector. The assertion is exactly that replacing the gradient argument of this composite by an equal vector leaves the $\\\\sigma$-valued result unchanged, with $T$, $c$, $U$, and $S'$ held fixed on both sides; if $T$ is empty the projection sends every $g$ to $0$.\n\n**(iv)** For every finite set $T$ of coordinate indices (again possibly empty or full) and all $g_1, g_2 \\\\in \\\\mathbb{R}^d$, the conditional equality\n

$$\\ng_1 = g_2 \\\\;\\\\Longrightarrow\\\\; \\\\operatorname{adamWStep}(\\\\beta_1, \\\\beta_2, \\\\eta, \\\\lambda, \\\\varepsilon;\\\\, T, S, g_1) = \\\\operatorname{adamWStep}(\\\\beta_1, \\\\beta_2, \\\\eta, \\\\lambda, \\\\varepsilon;\\\\, T, S, g_2)\\n$$

\nholds, where the transition returns the new training state $(w', m', v', t+1)$ defined coordinatewise by\n

$$\\nm'_j = \\\\beta_1\\\\, m_j + (1 - \\\\beta_1)\\\\, g_j,\\n\\\\qquad\\nv'_j = \\\\beta_2\\\\, v_j + (1 - \\\\beta_2)\\\\, (g_j)^2\\n\\\\qquad (\\\\text{every } j, \\\\text{ regardless of } T),\\n$$

\n

\\nw'_j =\\n\\\\begin{cases}\\n(1 - \\\\eta\\\\lambda)\\\\, w_j \\\\; - \\\\; \\\\eta \\\\cdot \\\\dfrac{\\\\,m'_j \\\\big/ \\\\bigl(1 - \\\\beta_1^{\\\\,t+1}\\\\bigr)\\\\,}{\\\\sqrt{\\\\,v'_j \\\\big/ \\\\bigl(1 - \\\\beta_2^{\\\\,t+1}\\\\bigr)\\\\,} \\\\, + \\\\, \\\\varepsilon}, & j \\\\in T, \\\\\\\\\\\\[10pt]\\nw_j, & j \\\\notin T,\\n\\\\end{cases}\\n

\ni.e. trainable coordinates receive the decoupled-weight-decay AdamW update built from the bias-corrected first and second moments, frozen coordinates of $w$ are copied through unchanged, both moment vectors are updated at every coordinate (frozen coordinates included), and the step counter is incremented by exactly one. The asserted equality is equality of the full state record \u2014 all four components ($w$, $m$, $v$, and the counter) \u2014 with $T$, the hyperparameters, and the state $S = (w, m, v, t)$ fixed on both sides and only the gradient argument replaced by the equal vector. All arithmetic is total: nothing excludes $\\\\beta_1 = 1$ or $\\\\beta_2 = 1$ (which zero the bias-correction denominators $1 - \\\\beta_i^{t+1}$), nor $\\\\varepsilon = -\\\\sqrt{\\\\,v'_j/(1-\\\\beta_2^{t+1})}$ (which zeros the update denominator), nor negative arguments under the total real square root; in those cases the divisions and square root take their total-division/total-sqrt values, and the claim above is still asserted verbatim."\n}", "details": {"resolvedPath": "/home/ajax/.omp/agent/sessions/-math/2026-09-22T19-31-08-510Z_01a0ca99-be5e-7000-93c6-dac7c74cc004/RB-M07.md", "contentType": "text/markdown", "totalLines": 3, "displayContent": {"text": "{\n "data": "M07_masked_update_reduction. Let $d$ be an arbitrary natural number (implicit; $d = 0$ is allowed, in which case $\\\\mathbb{R}^d$ is the one-point zero space), let $c, \\\\beta_1, \\\\beta_2, \\\\eta, \\\\lambda, \\\\varepsilon$ be arbitrary real numbers \u2014 no sign or range hypotheses are imposed on any of them \u2014 and let $S = (w, m, v, t)$ be an arbitrary training state on $\\\\mathbb{R}^d$, i.e. a record with $w, m, v \\\\in \\\\mathbb{R}^d$ (the parameter vector, the first-moment vector, and the second-moment vector) and a step counter $t \\\\in \\\\mathbb{N}$. Throughout, $\\\\mathbb{R}^d$ denotes the space of real $d$-tuples indexed by $j \\\\in \\\\{0, \\\\dots, d-1\\\\}$ equipped with the Euclidean ($\\\\ell^2$) norm $\\\\|g\\\\| = \\\\bigl(\\\\sum_{j} g_j^2\\\\bigr)^{1/2}$, and $g_j$ is the $j$-th coordinate of $g$. The theorem has no hypotheses beyond these binders and asserts the conjunction of the following four statements; $c$ is used in (i)\u2013(iii), while $\\\\beta_1, \\\\beta_2, \\\\eta, \\\\lambda, \\\\varepsilon$ and the state $S$ are used only in (iv).\n\n**(i)** For every $g \\\\in \\\\mathbb{R}^d$: if $\\\\|g\\\\| \\\\le c$, then $\\\\operatorname{clip}_c(g) = g$. Here $\\\\operatorname{clip}_c$ is the global clip of a whole vector at radius $c$, defined by the two total branches\n

\\n\\\\operatorname{clip}_c(g) =\\n\\\\begin{cases}\\ng, & \\\\text{if } \\\\|g\\\\| \\\\le c, \\\\\\\\\\n\\\\dfrac{c}{\\\\|g\\\\|}\\\\, g, & \\\\text{if } \\\\|g\\\\| > c.\\n\\\\end{cases}\\n

\nWhen $c < 0$ the hypothesis $\\\\|g\\\\| \\\\le c$ is unsatisfiable (norms are nonnegative), so that instance is vacuously true; when $c \\\\ge 0$ the claim is that the clip acts as the identity on the closed ball of radius $c$ (at $c = 0$ this covers only $g = 0$).\n\n**(ii)** For the same radius $c$ (any real number): $\\\\operatorname{clip}_c(0) = 0$, where $0$ is the zero vector of $\\\\mathbb{R}^d$. Note the edge case: if $c < 0$, the zero vector fails the branch test $\\\\|0\\\\| = 0 \\\\le c$, so the assertion is that the second branch \u2014 which scales $0$ by the factor $c / \\\\|0\\\\|$, a division by the zero norm under the reals' total division \u2014 still returns the zero vector.\n\n**(iii)** For every type $\\\\sigma$ (arbitrary, possibly with no elements, in which case the inner quantification over $S'$ is vacuous), every finite set $T$ of coordinate indices (the trainable set; it may be empty or all of $\\\\{0,\\\\dots,d-1\\\\}$), every function $U : \\\\sigma \\\\to \\\\mathbb{R}^d \\\\to \\\\sigma$ (an arbitrary deterministic optimizer transition), every $S' \\\\in \\\\sigma$, and all vectors $g_1, g_2 \\\\in \\\\mathbb{R}^d$, the conditional equality\n

$$\\ng_1 = g_2 \\\\;\\\\Longrightarrow\\\\; \\\\operatorname{logicalStep}(T, c, U, S', g_1) = \\\\operatorname{logicalStep}(T, c, U, S', g_2)\\n$$

\nholds, where the logical step is the composite\n

\\n\\\\operatorname{logicalStep}(T, c, U, S', g) \\\\;:=\\\\; U\\\\bigl(S',\\\\, \\\\operatorname{clip}_c(P_T g)\\\\bigr),\\n\\\\qquad\\n(P_T g)_j =\\n\\\\begin{cases}\\ng_j, & j \\\\in T, \\\\\\\\\\n0, & j \\\\notin T,\\n\\\\end{cases}\\n

\ni.e. the gradient is first projected onto the trainable coordinates (every frozen coordinate $j \\\\notin T$ is zeroed), then globally clipped at radius $c$ by the same two-branch definition as in (i), and the map $U$ is then applied exactly once, to the fixed state $S'$ and the resulting clipped vector. The assertion is exactly that replacing the gradient argument of this composite by an equal vector leaves the $\\\\sigma$-valued result unchanged, with $T$, $c$, $U$, and $S'$ held fixed on both sides; if $T$ is empty the projection sends every $g$ to $0$.\n\n**(iv)** For every finite set $T$ of coordinate indices (again possibly empty or full) and all $g_1, g_2 \\\\in \\\\mathbb{R}^d$, the conditional equality\n

$$\\ng_1 = g_2 \\\\;\\\\Longrightarrow\\\\; \\\\operatorname{adamWStep}(\\\\beta_1, \\\\beta_2, \\\\eta, \\\\lambda, \\\\varepsilon;\\\\, T, S, g_1) = \\\\operatorname{adamWStep}(\\\\beta_1, \\\\beta_2, \\\\eta, \\\\lambda, \\\\varepsilon;\\\\, T, S, g_2)\\n$$

\nholds, where the transition returns the new training state $(w', m', v', t+1)$ defined coordinatewise by\n

$$\\nm'_j = \\\\beta_1\\\\, m_j + (1 - \\\\beta_1)\\\\, g_j,\\n\\\\qquad\\nv'_j = \\\\beta_2\\\\, v_j + (1 - \\\\beta_2)\\\\, (g_j)^2\\n\\\\qquad (\\\\text{every } j, \\\\text{ regardless of } T),\\n$$

\n

\\nw'_j =\\n\\\\begin{cases}\\n(1 - \\\\eta\\\\lambda)\\\\, w_j \\\\; - \\\\; \\\\eta \\\\cdot \\\\dfrac{\\\\,m'_j \\\\big/ \\\\bigl(1 - \\\\beta_1^{\\\\,t+1}\\\\bigr)\\\\,}{\\\\sqrt{\\\\,v'_j \\\\big/ \\\\bigl(1 - \\\\beta_2^{\\\\,t+1}\\\\bigr)\\\\,} \\\\, + \\\\, \\\\varepsilon}, & j \\\\in T, \\\\\\\\\\\\[10pt]\\nw_j, & j \\\\notin T,\\n\\\\end{cases}\\n

\ni.e. trainable coordinates receive the decoupled-weight-decay AdamW update built from the bias-corrected first and second moments, frozen coordinates of $w$ are copied through unchanged, both moment vectors are updated at every coordinate (frozen coordinates included), and the step counter is incremented by exactly one. The asserted equality is equality of the full state record \u2014 all four components ($w$, $m$, $v$, and the counter) \u2014 with $T$, the hyperparameters, and the state $S = (w, m, v, t)$ fixed on both sides and only the gradient argument replaced by the equal vector. All arithmetic is total: nothing excludes $\\\\beta_1 = 1$ or $\\\\beta_2 = 1$ (which zero the bias-correction denominators $1 - \\\\beta_i^{t+1}$), nor $\\\\varepsilon = -\\\\sqrt{\\\\,v'_j/(1-\\\\beta_2^{t+1})}$ (which zeros the update denominator), nor negative arguments under the total real square root; in those cases the divisions and square root take their total-division/total-sqrt values, and the claim above is still asserted verbatim."\n}", "startLine": 1, "lineNumbers": [1, 2, 3]}, "meta": {"source": {"type": "internal", "value": "agent://RB-M07"}}}}