seam_denominator_at_D3
plain-language theorem explainer
The seam denominator for spatial dimension three evaluates to 102 as the product of six cube faces and seventeen wallpaper groups. Researchers assembling the curvature term in the fine-structure constant derivation would cite this normalization to fix the denominator in the fraction 103 over 102 pi to the fifth. The result follows directly from the definition of seam_denominator as cube faces times wallpaper groups evaluated at D equals three. The proof is a one-line native decision confirming the arithmetic identity.
Claim. For spatial dimension $D=3$, the seam denominator equals $6$ times $17$, hence $102$, where the factor of six is the number of faces of the unit cube and seventeen is the number of wallpaper groups in the crystallographic closure.
background
The Alpha Derivation module constructs the fine-structure constant from the geometry of the cubic ledger on Z cubed. The unit cell is the three-dimensional cube Q3 with six faces, twelve edges, and eight vertices. The seam denominator is defined as the product of cube faces and wallpaper groups, supplying the base normalization for the curvature fraction in the topological closure step. Upstream, the seam_denominator definition states that this product is the denominator of the curvature fraction, while D is fixed at three by the forcing chain that links recognition to three spatial dimensions.
proof idea
The proof is a one-line wrapper that applies native_decide to the equality seam_denominator D equals 102. No additional lemmas are invoked beyond the definition of seam_denominator as cube_faces D times wallpaper_groups and the concrete value D equals three.
why it matters
This theorem supplies the denominator 102 that appears in the curvature term -103 over 102 pi to the fifth, which is assembled in curvature_term_eq and then used by curvature_correction_eq_formula, curvature_power_family_matches_derived_iff, and seam_ratio_from_topology. It completes the topological normalization step in the alpha derivation from the cubic ledger, consistent with D equals three from the unified forcing chain and the eight-tick octave. The result closes the seam count that feeds the curvature correction and exponent uniqueness statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.