`c_pos`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.ConstantDerivations
domain: Foundation
line: 110 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.ConstantDerivations on GitHub at line 110.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 107  norm_num
 108
 109/-- c > 0. -/
 110theorem c_pos : c_rs > 0 := by rw [c_rs_eq_one]; norm_num
 111
 112/-! ## Planck's Constant: ℏ = E_coh · τ₀ -/
 113
 114/-- **Planck's reduced constant** in RS-native units.
 115
 116    ℏ is the product of coherence energy and fundamental time.
 117    This sets the scale of the IR gate (minimum action for coherent state).
 118
 119    In RS-native units: ℏ = φ^(-5) · 1 = φ^(-5). -/
 120noncomputable def ℏ_rs : ℝ := E_coh * τ₀
 121
 122/-- ℏ = φ^(-5) in RS-native units. -/
 123theorem ℏ_rs_eq : ℏ_rs = φ_val^(-5 : ℤ) := by
 124  unfold ℏ_rs E_coh τ₀
 125  ring
 126
 127/-- ℏ > 0. -/
 128theorem ℏ_pos : ℏ_rs > 0 := by
 129  rw [ℏ_rs_eq]
 130  exact zpow_pos phi_pos (-5)
 131
 132/-- ℏ is algebraic in φ. -/
 133theorem ℏ_algebraic_in_φ : ∃ n : ℤ, ℏ_rs = φ_val^n := ⟨-5, ℏ_rs_eq⟩
 134
 135/-! ## Gravitational Constant: G -/
 136
 137/-- **Gravitational constant** in RS-native units.
 138
 139    G emerges as the curvature extremum in recognition geometry.
 140    The derivation involves the holographic bound and ledger capacity.

papers checked against this theorem

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