alpha_ingredients_from_D3_cube
plain-language theorem explainer
The declaration verifies that the geometric seed factor equals total cube edges minus the single active edge per tick, the seam numerator equals cube faces times wallpaper groups plus Euler closure, and the seam denominator equals cube faces times wallpaper groups, all evaluated at D=3. Researchers deriving the fine-structure constant from discrete geometry cite it to trace the origin of the factors 11 and 103. The proof is a direct term-mode verification by unfolding the geometric definitions.
Claim. Let $D=3$. The geometric seed factor equals the number of edges in the $D$-cube minus the active edges per tick; the seam numerator equals the number of faces in the $D$-cube times the number of wallpaper groups plus the Euler closure term; the seam denominator equals the number of faces in the $D$-cube times the number of wallpaper groups.
background
The Alpha Derivation module fixes spatial dimension at $D=3$ (T8 of the forcing chain) and models the fundamental cell as the 3-cube $Q_3$. Cube edges are defined as $D·2^{D-1}=12$, faces as $2D=6$, and active edges per tick as 1, so passive field edges equal 11. The geometric seed factor is this passive count. Seam denominator is faces times 17 wallpaper groups, giving 102; seam numerator adds the Euler closure of 1 to reach 103. Module doc states: 'Complete provenance: all magic numbers are derived from D=3 cube geometry.'
proof idea
Term-mode proof. Constructor splits the conjunction into three subgoals. Reflexivity (rfl) discharges each by direct definition unfolding of cube_edges, cube_faces, active_edges_per_tick, geometric_seed_factor, seam_numerator, seam_denominator, wallpaper_groups, and euler_closure.
why it matters
Supplies the explicit 11 and 103 ingredients that seed the alpha inverse expression in the same module, completing the geometric provenance step before curvature terms are introduced. It instantiates the D=3 cube ledger required by the Recognition Science forcing chain (T8) and the discrete recognition event per tick. No downstream theorems are listed; the result closes the seeding block inside the alpha derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.