Tick
plain-language theorem explainer
Ticks formalize discrete time as ledger indices in Recognition Science. Researchers modeling emergent time from computational updates cite this to ground the arrow of time in irreversible defect reduction. The definition supplies the natural number index together with decidable order instances that make temporal comparison immediate.
Claim. A tick $t$ is specified by its index $n : ℕ$, equipped with the order $t_1 ≤ t_2$ iff $n_1 ≤ n_2$ and the strict order $t_1 < t_2$ iff $n_1 < n_2$, both decidable via the corresponding operations on natural numbers.
background
The TimeEmergence module formalizes how time emerges from the ledger update cycle with no background manifold. Time is the tick counter; the minimal complete update is the 8-tick cycle (2^D for D=3). The fundamental RS time quantum τ₀ equals 1 tick in native units, as supplied by the Constants module.
proof idea
The declaration defines the Tick structure with a single index field and derives DecidableEq. It then installs the LE and LT instances by direct delegation to the index order, followed by DecidableRel instances that invoke Nat.decLe and Nat.decLt.
why it matters
This supplies the atomic time unit used by downstream results such as ml_nucleosynthesis_eq_phi and ml_is_phi_power in astrophysics, as well as crystal and magnetism theorems in chemistry. It realizes the T7 eight-tick octave and the F-004/F-006 claims that time is ledger progression with an arrow from monotonic defect decrease.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.