Z2_sectors_eq

formal source

 144
 145/-- Number of Z₂ half-period sectors. -/
 146def Z2_sectors : ℕ := 2 ^ half_period_dim
 147theorem Z2_sectors_eq : Z2_sectors = 32 := by native_decide
 148
 149/-! ## Series Framework -/
 150
 151/-- The general n-th order correction is a finite sum over n-fold configs
 152    weighted by the Z₂⁵ measure. This is the type of the sum. -/
 153def VoxelSeamCorrection (n : ℕ) : Type :=
 154  Fin (n_fold_configs n) → ℝ
 155
 156/-- The δ_n value: sum of weighted corrections. -/
 157def delta_n (n : ℕ) (weights : VoxelSeamCorrection n) : ℝ :=
 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 δ₂ -/