delta_n
plain-language theorem explainer
The definition of the n-th order voxel-seam correction δ_n as the sum of supplied real weights over the finite set of ordered n-fold face-wallpaper configurations on Q₃. Researchers extending the Recognition Science series for α^{-1} beyond first order would cite this when assembling higher terms in the expansion. It is a direct summation definition over the Fin-indexed weights of type VoxelSeamCorrection.
Claim. $\delta_n = \sum_{i \in \mathrm{Fin}(k_n)} w(i)$, where $k_n$ is the number of ordered n-fold face-wallpaper configurations and $w$ assigns a real weight to each configuration.
background
The module develops higher-order corrections to the fine-structure constant in Recognition Science. The target series is $\alpha^{-1} = \alpha_{\mathrm{seed}} - f_{\mathrm{gap}} + \sum_{n=1}^\infty \delta_n$, where each $\delta_n$ sums weighted corrections over n-fold configurations on the cube Q₃ using the $\mathbb{Z}_2^5$ half-period measure.
VoxelSeamCorrection n is the type of weight functions Fin (n_fold_configs n) → ℝ. The count n_fold_configs n equals (face_wallpaper_pairs)^n, with face_wallpaper_pairs drawn from the cube combinatorics proved in the same module.
Upstream structures include the forcing of SU(3)×SU(2)×U(1) and three generations from SpectralEmergence, together with the J-cost and ledger factorization from PhiForcingDerived and DAlembert.
proof idea
One-line definition that directly sums the weights over the Fin-indexed set of n-fold configurations supplied by n_fold_configs.
why it matters
This definition supplies the general term for the series that targets the ~8 ppm residual between the first-order α^{-1} approximation and CODATA. It completes the framework for arbitrary-order δ_n after the proved cube combinatorics and δ₁ structure, with the explicit δ₂ computation remaining open. It directly implements the combinatorial sum described in the module doc-comment for extending the geometric seed α_seed = 4π × 11.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.