tick_is_atomic_time_unit
plain-language theorem explainer
The declaration shows that for any positive integer n the product n times the fundamental tick remains at least one tick. Researchers modeling discrete spacetime or bounding parallel computation rates would cite it to enforce the atomic time floor. The proof casts the natural-number premise into the reals and closes the inequality with linear arithmetic.
Claim. For every positive integer $n$, $n tau_0 geq tau_0$, where $tau_0$ is the fundamental tick (the atomic time unit in Recognition Science).
background
The module IC-002 derives computation limits from temporal discreteness in Recognition Science. The fundamental tick $tau_0$ is defined as the minimum time quantum; each recognition event occupies exactly one tick, so the maximum operation rate is $1/tau_0$ in RS units. Parallel operations cannot subdivide this interval below $tau_0$ itself. Upstream lemmas supply the positivity of the tick and the natural-number ordering used here; sibling results such as tick_pos and fundamental_tick fix the notation and the strict positivity needed for the arithmetic step.
proof idea
The term proof opens with intro n hn, derives the real inequality $1 leq n$ from Nat.one_le_cast applied to hn, recalls fundamental_tick > 0 from the sibling lemma tick_pos, and finishes with nlinarith.
why it matters
The result anchors the temporal-discreteness pillar of IC-002 by confirming that no integer number of parallel operations can undercut the tick duration. It directly supports the maximum bit-rate claim of one operation per tick and aligns with the eight-tick octave structure in the forcing chain. Because used_by is empty, the lemma functions as a self-contained building block for later limit theorems rather than feeding an immediate parent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.