runningAngle
plain-language theorem explainer
The runningAngle definition supplies the logarithmic energy dependence of sin²(θ_W) in Recognition Science units. Electroweak unification studies cite it when matching RS predictions against collider running data. It is a direct algebraic scaling from the GUT-scale value using a one-loop logarithmic correction drawn from the φ-ladder.
Claim. The running weak mixing parameter is given by $sin^2 θ_W (log E) = sin^2 θ_W^{GUT} (1 - log E / (16 π^2))$, where the coefficient follows from φ-optimization on the eight-tick ladder.
background
The StandardModel.WeinbergAngle module derives θ_W from the 8-tick phase geometry of Recognition Science. The fundamental tick τ₀ = 1 supplies the discrete time quantum, while the φ-ladder governs all scaling relations including gauge mixing. Upstream constants fix Charge and Mass in RS-native units and enforce the one-octave period of eight ticks.
proof idea
This is a definition that directly encodes the running formula stated in the doc-comment: multiply the GUT value by the linear term (1 - logEnergy / (16 π²)). No lemmas are applied; the body is the explicit algebraic expression.
why it matters
It fills the energy-running step required by the module's core result on electroweak mixing from φ-structure, feeding the sibling prediction functions. The construction realizes the T7 eight-tick octave landmark and the coupling-unification clause in the PRL paper proposition. No open scaffolding remains inside the declaration itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.