`G_derived`

definition

show as: view math explainer →

module: IndisputableMonolith.RRF.Foundation.Constants
domain: RRF
line: 120 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RRF.Foundation.Constants on GitHub at line 120.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 117Solving for G:
 118G = π · c³ · λ_rec² / ℏ
 119-/
 120noncomputable def G_derived (c hbar lambda_rec : ℝ) : ℝ :=
 121  Real.pi * c^3 * lambda_rec^2 / hbar
 122
 123/-! ## The K-Gate Identity -/
 124
 125/-- K = 2π / (8 ln φ) — the universal dimensionless ratio.
 126
 127This ratio appears in:
 128- τ_rec / τ₀ = K
 129- λ_kin / ℓ₀ = K
 130-/
 131noncomputable def K_ratio : ℝ := 2 * Real.pi / (8 * Real.log phi)
 132
 133/-- K is positive. -/
 134theorem K_ratio_pos : 0 < K_ratio := by
 135  unfold K_ratio
 136  apply div_pos
 137  · exact mul_pos (by norm_num : (0:ℝ) < 2) Real.pi_pos
 138  · apply mul_pos (by norm_num : (0:ℝ) < 8)
 139    exact Real.log_pos phi_gt_one
 140
 141/-! ## Complete Constants Bundle -/
 142
 143/-- All derived constants in one structure. -/
 144structure DerivedConstants where
 145  phi : ℝ
 146  E_coh : ℝ
 147  tau_0 : ℝ
 148  c : ℝ
 149  hbar : ℝ
 150  G : ℝ

papers checked against this theorem

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