pith. machine review for the scientific record. sign in
theorem proved tactic proof

c_pos

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 110theorem c_pos : c_rs > 0 := by rw [c_rs_eq_one]; norm_num

proof body

Tactic-mode proof.

 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.
 141
 142    G ~ ℓ₀³/(τ₀² · M₀) where M₀ is the fundamental mass.
 143
 144    In RS-native units with natural mass scale M₀ = 1/φ^5:
 145    G = ℓ₀³ · φ^5 / τ₀² = 1 · φ^5 / 1 = φ^5. -/

used by (22)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (23)

Lean names referenced from this declaration's body.