coupling_geometric_factors
plain-language theorem explainer
The theorem asserts that the geometric seed factor equals 11 and the number of wallpaper groups equals 17. Researchers deriving the electromagnetic and strong gauge couplings from Recognition Science ledger geometry cite these fixed constants to anchor the formulas for α and α_s. The proof splits the conjunction and invokes the upstream equality theorem for the seed factor together with reflexivity on the wallpaper definition.
Claim. The geometric seed factor, defined as the count of passive field edges in three dimensions, equals 11, and the number of distinct two-dimensional wallpaper groups equals 17.
background
The module derives all three Standard Model gauge couplings from Recognition Science ledger geometry without free parameters. The geometric seed factor is the passive edge count passive_field_edges D, which equals 11 because the cube has 12 edges and one is active. The wallpaper_groups constant is the crystallographic count of 17 distinct 2D groups, used as the denominator for the strong coupling fraction 2/17.
proof idea
The term proof applies the constructor tactic to split the conjunction. It invokes the upstream theorem geometric_seed_factor_eq_11 for the first conjunct. For the second conjunct it unfolds the definition of wallpaper_groups and applies reflexivity.
why it matters
This supplies the two geometric constants required for the C-014 derivations of α^{-1} = 4π·11·exp(...) and α_s = 2/17. It feeds the unification hint that the three couplings converge near the GUT scale from RS ledger structure. The result closes the input layer for the sibling derivations of the individual couplings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.