M05 — Streaming accumulator invariant
ProvedVathekProof.M05_tile_accum_partitionThe streaming accumulator computes plain finite sums, independent of the tile decomposition. For any two valid partitions of the same occurrence set, the executable left-to-right fold over tiles — accumulating loss, direct gradient contribution, and shared cotangent — yields exactly
for both partitions alike, and it satisfies the prefix law: folding is folding and continuing with from the intermediate accumulator. In exact arithmetic the accumulated result is therefore independent of tile order and of tile shape; a finite-precision schedule may differ, and that refinement is deliberately out of scope.
import Definitions.Def_VathekFrame import Definitions.Def_VathekState import Definitions.Def_VathekAdamW import Definitions.Def_VathekWitness
namespace VathekProof
/-- **M05 — Streaming accumulator invariant.** The executable left-to-right fold over
the tiles (loss, direct gradient, shared cotangent) equals, after every prefix, the
plain finite sums over the occurrences visited; consequently in exact arithmetic the
accumulated result is independent of the tile decomposition and of the tile order:
any two valid partitions of the same occurrence set give the same accumulator. -/
theorem M05_tile_accum_partition {ι : Type*} [DecidableEq ι] {W V : Type*}
[NormedAddCommGroup W] [NormedAddCommGroup V] [NormedSpace ℝ W] [NormedSpace ℝ V]
{I : Finset ι}
{ℬ ℬ' : List (Finset ι)} (α : ι → ℝ) (val : ι → ℝ) (a : ι → W) (c : ι → V)
(h : IsTilePartition I ℬ) (h' : IsTilePartition I ℬ') :
tileAccum α val a c ℬ = tileAccum α val a c ℬ'
∧ (tileAccum α val a c ℬ).loss = ∑ i ∈ I, α i * val i
∧ (tileAccum α val a c ℬ).direct = ∑ i ∈ I, α i • a i
∧ (tileAccum α val a c ℬ).shared = ∑ i ∈ I, α i • c i
∧ ∀ ℬ₁ ℬ₂ : List (Finset ι),
tileAccum α val a c (ℬ₁ ++ ℬ₂)
= tileAccumFold α val a c ℬ₂ (tileAccum α val a c ℬ₁) := by sorry
end VathekProofRead-back
What the Lean code literally says, in plain math · glm-5.3 (independent auditor subagent)
{"text": "{\n "data": "Declaration (single theorem). Let be an arbitrary type equipped with decidable equality (this assumption underwrites the finite-set union appearing below), and let and be arbitrary types carrying the structure of real normed vector spaces \u2014 a normed abelian group with a compatible -scalar multiplication; only the induced addition, zero, and scalar multiplication appear in the assertion itself, the norm plays no role. Universally quantified over all of these, and over:\n\n- a finite set (the occurrence set);\n- two finite lists of finite subsets of , and (the tile lists);\n- functions (weights), (values), and (per-occurrence contributions),\n\nthe theorem assumes, as hypotheses and , that each of and is a valid tile partition of , which literally means two things: first,\n
\n(the fold of set union over the list, starting from , equals exactly \u2014 so every tile is contained in and every element of lies in some tile); and second, the list is pairwise disjoint: any two tiles occupying distinct positions in the list are disjoint finite sets, i.e. no index belongs to two different tiles of the list. Together these force every to lie in exactly one tile of (and exactly one of ). What the quantifier thereby silently includes: empty tiles are permitted, in any number and at any position (an empty tile is disjoint from everything and does not change the union); a nonempty tile cannot appear twice in one list, since it is not disjoint from itself; the empty list is a valid partition only of ; and the hypotheses are always satisfiable (e.g. the one-tile list ), so the statement is not vacuous. In particular and may differ in the number of tiles, in the tiles themselves, and in their order.\n\nThe constructions the assertion refers to, unfolded: an accumulator is a triple with three data fields and nothing else,\n
\n(a running weighted loss, a running direct parameter-gradient contribution, and a running shared-state contribution). One streaming step over a finite tile sends\n
\nwhere the sums are finite sums over the finite set (an empty sum is ), is an ordinary product in , and is the -scalar multiplication on and on ; the data is fixed for the whole computation \u2014 no field is updated between tiles. The fold processes a tile list strictly left to right (the head tile is consumed first, then the tail), returning its starting accumulator unchanged on the empty list. Write for the fold over the list started from the zero accumulator , and for the same fold started from an arbitrary accumulator .\n\nUnder these hypotheses the theorem asserts the conjunction of five claims:\n\n1. Order- and decomposition-independence. . This is an equality of accumulator structures; since an accumulator is nothing but the three data components above, it holds exactly when all three fields agree \u2014 in , in , and in . Because may be any valid partition of \u2014 a coarser or finer decomposition, or a reordering of (a reordering is again a valid partition) \u2014 this says the final accumulator is the same whatever the tile decomposition and whatever the order of the tiles.\n\n2. Loss field equals the plain sum. : the tile-by-tile streamed accumulation of the loss reproduces the single finite sum over all of .\n\n3. Direct field equals the plain sum. in .\n\n4. Shared field equals the plain sum. in .\n\nClaims 2\u20134 are stated only for the list ; by claim 1 they hold verbatim with replaced by .\n\n5. Prefix (splitting) law. For all lists of finite subsets of \u2014 arbitrary lists carrying no partition, disjointness, or subset assumption whatsoever (repetitions and overlapping tiles included), so this clause does not depend on the hypotheses at all \u2014\n
\nwhere is concatenation of lists: folding over the concatenated stream in one pass from zero yields the same accumulator (again, field by field, all three components) as first folding over the first block from zero and then resuming the fold over the second block from that intermediate checkpoint. Its endpoint instances are degenerate and hold by the definition of the fold alone ( empty: both sides are ; empty: both sides are ).\n\nEdge cases of the whole statement: if , every valid partition consists only of empty tiles (or is the empty list), all finite sums vanish, and claims 1\u20134 reduce to saying the resulting accumulator is in each field; claim 5, being quantified over all tile lists, holds regardless of . No metric, limit, or analytic operation occurs anywhere in the assertion \u2014 it is a statement about finite sums, additions, and scalar multiples in , , and ."\n}", "details": {"resolvedPath": "/home/ajax/.omp/agent/sessions/-math/2026-09-22T19-31-08-510Z_01a0ca99-be5e-7000-93c6-dac7c74cc004/RB-M05.md", "contentType": "text/markdown", "totalLines": 3, "displayContent": {"text": "{\n "data": "Declaration (single theorem). Let be an arbitrary type equipped with decidable equality (this assumption underwrites the finite-set union appearing below), and let and be arbitrary types carrying the structure of real normed vector spaces \u2014 a normed abelian group with a compatible -scalar multiplication; only the induced addition, zero, and scalar multiplication appear in the assertion itself, the norm plays no role. Universally quantified over all of these, and over:\n\n- a finite set (the occurrence set);\n- two finite lists of finite subsets of , and (the tile lists);\n- functions (weights), (values), and (per-occurrence contributions),\n\nthe theorem assumes, as hypotheses and , that each of and is a valid tile partition of , which literally means two things: first,\n
\n(the fold of set union over the list, starting from , equals exactly \u2014 so every tile is contained in and every element of lies in some tile); and second, the list is pairwise disjoint: any two tiles occupying distinct positions in the list are disjoint finite sets, i.e. no index belongs to two different tiles of the list. Together these force every to lie in exactly one tile of (and exactly one of ). What the quantifier thereby silently includes: empty tiles are permitted, in any number and at any position (an empty tile is disjoint from everything and does not change the union); a nonempty tile cannot appear twice in one list, since it is not disjoint from itself; the empty list is a valid partition only of ; and the hypotheses are always satisfiable (e.g. the one-tile list ), so the statement is not vacuous. In particular and may differ in the number of tiles, in the tiles themselves, and in their order.\n\nThe constructions the assertion refers to, unfolded: an accumulator is a triple with three data fields and nothing else,\n
\n(a running weighted loss, a running direct parameter-gradient contribution, and a running shared-state contribution). One streaming step over a finite tile sends\n
\nwhere the sums are finite sums over the finite set (an empty sum is ), is an ordinary product in , and is the -scalar multiplication on and on ; the data is fixed for the whole computation \u2014 no field is updated between tiles. The fold processes a tile list strictly left to right (the head tile is consumed first, then the tail), returning its starting accumulator unchanged on the empty list. Write for the fold over the list started from the zero accumulator , and for the same fold started from an arbitrary accumulator .\n\nUnder these hypotheses the theorem asserts the conjunction of five claims:\n\n1. Order- and decomposition-independence. . This is an equality of accumulator structures; since an accumulator is nothing but the three data components above, it holds exactly when all three fields agree \u2014 in , in , and in . Because may be any valid partition of \u2014 a coarser or finer decomposition, or a reordering of (a reordering is again a valid partition) \u2014 this says the final accumulator is the same whatever the tile decomposition and whatever the order of the tiles.\n\n2. Loss field equals the plain sum. : the tile-by-tile streamed accumulation of the loss reproduces the single finite sum over all of .\n\n3. Direct field equals the plain sum. in .\n\n4. Shared field equals the plain sum. in .\n\nClaims 2\u20134 are stated only for the list ; by claim 1 they hold verbatim with replaced by .\n\n5. Prefix (splitting) law. For all lists of finite subsets of \u2014 arbitrary lists carrying no partition, disjointness, or subset assumption whatsoever (repetitions and overlapping tiles included), so this clause does not depend on the hypotheses at all \u2014\n
\nwhere is concatenation of lists: folding over the concatenated stream in one pass from zero yields the same accumulator (again, field by field, all three components) as first folding over the first block from zero and then resuming the fold over the second block from that intermediate checkpoint. Its endpoint instances are degenerate and hold by the definition of the fold alone ( empty: both sides are ; empty: both sides are ).\n\nEdge cases of the whole statement: if , every valid partition consists only of empty tiles (or is the empty list), all finite sums vanish, and claims 1\u20134 reduce to saying the resulting accumulator is in each field; claim 5, being quantified over all tile lists, holds regardless of . No metric, limit, or analytic operation occurs anywhere in the assertion \u2014 it is a statement about finite sums, additions, and scalar multiples in , , and ."\n}", "startLine": 1, "lineNumbers": [1, 2, 3]}, "meta": {"source": {"type": "internal", "value": "agent://RB-M05"}}}}
Confirmed by the mission captain (proposal self-audit).