def
definition
alpha_inv_formula
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RRF.Foundation.Constants on GitHub at line 101.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
98- 45 = rung of biological octave
99- curvature_correction ≈ 0.05
100-/
101noncomputable def alpha_inv_formula (geometric_seed curvature_corr : ℝ) : ℝ :=
102 geometric_seed + curvature_corr
103
104/-- The geometric seed: 128 · ln(π/2) + 45 · ln φ. -/
105noncomputable def geometric_seed : ℝ :=
106 128 * Real.log (Real.pi / 2) + 45 * Real.log phi
107
108/-- α⁻¹ ≈ 137.036 (the empirical value). -/
109noncomputable def alpha_inv_empirical : ℝ := 137.036
110
111/-! ## Gravitational Constant -/
112
113/-- G derived from the Planck gate identity.
114
115(c³ · λ_rec²) / (ℏ · G) = 1/π
116
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)