pith. machine review for the scientific record. sign in
theorem proved decidable or rfl high

delta_1_structure

show as:
view Lean formalization →

delta_1_structure asserts that the first-order curvature correction equals the negative ratio of the curvature numerator to the product of face-wallpaper pairs and pi to the measure dimension. Researchers assembling the alpha inverse series in Recognition Science cite this when adding the initial voxel-seam term to the geometric seed and gap weight. The proof is a single reflexivity step that matches the definition of delta_1 exactly.

claim$δ_1 = -κ / (f ⋅ π^d)$, where κ is the curvature numerator (face-wallpaper pairs plus active edges), f is the number of face-wallpaper pairs (cube faces times wallpaper groups), and d is the integration measure dimension (equal to 5).

background

The module develops higher-order voxel-seam corrections to α^{-1} inside the Recognition Science derivation. It begins from the geometric seed α_seed = 4π × 11, subtracts the gap weight f_gap = w_8 ln φ, and adds the series Σ δ_n. Each δ_n sums combinatorial face-wallpaper configurations on the Q_3 cube under the Z_2^5 half-period measure.

proof idea

The proof applies rfl. This one-line wrapper confirms the equality because the definition of delta_1 is written verbatim as the displayed ratio of curvature_numerator, face_wallpaper_pairs, and measure_dimension.

why it matters in Recognition Science

The result supplies the explicit first-order term δ_1 that feeds the alphaFramework certification of cube combinatorics. It closes the n=1 slot in the series α^{-1} = α_seed − f_gap + Σ δ_n, targeting the 8 ppm CODATA residual. The framework still leaves δ_2 computation open as the next required step.

scope and limits

formal statement (Lean)

 104theorem delta_1_structure :
 105    delta_1 = -(curvature_numerator : ℝ) / ((face_wallpaper_pairs : ℝ) * π ^ measure_dimension) :=

proof body

Decided by rfl or decide.

 106  rfl
 107

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.