VoxelSeamCorrection
plain-language theorem explainer
The type of n-th order voxel-seam corrections is the space of real-valued assignments to each ordered n-fold face-wallpaper configuration on the cube Q3. Researchers extending the Recognition Science series for alpha inverse beyond the first-order term would cite this definition when constructing the weighted sum delta_n. The definition is a direct type alias that composes the combinatorial count of configurations with the codomain of real numbers.
Claim. The space of weights for the n-th order correction is the function space $Fin(N_n) → ℝ$, where $N_n$ denotes the number of ordered n-fold face-wallpaper configurations on the cube $Q_3$.
background
The module AlphaHigherOrder develops higher-order corrections to the fine-structure constant in Recognition Science. The target series is $α^{-1} = α_{seed} - f_{gap} + Σ δ_n$, where the first-order term already reaches within 8 ppm of the CODATA value 137.035999206. Each $δ_n$ is a finite sum over n-fold configurations on Q3, weighted by the $Z_2^5$ half-period measure. The upstream definition n_fold_configs supplies the cardinality $N_n = (face_wallpaper_pairs)^n$, while SpectralEmergence establishes that Q3 simultaneously forces the gauge group SU(3)×SU(2)×U(1) and three generations. PhiForcingDerived and DAlembert.LedgerFactorization supply the convex J-cost structure that governs admissible weights.
proof idea
The declaration is a one-line type alias that instantiates the function space over the finite set produced by n_fold_configs, directly supplying the domain required by the summation in delta_n.
why it matters
This definition supplies the type for the weight vector in delta_n, the term that computes each partial sum of the alpha inverse series. It completes the combinatorial scaffolding needed to address the open ~8 ppm residual after the first-order correction δ1 = -103/(102π^5). The module states that the full series is alternating and convergent, yet leaves explicit computation of δ2 as the key remaining deliverable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.