tickEquivNat_apply
plain-language theorem explainer
The declaration shows that the canonical map from the tick structure to natural numbers returns exactly the index component of each tick. Researchers formalizing the recognition-forced natural-number object would cite it to simplify index extractions in time-related proofs. The argument is immediate reflexivity once the equivalence definition is unfolded.
Claim. Let $Tick$ be the structure whose sole field is an index in $ℕ$. Let $ι: Tick → ℕ$ be the canonical equivalence sending each tick $t$ to its index. Then $ι(t) = t.index$ holds for every tick $t$.
background
The TimeAsOrbit module identifies the temporal sequence with the natural-number object forced by recognition. Tick is defined as a structure with a single field index : ℕ; time advances strictly by discrete increments with no background manifold. The equivalence tickEquivNat : Tick ≃ Nat is constructed by toFun t := t.index and invFun n := ⟨n⟩, with both inverses holding by reflexivity on the structure.
proof idea
The proof is a direct reflexivity after the definition of the equivalence is unfolded. No lemmas are applied; the left-hand side is literally t.index by the toFun clause of tickEquivNat.
why it matters
This supplies the concrete projection needed to treat tick counts as natural numbers inside the orbit construction of recognition. It directly supports the module claim that Tick is the canonical iteration object, closing the combinatorial identification of time with the natural-number object. The surrounding documentation notes that metric time, the eight-tick cycle, and the arrow of time remain outside this result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.