tick_orbit_eq_logicNat
plain-language theorem explainer
The Tick type, the discrete ledger unit of recognition steps, is canonically isomorphic as a natural-number object to LogicNat, the orbit generated by the Law of Logic. Researchers deriving time from recognition forcing would cite this to equate the temporal iteration with the arithmetic orbit construction. The equivalence is obtained by a one-line application of the universal property of Lawvere natural-number objects to the two structures.
Claim. The structure $Tick$ with distinguished element $tickZero$ and successor $tickSucc$ is canonically isomorphic, as a Lawvere natural-number object, to the inductive type $LogicNat$ with constructors $identity$ and $step$.
background
In this module time is identified with the canonical iteration object forced by recognition. The type $Tick$ is a structure carrying an index in the natural numbers; it is equipped with $tickZero$ as base and $tickSucc$ as the map sending each tick to its successor. The definition $tick_isNNO$ verifies that these data satisfy the universal property of a Lawvere natural-number object: for any pointed endomap there exists a unique recursor preserving zero and successor steps.
proof idea
The definition is a one-line wrapper that applies IsNaturalNumberObject.equiv to the two proofs that the structures are natural-number objects, namely tick_isNNO and logicNat_isNNO.
why it matters
This equivalence realizes the module claim that the temporal sequence is the natural-number object forced by recognition. It is invoked directly by tick_orbit_eq_logicNat_zero and tick_orbit_eq_logicNat_succ to preserve zero and successor, and these two theorems together with tick_isNNO populate the certificate timeAsOrbitCert. The result closes the combinatorial identification of time with the orbit construction while leaving metric time, the eight-tick origin of D=3, and Berry-phase monotonicity to separate modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.