gut_above_ew
plain-language theorem explainer
The theorem shows that the GUT unification scale exceeds the RS anchor scale only when the unification scale itself is positive. A physicist constructing grand-unification models on the Recognition Science φ-ladder would cite this to enforce consistent scale ordering before running couplings. The proof is a one-line term that unfolds the anchor-scale definition and applies linear arithmetic.
Claim. Let $G$ be a GUTUnification structure with unification scale $μ_{GUT}$. If the RS anchor scale $μ^*$ satisfies $μ^* < μ_{GUT}$, then $0 < μ_{GUT}$.
background
The module treats renormalization-group flow on the RS φ-ladder. The anchor scale $μ^* = 182.201$ GeV is defined as a stationarity point of the flow; the β-function sign follows from the ladder derivative of the coupling, and asymptotic freedom holds for $n_f ≤ 16$. The GUTUnification structure requires that the three Standard-Model couplings meet at $μ_{GUT}$, which must lie on an integer rung of the φ-ladder, together with the standing hypothesis that $μ_{GUT}$ is positive.
proof idea
The proof is a one-line term. It receives the hypothesis $h : rs_anchor_scale < gut.μ_GUT$, unfolds the definition of rs_anchor_scale inside $h$, and invokes linarith to obtain $0 < gut.μ_GUT$.
why it matters
The result closes the elementary consistency requirement that any GUT scale placed above the RS anchor must be positive, thereby licensing the subsequent running-coupling formulas in the same module. It directly supports the claim that the GUT scale lies on the φ-ladder above the electroweak regime. No downstream theorems are recorded, leaving the hierarchy check as a local safeguard rather than a global lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.