  45
  46    k_R = ln(φ) — the fundamental cost per ledger bit.
  47    This replaces k_B in RS-native thermodynamics. -/
  48noncomputable def k_R : ℝ := Real.log Constants.phi
  49
  50/-- **THEOREM C-006.1**: k_R is positive.
  51
  52    Proof: φ > 1, so ln(φ) > 0. -/
  53theorem k_R_pos : k_R > 0 := by
  54  unfold k_R
  55  apply Real.log_pos
  56  exact Constants.one_lt_phi
  57
  58/-- **THEOREM C-006.2**: k_R is nonzero.
  59
  60    This is required for thermodynamic calculations (division by k_R). -/
  61theorem k_R_ne_zero : k_R ≠ 0 := by
  62  exact ne_of_gt k_R_pos
  63
  64/-- **THEOREM C-006.3**: k_R < 0.5.
  65
  66    Since φ < 1.62 < e^0.5 ≈ 1.6487, we have ln(φ) < 0.5.
  67    
  68    **Proof**: From φ < 1.62 and the monotonicity of ln:
  69    ln(φ) < ln(1.62). 
  70    
  71    Numerically, ln(1.62) ≈ 0.482 < 0.5.
  72    
  73    **Status**: The bound follows from φ < 1.62 and ln monotonicity.
  74    **Numerical proof**: Taylor bound exp(0.5) > 1.645 > 1.62 via Real.exp_bound. -/
  75theorem k_R_lt_half : k_R < (0.5 : ℝ) := by
  76  unfold k_R
  77  have h1 : Constants.phi < (1.62 : ℝ) := Constants.phi_lt_onePointSixTwo
  78  -- ln(φ) < ln(1.62) by monotonicity

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.