minimal_temporal_resolution
plain-language theorem explainer
The theorem asserts that whenever one ledger snapshot precedes another under the before relation, their tick indices differ by at least one. Researchers formalizing discrete time in Recognition Science cite it to enforce quantization with no sub-tick events. The proof is a one-line wrapper that unfolds the before predicate and applies omega to the resulting integer inequality.
Claim. For all ledger snapshots $s_1, s_2$, if the tick index of $s_1$ is strictly smaller than the tick index of $s_2$, then $1$ is at most the difference of those indices.
background
LedgerSnapshot is a structure pairing a Tick with a nonnegative real defect value; it records ledger state at discrete instants rather than along a continuous parameter. The before relation on snapshots is defined by strict inequality of their tick indices. The module sets time equal to the ledger tick counter with no background continuum, and the eight-tick epoch (period $2^3$) as the minimal complete update cycle. Upstream, the tick constant supplies the fundamental RS time quantum of value 1, while defect monotonicity supplies the direction for the arrow of time.
proof idea
The term proof introduces the two snapshots and the before hypothesis, unfolds before to expose the strict index inequality, and invokes omega to obtain the required lower bound of 1 on the difference.
why it matters
The result fills the F-004 claim that time is discrete tick count with no sub-tick dynamics. It supports the arrow-of-time construction via irreversible defect decrease within an epoch and aligns with the eight-tick octave forced by T7. No downstream theorems yet reference it, but it closes the quantization step required for the present-past-future distinction in the ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.