tick_isNNO
Tick equipped with tickZero and tickSucc forms a Lawvere natural-number object, so primitive recursion on ticks is unique. Researchers tracing the Recognition Science derivation of time from recognition steps cite this to equate the ledger iteration with the forced orbit. The definition supplies the recursor via tickRecursor and proves uniqueness by reducing the equality to induction on the underlying index.
claimThe type $Tick$ together with the distinguished element $tickZero$ and the successor map $tickSucc$ satisfies the Lawvere universal property of a natural-number object: for any type $X$, element $x_0 : X$ and function $f : X → X$ there exists a unique function $h : Tick → X$ such that $h(tickZero) = x_0$ and $h(tickSucc(t)) = f(h(t))$ for every $t$.
background
The module TimeAsOrbit asserts that temporal succession is the canonical iteration object forced by recognition. Tick is constructed from ledger indices; its zero and successor are the obvious base and increment. Upstream, LogicNat is the inductive type with constructors identity and step that encodes the orbit {1, γ, γ², …} under the generator supplied by ArithmeticFromLogic; its successor is defined by step. The structure IsNaturalNumberObject, imported from UniversalForcing.NaturalNumberObject, packages exactly the recursor and uniqueness data that Lawvere requires.
proof idea
The definition populates the four fields of IsNaturalNumberObject. recursor, recursor_zero and recursor_step are set directly to the already-proved tickRecursor, tickRecursor_zero and tickRecursor_succ. recursor_unique proceeds by reducing the claim to an auxiliary statement ∀ n : Nat, h ⟨n⟩ = tickRecursor x f ⟨n⟩, then proving the auxiliary by ordinary induction on n: the zero case is the supplied hz, the successor case rewrites via hs and applies the induction hypothesis.
why it matters in Recognition Science
tick_isNNO is the key datum fed to tick_orbit_eq_logicNat, which constructs the canonical isomorphism Tick ≃ LogicNat and thereby certifies that recognition steps generate the same iteration object as the orbit construction. The module doc-comment states that this identification “closes the time-as-orbit frontier: time is not added to physics; it is the canonical iteration object of recognition.” The result supplies the combinatorial skeleton required by the forcing chain before metric time or the eight-tick octave is introduced in later layers.
scope and limits
- Does not derive a metric or continuous time coordinate.
- Does not produce the eight-tick periodicity or spatial dimension D=3.
- Does not address the Berry-phase mechanism for the arrow of time.
- Does not calibrate physical constants such as α or G.
formal statement (Lean)
93def tick_isNNO :
94 IsNaturalNumberObject (N := Tick) tickZero tickSucc where
proof body
Definition body.
95 recursor := fun {X} x f => tickRecursor x f
96 recursor_zero := fun {X} x f => tickRecursor_zero x f
97 recursor_step := fun {X} x f t => tickRecursor_succ x f t
98 recursor_unique := by
99 intro X x f h hz hs t
100 -- Reduce to induction on t.index.
101 suffices hgen : ∀ n : Nat, h ⟨n⟩ = tickRecursor x f ⟨n⟩ by
102 have := hgen t.index
103 cases t
104 exact this
105 intro n
106 induction n with
107 | zero => exact hz
108 | succ n ih =>
109 have hstep : h ⟨n + 1⟩ = h (tickSucc ⟨n⟩) := rfl
110 rw [hstep, hs ⟨n⟩, ih]
111 rfl
112
113/-! ## Time IS the orbit (Lawvere identification) -/
114
115/-- **Time is the orbit.** The `Tick` type is canonically equivalent, as a
116natural-number object, to `LogicNat`. The temporal iteration of recognition
117and the orbit construction in `ArithmeticFromLogic` deliver the same
118iteration object up to unique isomorphism. -/