sequential_preserves_conservation
Why this theorem is linked from Diagnosing and Improving Diffusion Models by Estimating the Optimal Loss Value unclear
Pith linked this Lean declaration because the review connected a specific passage in the paper to this theorem. The relation tag says how strong that connection is; it is not a generic placeholder.
We develop effective estimators … stochastic variant scalable to large datasets with proper control of variance and bias
Relation between the paper passage and the cited Recognition theorem.
plain-language theorem explainer
If a predicate on states is preserved by each single event posting from a finite set H, then the predicate holds after folding the posting function over any schedule whose order covers H. Recognition Science work on causal serialization of finite histories cites this result to carry invariants through topological orderings. The proof runs by induction on the schedule list via its recursor, using a membership lemma to invoke the single-step hypothesis at each step.
Claim. Let $E$ be an event type and $S$ a state type. Let Conservation be a predicate on states and post a function posting an event to a state. Let prec be a precedence relation on events. For finite set $H$ of events and schedule σ whose order covers $H$, if Conservation holds on initial state $s_0$ and is preserved by every single posting of an event from $H$, then Conservation holds on the state obtained by folding post over the order of σ starting from $s_0$.
background
Precedence is the relation on events read as “e₁ must occur before e₂”. Schedule is the structure carrying a duplicate-free list order that forms a one-per-tick serialization of a finite history. The module works abstractly over any event type E equipped with a decidable precedence relation and produces constructive results for finite histories only, deliberately avoiding cost or convexity assumptions from T5 onward.
proof idea
The tactic proof first invokes classical, reverts the initial state and hypothesis, then refines the list recursor on σ.order. The base case is immediate by simpa. The step case extracts membership of the head event in H via toFinset conversion and the cover hypothesis, applies the single-step preservation hypothesis to obtain the updated conservation fact, then recurses via the inductive hypothesis.
why it matters
The lemma supplies the generic preservation half of the atomicity construction that tightens T2. It feeds the atomic_tick result by guaranteeing that any conservation predicate survives serialization. The result stays independent of the J-cost functional equation, the phi-ladder, and the eight-tick octave, isolating the finite-history serialization step in the forcing chain.
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."