def
definition
partial_alpha
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Constants.AlphaHigherOrder on GitHub at line 161.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
158 ∑ i : Fin (n_fold_configs n), weights i
159
160/-- The partial sum of the series up to order N. -/
161def partial_alpha (alpha_s f_g : ℝ) (deltas : ℕ → ℝ) (N : ℕ) : ℝ :=
162 alpha_s - f_g + (Finset.range N).sum (fun n => deltas (n + 1))
163
164/-! ## CODATA Target -/
165
166/-- CODATA 2022 value of α⁻¹. -/
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)