M06 — Frozen-input differentiation

Proved

VathekProof.M06_frozen_input_gradient

by ajax · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

formal-verificationgradient-descentmachine-learning

Two facts about frozen components.

(i) The chain derivative through a frozen component's input survives. Take the concrete graft of the source: a trainable bridge $w \mapsto 3w$ grafted into a frozen donor $u \mapsto 2u$ , with loss $\tfrac{1}{2}\|u - 1\|^2$ evaluated at $w_0 = 2$ . The composite $w \mapsto \tfrac{1}{2}\|2 \cdot (3w) - 1\|^2 = \tfrac{1}{2}(6w - 1)^2$ has gradient $6(6 \cdot 2 - 1) = 66 \neq 0$ at $w_0$ : freezing the donor's parameters does not remove the derivative through its input (detaching that input would falsely give $0$ ).

(ii) The declared masked update preserves frozen coordinates. For the masked AdamW instance with $0 \le \beta_1, \beta_2 < 1$ , $\varepsilon > 0$ , and nonnegative incoming second moments: every frozen coordinate ( $j \notin T$ ) of $w$ is unchanged by the update, second moments stay nonnegative, and the update denominator $\sqrt{\hat v_j} + \varepsilon$ is strictly positive — properties of this declared masked update, not of an arbitrary update function.

Preamble

import Definitions.Def_VathekFrame
import Definitions.Def_VathekState
import Definitions.Def_VathekAdamW
import Definitions.Def_VathekWitness

Formal statement

namespace VathekProof

/-- **M06 — Frozen-input differentiation.**  (i) The §5.3 chain instance: a trainable
bridge `w ↦ 3w` grafted into a *frozen* donor `u ↦ 2u`, with loss `½‖u - 1‖²` at
`w₀ = 2`, has the nonzero gradient `66` — freezing the donor's parameters does not
remove the chain derivative through its input (detaching that input would instead
falsely give `0`).  (ii) For the declared masked AdamW update: frozen coordinates are
preserved untouched, nonnegative second moments stay nonnegative, and the update
denominator `√v̂ + ε` is strictly positive — properties of this declared masked
update, not of an arbitrary update function. -/
theorem M06_frozen_input_gradient :
    HasGradientAt
      (fun (w : EuclideanSpace ℝ (Fin 1)) =>
        (1 / 2) * ‖(2 : ℝ) • ((3 : ℝ) • w) - WithLp.toLp 2 (fun _ => (1 : ℝ))‖ ^ 2)
      (WithLp.toLp 2 (fun _ => (66 : ℝ)))
      (WithLp.toLp 2 (fun _ => (2 : ℝ)))
    ∧ (WithLp.toLp 2 (fun _ => (66 : ℝ)) : EuclideanSpace ℝ (Fin 1)) ≠ 0
    ∧ ∀ (d : ℕ) (β₁ β₂ η lam ε : ℝ) (T : Finset (Fin d)) (S : TrainState d)
        (g : EuclideanSpace ℝ (Fin d)),
        0 ≤ β₁ → β₁ < 1 → 0 ≤ β₂ → β₂ < 1 → 0 < ε → (∀ j, 0 ≤ S.mom2 j) →
        (∀ j ∉ T, (adamWStep β₁ β₂ η lam ε T S g).w j = S.w j)
        ∧ (∀ j, 0 ≤ (adamWStep β₁ β₂ η lam ε T S g).mom2 j)
        ∧ ∀ j, 0 < Real.sqrt (adamM2 β₂ S g j / (1 - β₂ ^ (S.t + 1))) + ε := by sorry

end VathekProof

Source

Vathek Graft: A Proof and Evidence Programme, mission-source white paper v1.0, 22 September 2026 (Thomas Davis). Section 5.3 (witness), Section 6 milestone M06, and Appendix A.

Read-back

What the Lean code literally says, in plain math · glm-5.3 (independent auditor subagent)

