geometricMixing
plain-language theorem explainer
geometricMixing computes the base electroweak mixing ratio directly from the phase counts in an EightTickGeometry record, returning u1_phases divided by the sum of su2_phases and u1_phases. Electroweak unification work in Recognition Science cites this when extracting the starting sin²θ_W value from the 8-tick discrete phase space before applying φ corrections. The definition is a one-line field extraction and division with no further computation.
Claim. The geometric mixing ratio is defined by $r = n_{U(1)} / (n_{SU(2)} + n_{U(1)})$, where the eight-tick geometry allocates $n_{SU(2)} = 3$ phases to the SU(2) sector and $n_{U(1)} = 1$ phase to the U(1) sector.
background
The module derives the Weinberg angle θ_W from Recognition Science φ-structure via 8-tick phase geometry. The eight-tick circle supplies eight equally spaced phases at angles kπ/4; electroweak mixing is realized by embedding SU(2) on three of these phases and U(1) on one phase, with the resulting ratio constrained by the geometric arrangement. EightTickGeometry is the structure carrying su2_phases : ℕ := 3, u1_phases : ℕ := 1 and total : ℕ := 8; the module states that the golden cut of this circle supplies the base mixing angle.
proof idea
The definition is a direct one-line extraction: it casts the u1_phases and su2_phases fields of the supplied EightTickGeometry record to ℝ and returns their ratio.
why it matters
This definition supplies the base ratio evaluated by the downstream theorem simple_geometric_ratio, which obtains the value 1/4. It realizes the 8-tick octave (T7) for electroweak mixing inside the Recognition Science derivation of θ_W from φ-optimization, as stated in the module target. The observed sin²(θ_W) ≈ 0.2229 at the Z scale then requires the separate φ-ladder correction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.