tick_pos
plain-language theorem explainer
The fundamental tick τ₀ is strictly positive in RS-native units. Researchers deriving discrete-time computation bounds cite this to fix the minimum time per operation. The proof is a one-line term reduction that unfolds the definition to the constant 1 and applies numerical normalization.
Claim. Let τ₀ denote the fundamental time quantum. Then τ₀ > 0.
background
The module IC-002 derives computation limits from Recognition Science via temporal discreteness, where τ₀ is the minimum time quantum and sets the maximum bit rate at 1/τ₀. Upstream, tick is defined as the constant 1 in ℝ with the abbreviation τ₀ := tick, and fundamental_tick is the direct alias τ₀. The module doc states that this discreteness supplies one of three sources of limits, alongside irrational constants and Landauer costs.
proof idea
The term proof unfolds fundamental_tick to τ₀, then to tick, which equals 1 by definition, and closes with norm_num to establish positivity of the constant.
why it matters
This is IC-002.1 and directly supplies the positivity hypothesis for downstream results including tick_rate_bounded, max_rate_pos, tick_is_atomic_time_unit, and computation_takes_time (which states that n steps require at least n × τ₀). It anchors the IC-002 certificate and supports the framework claim that temporal discreteness bounds information processing, consistent with the eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.