module module high

`IndisputableMonolith.Foundation.TimeAsOrbit`

This module realizes time as the canonical orbit on the Tick type by equipping it with the Lawvere natural-number-object structure: zero, successor, and a recursor. It is cited by the master forcing-chain theorem in RealityFromDistinction. The module is purely definitional, introducing tickSucc, tickZero, tickEquivNat, and tickRecursor together with their basic properties.

claimLet $\mathrm{Tick}$ be the type with $0 : \mathrm{Tick}$ and $s : \mathrm{Tick} \to \mathrm{Tick}$ such that for any type $X$ with $x_0 : X$ and $f : X \to X$ there exists a unique map $r : \mathrm{Tick} \to X$ satisfying $r(0) = x_0$ and $r(s(t)) = f(r(t))$. There is a canonical equivalence $\mathrm{Tick} \simeq \mathbb{N}$ preserving zero and successor.

background

The module sits inside the foundation layer that derives time from the ledger update cycle. Upstream, TimeEmergence states that time IS the ledger tick counter and that the minimal complete update is the 8-tick cycle (2^D for D=3). NaturalNumberObject supplies the Lawvere characterization: a triple (N, z, s) is a natural-number object when every (X, x, f) admits a unique mediating map.

Tick is introduced as the concrete carrier that satisfies this universal property. The definitions tickZero, tickSucc, tickEquivNat, and tickRecursor realize the zero, successor, equivalence to the standard naturals, and the recursion principle. These are the minimal data needed to treat time as discrete orbits generated by a single successor operation.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the concrete Tick orbit that the master forcing-chain theorem in RealityFromDistinction requires. That theorem starts from a single distinction on an inhabited carrier and derives spacetime, the light cone, and time as the canonical orbit; the present definitions close the step that identifies time with the forced natural-number object.

scope and limits

Does not introduce continuous time or real numbers.
Does not derive the 8-tick minimal period or the value D=3.
Does not compute physical constants or mass ladders.
Does not address the arrow of time beyond the successor direction.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.RealityFromDistinction module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.ArithmeticFromLogic module_import
IndisputableMonolith.Foundation.TimeEmergence module_import
IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject module_import

declarations in this module (21)

def tickSucc L47
theorem tickSucc_index L49
def tickZero L52
theorem tickZero_index L54
def tickEquivNat L59
theorem tickEquivNat_apply L65
theorem tickEquivNat_symm_apply L66
theorem tickEquivNat_zero L69
theorem tickEquivNat_succ L71
def tickEquivLogicNat L75
def tickRecursor L81
theorem tickRecursor_zero L84
theorem tickRecursor_succ L87
def tick_isNNO L93
def tick_orbit_eq_logicNat L119
theorem tick_orbit_eq_logicNat_zero L123
theorem tick_orbit_eq_logicNat_succ L129
theorem recognitionStep_iterates_succ L140
structure TimeAsOrbitCert L157
def timeAsOrbitCert L167
theorem timeAsOrbitCert_inhabited L174