tickEquivLogicNat
plain-language theorem explainer
The declaration supplies the canonical isomorphism identifying the tick sequence with the logic-natural numbers. Researchers tracing the Recognition forcing chain from recognition steps to arithmetic would cite it to equate time with the natural-number object. The proof is a one-line composition of the tick-to-natural equivalence with the inverse of the logic-natural-to-natural equivalence.
Claim. The canonical isomorphism between the tick sequence (as Lawvere natural-number object under successor) and the logic-natural numbers (as the orbit generated by the recognition step) obtained by round-trip through the ordinary natural numbers.
background
The module establishes that the temporal sequence Tick is the Lawvere natural-number object forced by recognition, with successor defined by incrementing the index. LogicNat is the inductive type whose constructors are identity (zero-cost element) and step (one iteration of the generator), mirroring the orbit {1, γ, γ², …} closed under multiplication by the recognition generator γ. The upstream result equivNat supplies the round-trip isomorphism LogicNat ≃ Nat with explicit left and right inverses fromNat_toNat and toNat_fromNat. The module imports TimeEmergence for the Tick type and ArithmeticFromLogic for the orbit construction, closing the identification that recognition steps generate the same iteration object as the tick count.
proof idea
One-line wrapper that applies the transitivity of equivalence: compose the already-established tick-to-natural map with the symmetric of the logic-natural-to-natural map.
why it matters
This definition completes the structural claim in the module that time is the canonical iteration object of recognition rather than an added structure. It feeds the universal property of natural-number objects proved in UniversalForcing.NaturalNumberObject and aligns with the T0–T8 forcing chain by supplying the natural-number object at the combinatorial level. The module explicitly notes that metric time, the eight-tick origin of D=3, and the Berry-phase arrow of time remain outside this identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.