sequential_preserves_conservation
plain-language theorem explainer
If a conservation predicate on states holds initially and is preserved under each single event posting from a finite history, then it holds after folding the posting function over any sequential schedule whose order covers that history. Researchers formalizing causal invariants in recognition-based discrete physics would cite this when checking properties along topological orderings. The proof applies list recursion to the schedule order, confirming membership via the covering hypothesis and invoking single-step preservation at each inductive 1
Claim. Let $S$ be a state space, $C:S→Prop$ a conservation predicate, $post:S→E→S$ the update map, and $≺$ a precedence relation on events $E$. For finite $H⊆E$ and schedule $σ$ with order list covering $H$, if $C(s_0)$ and $∀s,e∈H, C(s)⇒C(post(s,e))$, then $C(σ.order.foldl(post,s_0))$.
background
The Atomicity module supplies axiom-free serialization for finite recognition histories over an abstract event type $E$ with precedence relation $prec$, where $prec e_1 e_2$ asserts that $e_1$ must occur before $e_2$. A Schedule is a structure containing a list order of pairwise distinct events. The present theorem assumes the order's toFinset equals the supplied finite set $H$ and works entirely within decidable relations on that set.
proof idea
The tactic proof enters classical mode, reverts the initial state and hypothesis, then refines recursion on the schedule order list. The base case simplifies directly. The step case extracts head-event membership in $H$ from the covering equality and list membership lemmas, applies the single-step preservation hypothesis to obtain the updated conservation fact, and invokes the inductive hypothesis on the tail.
why it matters
This generic preservation lemma supplies the conservation-invariance step required by the atomicity construction that tightens T2 in the forcing chain. It guarantees that any predicate preserved by individual postings remains invariant under any valid topological serialization of a finite history. The module deliberately avoids cost or convexity assumptions from T5, keeping the result independent of the J-function and phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 5 of 5)
-
Optimal loss estimate diagnoses diffusion training
"We develop effective estimators … stochastic variant scalable to large datasets with proper control of variance and bias"
-
Condition number bounds clustering error from objective gap
"Core(s) = {i : d(x_i,θ*_j) ≤ D_eff − s}; enhanced margin γ + 2s; zero-error cores when local κ(s)·δ < 1/n (Lemma 5.1, Proposition 5.2)"
-
Mutual information beats entropy in benchmark selection
"Entropy greedy is pivoted Cholesky, runs in O(k²N) time... MI is non-monotone in general but empirically monotone for small k, so we use greedy as a heuristic rather than invoking the standard monotone-submodular guarantee."
-
Risk budgets stabilize continuous edge inference scheduling
"Asynchronous online algorithm with finite-step convergence via FIP of potential games (Monderer–Shapley)."
-
Stiff limit of conservation laws produces new crowd PDE
"Uniform BV estimates ‖∂_x ρ(t)‖_{L^1} ≤ C(T)‖ρ_0‖_{BV} and ∫∫|∂_x ρ^{k+1} ∂_x U| ≤ C(T)‖ρ_0‖_{BV}, used for strong compactness via Aubin–Lions."