T2_atomicity
plain-language theorem explainer
Atomicity of ticks asserts that each natural-number tick posts to at most one unit inside any RecognitionStructure carrying an AtomicTick instance. Chain and Recognition module authors cite it to guarantee collision-free discrete events before deriving continuity or flux conservation. The proof extracts the unique witness supplied by unique_post and equates both input postings to that witness by transitivity.
Claim. For any RecognitionStructure $M$ equipped with an AtomicTick instance, if a natural number $t$ satisfies postedAt$(t,u)$ and postedAt$(t,v)$ for units $u,v$ in $M$, then $u=v$.
background
The AtomicTick class on a RecognitionStructure $M$ supplies the predicate postedAt : Nat → M.U → Prop together with the axiom unique_post : ∀ t, ∃! u, postedAt t u. This supplies the only hypothesis used by T2_atomicity. The Chain module contains a minimal RecognitionStructure stub whose sole purpose is to host this and the sibling T3_continuity theorem. The identical AtomicTick definition appears upstream in the Recognition module, where the same statement is proved verbatim and then re-exported by RRF.Core.Recognition.
proof idea
The term proof introduces t, u, v and the two posting hypotheses. It performs rcases on AtomicTick.unique_post t to obtain a witness w together with the uniqueness function huniq. Two applications of huniq produce u = w and v = w; transitivity with symmetry of equality yields the goal.
why it matters
T2_atomicity is the atomicity step (T2) inside the Recognition Science forcing chain. It is invoked directly by Recognition.T2_atomicity and by the RRF.Core re-export that bridges to the chainFlux conservation lemma. Atomicity precedes the continuity axiom T3 and the later steps that force the eight-tick octave and D = 3. No open scaffolding remains; the result is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.