tick_pos
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.
claimLet τ₀ 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 in Recognition Science
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.
scope and limits
- Does not assign a numerical value to τ₀ in SI units.
- Does not derive upper bounds on computation rate beyond positivity.
- Does not address continuous-time or relativistic corrections.
- Does not prove that τ₀ is the unique atomic time unit across all models.
Lean usage
theorem computation_takes_time (n : ℕ) (hn : n > 0) : n * fundamental_tick > 0 := mul_pos (Nat.cast_pos.mpr hn) tick_posformal statement (Lean)
47theorem tick_pos : fundamental_tick > 0 := by
proof body
Term-mode proof.
48 unfold fundamental_tick τ₀ tick
49 norm_num
50
51/-- The maximum computation rate (operations per unit time). -/