tick_orbit_eq_logicNat_succ
plain-language theorem explainer
The theorem establishes that the canonical equivalence mapping the tick sequence to LogicNat preserves the successor operation. Researchers verifying the identification of time with the recognition iteration object cite it when assembling the full TimeAsOrbitCert. The term proof unfolds the equivalence definition and applies the recursor step property of the natural number object on Tick.
Claim. Let $t$ be a tick. Under the canonical isomorphism equiv from the tick orbit to LogicNat, equiv(succ($t$)) equals the successor step applied to equiv($t$).
background
The module TimeAsOrbit asserts that Tick forms a Lawvere natural-number object under the successor tickSucc, hence is canonically isomorphic to LogicNat, the orbit object constructed in ArithmeticFromLogic. The equivalence tick_orbit_eq_logicNat is defined via IsNaturalNumberObject.equiv, which encodes the universal property that any structure with a zero and successor admits a unique morphism from the NNO. Upstream, tick_isNNO supplies the concrete recursor for Tick, while Constants.tick fixes the fundamental time quantum as the unit step in RS-native units.
proof idea
The term proof first unfolds tick_orbit_eq_logicNat together with IsNaturalNumberObject.equiv. It then applies the recursor_step lemma from tick_isNNO, instantiated at the zero map LogicNat.identity and the successor map LogicNat.step, evaluated at the input tick t.
why it matters
This result supplies the successor clause of the TimeAsOrbitCert certificate, which collects tick_isNNO, the zero and successor preservation lemmas, and the recognition advancement property. It completes the combinatorial half of the claim that temporal succession is the forced natural-number object of recognition, directly supporting the T0-T8 forcing chain where time emerges as the iteration structure before metric or dimensional structure is imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.