T2_atomicity
plain-language theorem explainer
Atomicity of ticks asserts that each natural-number tick posts to at most one state in any recognition structure. Researchers tracing the Recognition Science forcing chain would cite this to guarantee uniqueness of state per tick before building the phi-ladder or mass formulas. The proof is a direct term-mode reduction that applies the unique_post axiom from the AtomicTick class to equate the two states via a common witness.
Claim. Let $M$ be a recognition structure equipped with an atomic tick instance. For any natural number $t$ and states $u, v$ in the universe of $M$, if tick $t$ posts to both $u$ and $v$ then $u = v$.
background
The AtomicTick class on a recognition structure $M$ supplies a posting relation postedAt : Nat → M.U → Prop together with the axiom that each tick possesses a unique state satisfying the relation. This class is imported from the Chain module and instantiated locally on the concrete structure M defined in the Recognition module. The module begins with the T1 statement that nothing cannot recognize itself, which supplies the base recognition structure before atomicity is imposed.
proof idea
The term proof introduces the tick and two candidate states, then performs rcases on the unique_post witness for that tick to obtain a common state w. It derives u = w and v = w from the uniqueness property and concludes by transitivity of equality.
why it matters
This is the Recognition module's version of T2 atomicity, re-exported verbatim in RRF.Core.Recognition.T2_atomicity and referenced by the Chain module's own T2_atomicity. It supplies the atomicity step inside the T0-T8 forcing chain, ensuring unique posting per tick before J-uniqueness (T5) and the eight-tick octave (T7) are derived. The claim is fully proved with no scaffolding or open questions remaining.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.