tick_orbit_eq_logicNat_zero
plain-language theorem explainer
The theorem shows that the canonical Lawvere equivalence identifying the tick sequence with LogicNat maps the zero tick to the identity element. Researchers formalizing the recognition-forced natural numbers cite this when confirming the base case of the orbit isomorphism. The proof is a term-mode one-liner that unfolds the equivalence and invokes the recursor property of the tick natural-number object at zero.
Claim. Let $T$ be the tick type equipped with zero element $0_T$ and successor $S_T$, and let $L$ be the inductive type with constructors $id_L$ and $step_L$. The unique isomorphism $e : T ≃ L$ of natural-number objects satisfies $e(0_T) = id_L$.
background
The module shows that Tick, with successor advancing the index by one, forms a Lawvere natural-number object. LogicNat is the inductive type whose constructors identity and step generate the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by the generator and containing 1. Upstream, tick_isNNO establishes that Tick satisfies the universal property of natural-number objects via its recursor, while tick_orbit_eq_logicNat constructs the equivalence IsNaturalNumberObject.equiv tick_isNNO logicNat_isNNO.
proof idea
The proof is a term-mode one-liner. It unfolds tick_orbit_eq_logicNat (which is IsNaturalNumberObject.equiv tick_isNNO logicNat_isNNO) and applies the recursor_zero field of tick_isNNO to LogicNat.identity and LogicNat.step.
why it matters
This supplies the zero case inside timeAsOrbitCert, the packaged certificate that Tick is the natural-number object equivalent to LogicNat. It completes the base case of the structural claim that recognition steps generate the iteration object, consistent with the forcing chain in which natural numbers arise from J-uniqueness and the self-similar fixed point. The result touches no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.