pith. sign in
module module high

IndisputableMonolith.Foundation.TimeAsOrbit

show as:
view Lean formalization →

The TimeAsOrbit module equips the Tick type with zero and a canonical successor to realize it as the orbit under iteration, satisfying the Lawvere natural-number-object axioms. It connects the tick-count view of time from ledger updates to the forced arithmetic structure. Researchers following the Recognition Science chain from logic to spacetime cite it for the discrete time orbit. The module supplies the successor, zero, Nat equivalence, and recursor via direct definitions and one-line applications of upstream results.

claimThe structure $( ext{Tick}, 0, s)$ with successor $s$ forms a natural number object: for any triple $(X, x, f)$ with $x : X$ and $f : X o X$ there exists a unique map $ ext{Tick} o X$ preserving zero and successor. Equivalence to $\mathbb{N}$ holds via the induced isomorphism.

background

The module imports TimeEmergence, which states there is no background time and time IS the ledger tick counter with the 8-tick cycle as minimal complete update. It also imports ArithmeticFromLogic and the NaturalNumberObject module whose doc-comment gives the Lawvere characterization: a triple $(N, z, s)$ is a natural-number object if for every triple $(X, x, f)$ with $x : X$ and $f : X o X$ there exists a unique map. Sibling declarations introduce the successor on Tick, the zero element, the equivalence to natural numbers, and the recursor.

proof idea

This is a definition module. It declares tickZero and tickSucc, then constructs the equivalence to Nat and the recursor by direct appeal to the Lawvere universal property supplied by the NaturalNumberObject import. One-line wrappers establish the zero and successor cases of the equivalence.

why it matters in Recognition Science

The module supplies the canonical orbit structure for time that the RealityFromDistinction module imports as part of its master forcing-chain theorem. That theorem starts from a single distinction on an inhabited carrier and derives the full chain to spacetime, the light cone, and time as the canonical orbit. It thereby closes the step from ledger ticks to the arithmetic object required for the eight-tick octave and D=3.

scope and limits

used by (1)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (21)