J_bit_pos

formal source

  69noncomputable def J_bit : ℝ := Real.log φ_val
  70
  71/-- J_bit > 0 since φ > 1. -/
  72theorem J_bit_pos : J_bit > 0 := Real.log_pos φ_gt_one
  73
  74/-- The coherence quantum: E_coh = φ^(-5).
  75    This is the minimum energy for coherent recognition. -/
  76noncomputable def E_coh : ℝ := φ_val^(-5 : ℤ)
  77
  78/-- E_coh > 0. -/
  79theorem E_coh_pos : E_coh > 0 := by
  80  unfold E_coh
  81  exact zpow_pos phi_pos (-5)
  82
  83/-- The eight-tick period. -/
  84def period_8 : ℕ := 8
  85
  86/-- The fundamental time τ₀ (in RS-native units, τ₀ = 1 by definition). -/
  87noncomputable def τ₀ : ℝ := 1
  88
  89/-- The fundamental length ℓ₀ (in RS-native units). -/
  90noncomputable def ℓ₀ : ℝ := 1
  91
  92/-! ## Speed of Light: c = ℓ₀/τ₀ -/
  93
  94/-- **Speed of light** in RS-native units.
  95
  96    c is the ratio of fundamental length to fundamental time.
  97    In RS-native units where ℓ₀ = τ₀ = 1, we have c = 1.
  98
  99    This is not a parameter; it's a definition of unit coherence.
 100    The causal bound is that nothing propagates faster than 1 unit
 101    of length per 1 unit of time. -/
 102noncomputable def c_rs : ℝ := ℓ₀ / τ₀