Foundation Time As Orbit Tick Orbit Eq Logic Nat

The tick as natural number

Natural numbers are the counting numbers: 0, 1, 2, 3, and so on. Mathematicians often define them by a starting point (zero) and a successor operation (add one). A natural-number object is any structure that behaves exactly like this, with a zero and a successor, and with the property that any other such structure maps uniquely into it. The declaration tick_orbit_eq_logicNat states that the tick, a discrete record of recognition events, forms such a natural-number object, and that it is canonically equivalent to the natural numbers themselves.

The proof works by showing that the tick type has a zero tick (index 0) and a successor function (advance the index by one). These satisfy the universal property of a natural-number object: primitive recursion exists and is unique. The declaration then constructs an explicit equivalence between ticks and the natural numbers, sending the zero tick to 0 and the successor tick to the successor natural number. This equivalence preserves the structure, meaning it maps the zero and successor of ticks to the zero and successor of natural numbers.

In Recognition Science, this closes the time-as-orbit frontier. The framework models time not as a background dimension but as the iteration of recognition steps. Each recognition step advances the tick by one, and the tick sequence is the natural-number object forced by recognition. The declaration proves that the temporal sequence and the natural numbers are the same iteration object up to unique isomorphism. Time is not added to physics; it is the canonical iteration object of recognition.

The declaration does not claim more than this structural identification. It does not derive metric time, the origin of the three spatial dimensions, or the arrow of time as a monotonicity property. What is proved is the structural identification: recognition steps generate the natural-number object, and that object is the tick. The tick is the counting of recognition events, and that counting is the natural numbers.

/-- **Time is the orbit.** The `Tick` type is canonically equivalent, as a
natural-number object, to `LogicNat`. The temporal iteration of recognition
and the orbit construction in `ArithmeticFromLogic` deliver the same
iteration object up to unique isomorphism. -/
noncomputable def tick_orbit_eq_logicNat : Tick ≃ LogicNat :=
  IsNaturalNumberObject.equiv tick_isNNO logicNat_isNNO

@[simp] theorem tickZero_index : tickZero.index = 0 := rfl

@[simp] theorem tickSucc_index (t : Tick) : (tickSucc t).index = t.index + 1 := rfl

/-- **Tick is a Lawvere natural-number object.** Together with `tickZero`
and `tickSucc`, the `Tick` type satisfies the universal property of the
natural-number object: primitive recursion exists and is unique. -/
def tick_isNNO :
    IsNaturalNumberObject (N := Tick) tickZero tickSucc where
  recursor := fun {X} x f => tickRecursor x f
  recursor_zero := fun {X} x f => tickRecursor_zero x f
  recursor_step := fun {X} x f t => tickRecursor_succ x f t
  recursor_unique := by
    intro X x f h hz hs t
    -- Reduce to induction on t.index.
    suffices hgen : ∀ n : Nat, h ⟨n⟩ = tickRecursor x f ⟨n⟩ by
      have := hgen t.index
      cases t
      exact this
    intro n
    induction n with
    | zero => exact hz
    | succ n ih =>
        have hstep : h ⟨n + 1⟩ = h (tickSucc ⟨n⟩) := rfl
        rw [hstep, hs ⟨n⟩, ih]
        rfl

/-- A `RecognitionStep` advances the tick by one, equivalently applies
`tickSucc` to the input snapshot's tick. This is the bridge from the
ledger dynamics of `TimeEmergence` to the abstract natural-number object
on `Tick`. -/
theorem recognitionStep_iterates_succ (step : RecognitionStep) :
    step.output.tick = tickSucc step.input.tick := by
  have hadv := step.tick_advance
  cases hin : step.input.tick with
  | mk i =>
    cases hout : step.output.tick with
    | mk o =>
      rw [hin, hout] at hadv
      simp [tickSucc]
      exact hadv

What this page does not claim

The declaration does not derive metric time, such as seconds or years. The declaration does not derive the origin of the three spatial dimensions. The declaration does not derive the arrow of time as a monotonicity property.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/TimeAsOrbit.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: