structure
definition
AlphaPrecisionHypothesis
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.AlphaHigherOrder on GitHub at line 170.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
167def CODATA_alpha_inv : ℝ := 137.035999206
168
169/-- The precision hypothesis: the full series converges to CODATA. -/
170structure AlphaPrecisionHypothesis where
171 deltas : ℕ → ℝ
172 delta_1_matches : deltas 1 = delta_1
173 converges_to_CODATA : Filter.Tendsto
174 (fun N => partial_alpha alpha_seed (deltas 1) deltas N) Filter.atTop
175 (nhds CODATA_alpha_inv)
176
177/-! ## Bounds on δ₂ -/
178
179/-- The residual between additive formula and CODATA.
180 This is the amount the remaining δ_n terms must sum to. -/
181def additive_residual (w8_val : ℝ) : ℝ :=
182 CODATA_alpha_inv - (alpha_seed - f_gap w8_val + delta_1)
183
184/-- The exponential overshoot above CODATA. -/
185def exponential_residual (w8_val : ℝ) : ℝ :=
186 alpha_seed * Real.exp (-(f_gap w8_val) / alpha_seed) - CODATA_alpha_inv
187
188/-- The gap between exponential and additive formulas bounds δ₂ (if alternating). -/
189theorem exp_minus_add_pos
190 (w8_val : ℝ)
191 (h_add : alpha_seed - f_gap w8_val + delta_1 < CODATA_alpha_inv)
192 (h_exp : CODATA_alpha_inv < alpha_seed * Real.exp (-(f_gap w8_val) / alpha_seed)) :
193 0 < alpha_seed * Real.exp (-(f_gap w8_val) / alpha_seed) -
194 (alpha_seed - f_gap w8_val + delta_1) := by
195 linarith
196
197/-! ## Certificate -/
198
199/-- Framework certificate: all structural elements are in place for δ₂ computation. -/
200structure AlphaFrameworkCert where