module module high

`IndisputableMonolith.Foundation.TimeAsOrbit`

The TimeAsOrbit module defines the Tick type as the discrete orbit generated by a canonical successor, realizing time as ledger tick count with no background continuum. Researchers deriving the arrow of time from logical forcing would cite it to ground the eight-tick minimal period. The module assembles successor, zero, equivalence to naturals, and recursor from the imported Lawvere natural-number object axioms.

claimLet $T$ be the type equipped with zero element $0:T$ and successor map $s:T→ T$ that satisfies the Lawvere natural-number object axioms: for any type $X$ with distinguished point $x:X$ and endomorphism $f:X→ X$ there exists a unique map $u:T→ X$ such that $u(0)=x$ and $u(s(t))=f(u(t))$. The structure is canonically equivalent to the natural numbers.

background

The module imports ArithmeticFromLogic, TimeEmergence, and the NaturalNumberObject characterization. TimeEmergence establishes that time is identical to the ledger tick counter and that the minimal complete update cycle has period $2^D$ for $D=3$. NaturalNumberObject supplies the categorical definition: a triple $(N,z,s)$ is a natural-number object when, for every triple $(X,x,f)$ with $x:X$ and $f:X→ X$, there exists a unique mediating map from $N$ to $X$ preserving the point and commuting with the endomorphism.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the concrete discrete orbit structure that RealityFromDistinction invokes as the canonical time orbit in its master forcing-chain theorem. That theorem starts from a single distinction on an inhabited carrier and derives spacetime, light cone, and time as the canonical orbit; the present definitions realize the T7 eight-tick octave step of the unified forcing chain.

scope and limits

Does not derive the emergence of time from ledger updates.
Does not connect ticks to spatial dimensions or physical constants.
Does not treat continuous-time limits or Lorentz invariance.
Does not prove uniqueness of the successor beyond the NNO axioms.

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