coupling_formulas_distinct
plain-language theorem explainer
The declaration establishes that the electromagnetic coupling draws its geometric seed from exactly 11 passive edges, the strong coupling normalizes by the 17 wallpaper groups, and the weak mixing angle follows the expression (3 - φ)/6. A physicist deriving gauge couplings from Recognition Science ledger geometry would cite this to confirm the three couplings originate in distinct forced constants rather than free parameters. The proof is a direct term-mode construction that splits the conjunction and discharges each equality by exact lemma or
Claim. The geometric seed factor equals 11, the number of wallpaper groups equals 17, and the best prediction for the weak mixing angle satisfies $sin^2 θ_W = (3 - φ)/6$.
background
In the C-014 gauge coupling derivations the electromagnetic fine-structure constant α is seeded by the geometric seed factor, defined as the count of passive field edges in three-dimensional space and verified to equal 11. The strong coupling α_s is normalized by the wallpaper group count, the standard crystallographic constant fixed at 17 by Fedorov's 1891 classification. The weak mixing angle uses the φ-based expression (3 - φ)/6, where φ is the self-similar fixed point forced in the T5-T6 chain.
proof idea
The proof applies the constructor tactic to split the conjunction into three subgoals. The first subgoal is discharged exactly by the lemma geometric_seed_factor_eq_11. The second subgoal unfolds the definition of wallpaper_groups and reduces by reflexivity. The third subgoal unfolds bestPrediction together with prediction3 and reduces by reflexivity.
why it matters
This theorem anchors the C-014 registry item by confirming that α, α_s and sin²θ_w arise from distinct RS-forced geometric constants (11 passive edges, 17 wallpaper groups, and the φ-expression) rather than fitted parameters. It supports the module's unification hint that the couplings converge near the GUT scale because each traces to D=3 ledger geometry and the eight-tick octave. No downstream theorems depend on it yet, leaving open the embedding of these constants into a full unification proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.