timeAsOrbitCert
plain-language theorem explainer
The timeAsOrbitCert definition assembles a certificate showing that Tick with its zero and successor forms a Lawvere natural-number object canonically equivalent to the LogicNat orbit. Foundation researchers cite it to confirm that temporal iteration coincides with the recognition-forced natural-number object. The construction is a direct structure instantiation that references the pre-proved NNO property of Tick and the equivalence theorems to LogicNat.
Claim. Let Tick be the type of recognition ticks equipped with zero and successor. There exists a certificate C such that Tick satisfies the universal property of a Lawvere natural-number object, Tick is isomorphic to LogicNat, the isomorphism sends zero to the identity element and successor to the step operation, and every recognition step advances the tick by the successor.
background
The TimeAsOrbit module defines Tick as the type of recognition ticks with zero and successor, making the explicit claim that this sequence is the natural-number object forced by recognition. The structure TimeAsOrbitCert collects five fields: the IsNaturalNumberObject property on Tick, the equivalence Tick ≃ LogicNat, preservation of zero and successor under that equivalence, and the statement that recognition steps advance the tick by successor. Upstream results establish tick_isNNO via the recursor on Tick and tick_orbit_eq_logicNat as the canonical isomorphism induced by the universal property of natural-number objects, with the zero and successor preservation theorems following by unfolding the equivalence.
proof idea
The definition is a structure constructor that directly populates the five fields of TimeAsOrbitCert by reference to sibling results: tick_is_NNO from tick_isNNO, tick_equiv_logicNat from tick_orbit_eq_logicNat, and the zero, successor, and recognition-advance properties from the corresponding theorems. It functions as a one-line wrapper that assembles the certificate from the already-established NNO property and equivalence lemmas in the module.
why it matters
This definition supplies the concrete certificate that realizes the module's claim that Tick is the canonical natural-number object forced by recognition and equivalent to LogicNat, feeding directly into the inhabited theorem timeAsOrbitCert_inhabited. It closes the combinatorial identification of time as iteration object in the foundation layer, prior to metric time or the eight-tick octave. The module doc notes that this structural result does not address the arrow of time or D=3 forcing, which appear in separate layers of the chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.