{"text": "{\n "readback": "The theorem M06_frozen_input_gradient asserts a conjunction of three statements.\n\nFirst conjunct \u2014 the concrete gradient claim. Let $W = \\\\mathrm{EuclideanSpace}\\\\ \\\\mathbb{R}\\\\ (\\\\mathrm{Fin}\\\\ 1)$ , the one-coordinate Euclidean space (vectors are written via the identification $\\\\mathrm{WithLp.toLp}\\\\ 2$ , which packages a coordinate function as an $L^2$ -typed vector; e.g. $\\\\mathrm{WithLp.toLp}\\\\ 2\\\\ (\\\\lambda \\\\_ \\\\mapsto 2)$ is the constant vector $w_0 = (2)$ ). The claim is that the function\n\n

F(w) = \\\\tfrac{1}{2}\\\\,\\\\bigl\\\\|\\\\, 2 \\\\cdot (3w) - \\\\mathbf{1} \\\\,\\\\bigr\\\\|^2,

\n\nwhere $\\\\|\\\\cdot\\\\|$ is the Euclidean norm on the one-coordinate space and $\\\\mathbf{1} = (1)$ is the constant vector $1$ , has gradient at the point $w_0 = (2)$ equal to the constant vector $(66)$ . Here HasGradientAt is the standard Fr\u00e9chet-gradient notion: $F(w) = F(w_0) + \\\\langle (66),\\\\, w - w_0\\\\rangle + o(\\\\|w - w_0\\\\|)$ as $w \\\\to w_0$ . Concretely $F(w) = \\\\tfrac12(6w - 1)^2$ on the single coordinate, so the assertion is the literal numerical statement $\\\\nabla F(2) = 66$ . Note that $2\\\\cdot(3w)$ is the composition of scaling by $3$ with scaling by $2$ (i.e. $6w$ ); the norm and squaring are the Euclidean ones.\n\nSecond conjunct \u2014 nonzeroness. The constant vector $(66) \\\\in \\\\mathrm{EuclideanSpace}\\\\ \\\\mathbb{R}\\\\ (\\\\mathrm{Fin}\\\\ 1)$ is not the zero vector. This is a bare inequality; combined with the first conjunct it says the gradient in question is nonzero, but the conjunct itself asserts only $(66) \\\\neq 0$ .\n\nThird conjunct \u2014 the universally quantified AdamW clause. For every natural number $d$ , real numbers $\\\\beta_1, \\\\beta_2, \\\\eta, \\\\lambda, \\\\varepsilon$ , finite set $T \\\\subseteq \\\\mathrm{Fin}\\\\ d$ of trainable coordinates, training state $S$ , and gradient vector $g \\\\in \\\\mathrm{EuclideanSpace}\\\\ \\\\mathbb{R}\\\\ (\\\\mathrm{Fin}\\\\ d)$ , assuming:\n\n- $0 \\\\le \\\\beta_1$ and $\\\\beta_1 < 1$ ;\n- $0 \\\\le \\\\beta_2$ and $\\\\beta_2 < 1$ ;\n- $0 < \\\\varepsilon$ ;\n- every second-moment slot of $S$ is nonnegative: $0 \\\\le S_{\\\\mathrm{mom2}}(j)$ for all coordinates $j$ ;\n\nit concludes all three of the following about the state $S' = \\\\mathrm{adamWStep}\\\\ \\\\beta_1\\\\ \\\\beta_2\\\\ \\\\eta\\\\ \\\\lambda\\\\ \\\\varepsilon\\\\ T\\\\ S\\\\ g$ , where the masked AdamW transition is defined coordinatewise by\n\n

\\nm'_j &= \\\\beta_1\\\\, S_{\\\\mathrm{mom1}}(j) + (1 - \\\\beta_1)\\\\, g_j &&\\\\text{(first moment, } \\\\mathrm{adamM1}\\\\text{)},\\\\\\\\\\nv'_j &= \\\\beta_2\\\\, S_{\\\\mathrm{mom2}}(j) + (1 - \\\\beta_2)\\\\, g_j^2 &&\\\\text{(second moment, } \\\\mathrm{adamM2}\\\\text{)},\\\\\\\\\\nS'_w(j) &= \\\\begin{cases}\\n(1 - \\\\eta\\\\lambda)\\\\, S_w(j) \\\\;-\\\\; \\\\eta\\\\,\\\\dfrac{m'_j / (1 - \\\\beta_1^{\\\\,S_t + 1})}{\\\\sqrt{v'_j / (1 - \\\\beta_2^{\\\\,S_t + 1})} + \\\\varepsilon}, & j \\\\in T,\\\\\\\\[2ex]\\nS_w(j), & j \\\\notin T,\\n\\\\end{cases}\\\\\\\\\\nS'_t &= S_t + 1,\\n

\n\nwith $S_w, S_{\\\\mathrm{mom1}}, S_{\\\\mathrm{mom2}}$ the parameter, first-moment, and second-moment vectors of $S$ and $S_t \\\\in \\\\mathbb{N}$ its step counter:\n\n1. Frozen coordinates preserved: for every coordinate $j \\\\notin T$ , the updated parameter equals the old one, $S'_w(j) = S_w(j)$ ;\n2. Second moments stay nonnegative: $0 \\\\le S'_{\\\\mathrm{mom2}}(j) = v'_j$ for every $j$ ;\n3. Denominator positivity: for every $j$ , $0 < \\\\sqrt{\\\\,v'_j / (1 - \\\\beta_2^{\\\\,S_t + 1})} + \\\\varepsilon$ , where the square root is the real square root.\n\nEdge cases and fine print. The hypotheses $0 \\\\le \\\\beta_1 < 1$ and $0 \\\\le \\\\beta_2 < 1$ make the bias-correction denominators $1 - \\\\beta_1^{S_t+1}$ and $1 - \\\\beta_2^{S_t+1}$ positive (so no division by zero there), and together with $0 \\\\le S_{\\\\mathrm{mom2}}(j)$ they make $v'_j \\\\ge 0$ ; the third conclusion's strict positivity then rests on $\\\\varepsilon > 0$ (it forces the denominator strictly positive even when $v'_j = 0$ ). No sign or size restrictions are placed on $\\\\eta$ or $\\\\lambda$ (the learning rate and weight-decay coefficient appear only in the trainable-branch formula and are otherwise unconstrained), nor on $g$ or $S_{\\\\mathrm{mom1}}$ . The quantification includes the degenerate cases $d = 0$ (empty coordinate set, all three conclusions vacuous coordinatewise) and $T$ empty (then conclusion 1 says all coordinates of $w$ are unchanged) or $T$ full. No conclusion is drawn about the trainable-branch coordinates of $S'_w$ , about $S'_{\\\\mathrm{mom1}}$ , or about the step counter beyond its increment as part of the definition. Conclusion 3 concerns the same denominator expression used inside the trainable branch of the update, with $v'_j$ computed from the pre-update state $S$ ."\n}", "details": {"resolvedPath": "/home/ajax/.omp/agent/sessions/-math/2026-09-22T19-31-08-510Z_01a0ca99-be5e-7000-93c6-dac7c74cc004/RB-M06.md", "contentType": "text/markdown", "totalLines": 3, "displayContent": {"text": "{\n "readback": "The theorem M06_frozen_input_gradient asserts a conjunction of three statements.\n\nFirst conjunct \u2014 the concrete gradient claim. Let $W = \\\\mathrm{EuclideanSpace}\\\\ \\\\mathbb{R}\\\\ (\\\\mathrm{Fin}\\\\ 1)$ , the one-coordinate Euclidean space (vectors are written via the identification $\\\\mathrm{WithLp.toLp}\\\\ 2$ , which packages a coordinate function as an $L^2$ -typed vector; e.g. $\\\\mathrm{WithLp.toLp}\\\\ 2\\\\ (\\\\lambda \\\\_ \\\\mapsto 2)$ is the constant vector $w_0 = (2)$ ). The claim is that the function\n\n

F(w) = \\\\tfrac{1}{2}\\\\,\\\\bigl\\\\|\\\\, 2 \\\\cdot (3w) - \\\\mathbf{1} \\\\,\\\\bigr\\\\|^2,

\\nm'_j &= \\\\beta_1\\\\, S_{\\\\mathrm{mom1}}(j) + (1 - \\\\beta_1)\\\\, g_j &&\\\\text{(first moment, } \\\\mathrm{adamM1}\\\\text{)},\\\\\\\\\\nv'_j &= \\\\beta_2\\\\, S_{\\\\mathrm{mom2}}(j) + (1 - \\\\beta_2)\\\\, g_j^2 &&\\\\text{(second moment, } \\\\mathrm{adamM2}\\\\text{)},\\\\\\\\\\nS'_w(j) &= \\\\begin{cases}\\n(1 - \\\\eta\\\\lambda)\\\\, S_w(j) \\\\;-\\\\; \\\\eta\\\\,\\\\dfrac{m'_j / (1 - \\\\beta_1^{\\\\,S_t + 1})}{\\\\sqrt{v'_j / (1 - \\\\beta_2^{\\\\,S_t + 1})} + \\\\varepsilon}, & j \\\\in T,\\\\\\\\[2ex]\\nS_w(j), & j \\\\notin T,\\n\\\\end{cases}\\\\\\\\\\nS'_t &= S_t + 1,\\n

\n\nwith $S_w, S_{\\\\mathrm{mom1}}, S_{\\\\mathrm{mom2}}$ the parameter, first-moment, and second-moment vectors of $S$ and $S_t \\\\in \\\\mathbb{N}$ its step counter:\n\n1. Frozen coordinates preserved: for every coordinate $j \\\\notin T$ , the updated parameter equals the old one, $S'_w(j) = S_w(j)$ ;\n2. Second moments stay nonnegative: $0 \\\\le S'_{\\\\mathrm{mom2}}(j) = v'_j$ for every $j$ ;\n3. Denominator positivity: for every $j$ , $0 < \\\\sqrt{\\\\,v'_j / (1 - \\\\beta_2^{\\\\,S_t + 1})} + \\\\varepsilon$ , where the square root is the real square root.\n\nEdge cases and fine print. The hypotheses $0 \\\\le \\\\beta_1 < 1$ and $0 \\\\le \\\\beta_2 < 1$ make the bias-correction denominators $1 - \\\\beta_1^{S_t+1}$ and $1 - \\\\beta_2^{S_t+1}$ positive (so no division by zero there), and together with $0 \\\\le S_{\\\\mathrm{mom2}}(j)$ they make $v'_j \\\\ge 0$ ; the third conclusion's strict positivity then rests on $\\\\varepsilon > 0$ (it forces the denominator strictly positive even when $v'_j = 0$ ). No sign or size restrictions are placed on $\\\\eta$ or $\\\\lambda$ (the learning rate and weight-decay coefficient appear only in the trainable-branch formula and are otherwise unconstrained), nor on $g$ or $S_{\\\\mathrm{mom1}}$ . The quantification includes the degenerate cases $d = 0$ (empty coordinate set, all three conclusions vacuous coordinatewise) and $T$ empty (then conclusion 1 says all coordinates of $w$ are unchanged) or $T$ full. No conclusion is drawn about the trainable-branch coordinates of $S'_w$ , about $S'_{\\\\mathrm{mom1}}$ , or about the step counter beyond its increment as part of the definition. Conclusion 3 concerns the same denominator expression used inside the trainable branch of the update, with $v'_j$ computed from the pre-update state $S$ ."\n}", "startLine": 1, "lineNumbers": [1, 2, 3]}, "meta": {"source": {"type": "internal", "value": "agent://RB-M06"}}}}

Human review

Endorsed by Shuze Chen · Sep 25, 2026
Endorsed by ajax · Sep 25, 2026
Confirmed by the mission captain (proposal self-audit).

View graph