M08 — One-step equivalence
ProvedVathekProof.M08_one_step_equivalenceThe mathematical centre of the mission. Fix one frame (shared map , occurrence losses , coefficients , occurrence set ), a valid tile partition , and a genuine derivative-certificate package at the pre-update point . Then, for the tiled evaluator in which every tile reads the same :
- the tiled loss equals the monolithic loss, ;
- the tiled gradient equals the monolithic gradient
monoGradand genuinely is the gradient of the logical objective at ; and - the two evaluators therefore perform the same masked, clipped, single optimizer transition.
The hypothesis set is exactly the source's: genuine partial derivatives (certificates, not an oracle), one shared pre-update point, one deterministic optimizer. Nothing here assumes the tiled gradient is already correct — that equality is the conclusion, via the chain rule (M03) and linearity of the reverse pass (M04).
import Definitions.Def_VathekFrame import Definitions.Def_VathekState import Definitions.Def_VathekAdamW import Definitions.Def_VathekWitness
namespace VathekProof
/-- **M08 — One-step equivalence** (white paper Eq. (5)). For one frame with a valid
tile partition, where every tile reads the same pre-update point `w₀` and the
per-occurrence derivative data is certified genuine: the tiled loss equals the
monolithic loss, the tiled gradient (accumulated direct contributions plus one reverse
pass of the summed shared cotangents) equals the monolithic gradient, and the two
evaluators therefore perform the same masked, clipped, single optimizer transition. -/
theorem M08_one_step_equivalence {d m : ℕ} {ι : Type*} [DecidableEq ι] (ξ : Frame d m ι)
(ℬ : List (Finset ι)) (hpart : IsTilePartition ξ.I ℬ)
(w₀ : EuclideanSpace ℝ (Fin d)) (D : FrameDeriv d m ι ξ w₀)
(T : Finset (Fin d)) (c : ℝ)
(U : TrainState d → EuclideanSpace ℝ (Fin d) → TrainState d)
(S : TrainState d) :
(tileAccum ξ.α D.val D.direct D.shared ℬ).loss = frameLoss ξ.h ξ.f ξ.α ξ.I w₀
∧ tiledGrad ξ.α D.val D.direct D.shared D.h' ℬ = monoGrad ξ w₀
∧ HasGradientAt (frameLoss ξ.h ξ.f ξ.α ξ.I)
(tiledGrad ξ.α D.val D.direct D.shared D.h' ℬ) w₀
∧ U S (clipVec c (coordMask T (tiledGrad ξ.α D.val D.direct D.shared D.h' ℬ)))
= U S (clipVec c (coordMask T (monoGrad ξ w₀))) := by sorry
end VathekProofRead-back
What the Lean code literally says, in plain math · glm-5.3 (independent auditor subagent)
{'text': '{\n "readback": "M08_one_step_equivalence — For all natural numbers and , and every index type equipped with decidable equality (a purely computational assumption needed for the finite-set operations below; it carries no mathematical content), write and for the Euclidean spaces of logical parameters and shared state (standard inner product and norm ; coordinates indexed by and ; or gives the trivial one-point vector space).\n\nHypotheses (everything the theorem takes as given).\n\n- A frame : an arbitrary map (the shared computation); a family of loss maps for ; real reduction coefficients (no sign condition is imposed); and a finite occurrence set . The frame structure itself imposes no smoothness on or the .\n- A finite list of tiles , each a finite subset of , satisfying the partition hypothesis: exactly, and tiles at distinct positions are pairwise disjoint (). The list may be empty — which forces — and individual tiles may be empty (two empty tiles are disjoint, so empty tiles may even repeat).\n- A pre-update point and a certificate package at with nine fields:\n - a continuous linear map h\' : W \\\\to V, certified to be the Fréchet derivative of at ;\n - a value table , certified by for every ;\n - a direct-gradient table , certified so that is the gradient (Fréchet derivative, represented as a vector via the inner product) of the frozen-shared-state map at , for every ;\n - a shared-cotangent table , certified so that is the gradient of the frozen-parameter map at the point , for every ;\n - a certificate that each is differentiable at the pair , for every .\n\n For the three tables are completely unconstrained; since the tiles cover exactly , only indices of ever enter the sums below.\n- A finite set of trainable coordinates (possibly empty).\n- A real clipping radius (arbitrary — possibly zero or negative).\n- An arbitrary optimizer map turning a training state and an update vector into a new training state, where a training state is a -tuple : current parameters , two moment vectors , and a step counter . And an arbitrary such state .\n\nDefinitions appearing in the conclusion.\n\nThe monolithic loss of the frame is L_\\\\xi(w) = \\\\sum_{i \\\\in I} \\\\alpha_i\\\\, f_i\\\\big(w, h(w)\\\\big), a finite real sum.\n\nThe tiled accumulator processes the tiles of left to right starting from ; over a tile it adds to its loss slot, to its direct slot (a vector of ), and to its shared slot (a vector of ). Write and for the final direct and shared slots:\n
\n\nThe tiled gradient is , where is the adjoint of the certified derivative h\', i.e. the unique continuous linear map with .\n\nThe monolithic gradient is\n
g_{\\\\mathrm{mono}} \\\\;=\\\\; \\\\big(D L_\\\\xi(w_0)\\\\big)^*[\\\\mathbf{1}],\nthe inner-product representative of the Fréchet derivative of L_\\\\xi at : take that derivative (a continuous linear functional on ), form its adjoint (a map ), and evaluate at . This is a total definition — where L_\\\\xi fails to be differentiable the derivative operator is defined to be the zero map, so always denotes some vector (then the junk value ).\n\nThe coordinate mask and global clip are\n
(P_T g)_j = \\\\begin{cases} g_j & j \\\\in T,\\\\\\\\ 0 & j \\\\notin T,\\\\end{cases} \\\\qquad \\\\operatorname{clip}_c(g) = \\\\begin{cases} g & \\\\text{if } \\\\|g\\\\| \\\\le c,\\\\\\\\[2pt] \\\\dfrac{c}{\\\\|g\\\\|}\\\\, g & \\\\text{otherwise},\\\\end{cases}\nwith the Euclidean norm; real division is total with the convention .\n\nThe assertion is the conjunction of four statements.\n\n1. (Equal losses.) The tiled accumulator's final loss slot equals the monolithic loss at :\n
\nThe left side is built from the certified value table; the right side from the actual function values.\n\n2. (Equal gradients.) The tiled gradient equals the monolithic gradient:\n
A + (h\')^*[C] \\\\;=\\\\; \\\\big(D L_\\\\xi(w_0)\\\\big)^*[\\\\mathbf{1}].\n\n3. (Genuine differentiability.) The monolithic loss map is Fréchet-differentiable at with gradient vector exactly : its derivative at exists and is the functional .\n\n4. (Same optimizer transition.)\n
\ni.e. running the optimizer once on the state with the tile-accumulated gradient — first projected onto the trainable coordinates (per-coordinate zeroing of ), then clipped once globally by the single radius — produces the same next training state (parameters, both moment slots, and step counter alike) as running it with the monolithic gradient treated identically.\n\nWhat the quantifiers silently include. No nonnegativity is assumed anywhere: the weights may be negative or zero, and the radius may be zero or negative. For the test fails for every (norms are ), so the second clip branch is always taken: nonzero vectors are rescaled by the negative factor (length , direction reversed), and even goes through that branch, giving under the division convention; for the clip is the usual radial projection onto the closed ball of radius . Degenerate instances are all covered: or (trivial spaces), (then every tile is empty, all sums are empty, both losses are , and ), the empty tile list (forcing ), and (then for every , so both sides of clause 4 become ). The optimizer is an arbitrary function of state and update vector, with no further assumptions. The hypotheses are jointly satisfiable in non-degenerate ways (e.g. smooth and with and the tables set to the genuine values), so nothing here is vacuous."\n}', 'details': {'resolvedPath': '/home/ajax/.omp/agent/sessions/-math/2026-09-22T19-31-08-510Z_01a0ca99-be5e-7000-93c6-dac7c74cc004/RB2-M08.md', 'contentType': 'text/markdown', 'totalLines': 3, 'displayContent': {'text': '{\n "readback": "M08_one_step_equivalence — For all natural numbers and , and every index type equipped with decidable equality (a purely computational assumption needed for the finite-set operations below; it carries no mathematical content), write and for the Euclidean spaces of logical parameters and shared state (standard inner product and norm ; coordinates indexed by and ; or gives the trivial one-point vector space).\n\nHypotheses (everything the theorem takes as given).\n\n- A frame : an arbitrary map (the shared computation); a family of loss maps for ; real reduction coefficients (no sign condition is imposed); and a finite occurrence set . The frame structure itself imposes no smoothness on or the .\n- A finite list of tiles , each a finite subset of , satisfying the partition hypothesis: exactly, and tiles at distinct positions are pairwise disjoint (). The list may be empty — which forces — and individual tiles may be empty (two empty tiles are disjoint, so empty tiles may even repeat).\n- A pre-update point and a certificate package at with nine fields:\n - a continuous linear map h\' : W \\\\to V, certified to be the Fréchet derivative of at ;\n - a value table , certified by for every ;\n - a direct-gradient table , certified so that is the gradient (Fréchet derivative, represented as a vector via the inner product) of the frozen-shared-state map at , for every ;\n - a shared-cotangent table , certified so that is the gradient of the frozen-parameter map at the point , for every ;\n - a certificate that each is differentiable at the pair , for every .\n\n For the three tables are completely unconstrained; since the tiles cover exactly , only indices of ever enter the sums below.\n- A finite set of trainable coordinates (possibly empty).\n- A real clipping radius (arbitrary — possibly zero or negative).\n- An arbitrary optimizer map turning a training state and an update vector into a new training state, where a training state is a -tuple : current parameters , two moment vectors , and a step counter . And an arbitrary such state .\n\nDefinitions appearing in the conclusion.\n\nThe monolithic loss of the frame is L_\\\\xi(w) = \\\\sum_{i \\\\in I} \\\\alpha_i\\\\, f_i\\\\big(w, h(w)\\\\big), a finite real sum.\n\nThe tiled accumulator processes the tiles of left to right starting from ; over a tile it adds to its loss slot, to its direct slot (a vector of ), and to its shared slot (a vector of ). Write and for the final direct and shared slots:\n
\n\nThe tiled gradient is , where is the adjoint of the certified derivative h\', i.e. the unique continuous linear map with .\n\nThe monolithic gradient is\n
g_{\\\\mathrm{mono}} \\\\;=\\\\; \\\\big(D L_\\\\xi(w_0)\\\\big)^*[\\\\mathbf{1}],\nthe inner-product representative of the Fréchet derivative of L_\\\\xi at : take that derivative (a continuous linear functional on ), form its adjoint (a map ), and evaluate at . This is a total definition — where L_\\\\xi fails to be differentiable the derivative operator is defined to be the zero map, so always denotes some vector (then the junk value ).\n\nThe coordinate mask and global clip are\n
(P_T g)_j = \\\\begin{cases} g_j & j \\\\in T,\\\\\\\\ 0 & j \\\\notin T,\\\\end{cases} \\\\qquad \\\\operatorname{clip}_c(g) = \\\\begin{cases} g & \\\\text{if } \\\\|g\\\\| \\\\le c,\\\\\\\\[2pt] \\\\dfrac{c}{\\\\|g\\\\|}\\\\, g & \\\\text{otherwise},\\\\end{cases}\nwith the Euclidean norm; real division is total with the convention .\n\nThe assertion is the conjunction of four statements.\n\n1. (Equal losses.) The tiled accumulator's final loss slot equals the monolithic loss at :\n
\nThe left side is built from the certified value table; the right side from the actual function values.\n\n2. (Equal gradients.) The tiled gradient equals the monolithic gradient:\n
A + (h\')^*[C] \\\\;=\\\\; \\\\big(D L_\\\\xi(w_0)\\\\big)^*[\\\\mathbf{1}].\n\n3. (Genuine differentiability.) The monolithic loss map is Fréchet-differentiable at with gradient vector exactly : its derivative at exists and is the functional .\n\n4. (Same optimizer transition.)\n
\ni.e. running the optimizer once on the state with the tile-accumulated gradient — first projected onto the trainable coordinates (per-coordinate zeroing of ), then clipped once globally by the single radius — produces the same next training state (parameters, both moment slots, and step counter alike) as running it with the monolithic gradient treated identically.\n\nWhat the quantifiers silently include. No nonnegativity is assumed anywhere: the weights may be negative or zero, and the radius may be zero or negative. For the test fails for every (norms are ), so the second clip branch is always taken: nonzero vectors are rescaled by the negative factor (length , direction reversed), and even goes through that branch, giving under the division convention; for the clip is the usual radial projection onto the closed ball of radius . Degenerate instances are all covered: or (trivial spaces), (then every tile is empty, all sums are empty, both losses are , and ), the empty tile list (forcing ), and (then for every , so both sides of clause 4 become ). The optimizer is an arbitrary function of state and update vector, with no further assumptions. The hypotheses are jointly satisfiable in non-degenerate ways (e.g. smooth and with and the tables set to the genuine values), so nothing here is vacuous."\n}', 'startLine': 1, 'lineNumbers': [1, 2, 3]}, 'meta': {'source': {'type': 'internal', 'value': 'agent://RB2-M08'}}}}
Confirmed by the mission captain (proposal self-audit).