sequential_preserves_conservation
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
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of any schedule for a given history.
- Does not extend to infinite event collections.
- Does not invoke cost functions, J, or convexity.
- Does not assume specific values for phi, alpha, or G.
- Does not establish uniqueness of the schedule order.
formal statement (Lean)
234theorem sequential_preserves_conservation
235 {S : Type _} (Conservation : S → Prop) (post : S → E → S)
236 (prec : Precedence E)
237 [DecidableRel prec] [DecidableEq E]
238 (H : Finset E) (σ : Schedule E)
239 (hcover : σ.order.toFinset = H)
240 (s0 : S)
241 (h0 : Conservation s0)
242 (preserve_single : ∀ s e, e ∈ H → Conservation s → Conservation (post s e)) :
243 Conservation (σ.order.foldl post s0) := by
proof body
Tactic-mode proof.
244 classical
245 revert s0 h0
246 refine σ.order.rec ?base ?step
247 · intro s h; simpa using h
248 · intro e tail ih s h
249 have heH : e ∈ H := by
250 have : e ∈ (e :: tail).toFinset := by
251 simpa using List.mem_toFinset.mpr (by simp)
252 simpa [hcover] using this
253 have h' : Conservation (post s e) := preserve_single s e heH h
254 simpa using ih (post s e) h'
255
256/-- Atomic tick (finite history): any finite recognition history admits a
257 serialization with exactly one posting per tick that respects precedence. -/