GUTUnification
plain-language theorem explainer
GUTUnification packages a positive real unification scale μ_GUT in GeV with its integer rung r on the φ-ladder, satisfying μ_GUT = E_coh φ^r. Researchers deriving RS running couplings cite this structure to anchor the GUT scale above the electroweak regime. The declaration is a plain structure definition with three fields that directly encodes the ladder relation and positivity.
Claim. A structure consisting of a positive real unification scale μ_GUT (in GeV) and integer rung r on the φ-ladder such that μ_GUT = E_coh φ^r, at which the three Standard Model couplings converge.
background
The RunningCouplings module derives renormalization-group flows from the RS φ-ladder. The anchor scale μ* = 182.201 GeV is a stationarity point of the flow, and the β-function takes the form β(g) = (1/ln φ) dg/dr via the ladder derivative. Upstream, the unification theorem states that a recognizer automatically supplies the three definitional Aristotelian conditions (Identity, Non-Contradiction, Totality) on its event space together with the primitive observer, provided the event space is non-trivially populated.
proof idea
This is a structure definition with three fields: the real scale μ_GUT, the integer rung, and the positivity hypothesis 0 < μ_GUT. No tactics or lemmas are applied; the declaration simply packages the data required by downstream statements such as gut_above_ew.
why it matters
The structure supplies the hypothesis for the theorem gut_above_ew that places the GUT scale above the electroweak scale. It realizes the RS prediction that unification occurs on the φ-ladder, consistent with T5 J-uniqueness, T6 phi fixed point, and the eight-tick octave. It closes the interface between recognizer-induced logic and the running-coupling formulas in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.