tickEquivNat_symm_apply
plain-language theorem explainer
The inverse of the canonical equivalence between the Tick orbit and natural numbers recovers the Tick constructor from any index n. Researchers formalizing the combinatorial identification of time with the forced natural-number object would cite this for index-to-tick rewrites. The statement holds immediately by unfolding the inverse map in the equivalence definition.
Claim. Let $e : Tick ≃ ℕ$ be the canonical equivalence sending each tick to its index. Then $e^{-1}(n) = ⟨n⟩$ for every natural number $n$.
background
The module establishes that the temporal sequence Tick is the Lawvere natural-number object forced by recognition, canonically equivalent to the orbit construction LogicNat. Tick carries a successor that iterates recognition steps, and the equivalence identifies this iteration object with the standard naturals up to unique isomorphism.
proof idea
The proof is a one-line wrapper that applies reflexivity to the defining equation of the inverse function in tickEquivNat.
why it matters
This supplies the simp rule for the inverse direction of the Tick-Nat equivalence, supporting calculations that begin from natural-number counts and recover the corresponding recognition ticks. It fills the structural claim in the module that Tick is the canonical iteration object of recognition, prior to metric time or the eight-tick cycle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.