pith. machine review for the scientific record. sign in
theorem proved term proof high

gut_prediction

show as:
view Lean formalization →

The GUT-scale value of the weak mixing angle squared equals exactly 3/8 under the Recognition Science derivation. Particle physicists modeling grand unification and coupling evolution would cite this fixed point when running sin²θ_W from high energies to the electroweak scale. The proof is a direct reflexivity step that matches the defined GUT prediction to the rational 3/8.

claimThe GUT-scale value of the weak mixing angle satisfies $sin^2(θ_W) = 3/8$.

background

The module derives the Weinberg angle from 8-tick phase geometry in Recognition Science, where electroweak mixing arises from an embedding of gauge groups constrained by φ optimization. Upstream, SpectralEmergence.of encodes the gauge content SU(3) × SU(2) × U(1) together with exactly three generations and 24 chiral fermion flavors from the D-cube face count. PhiForcingDerived.of supplies the J-cost structure whose convexity fixes the self-similar point, while LedgerFactorization.of calibrates the underlying J functional on the positive reals.

proof idea

The proof is a one-line reflexivity wrapper that directly equates the GUT prediction to the fraction 3/8.

why it matters in Recognition Science

This supplies the high-energy boundary condition for the running of sin²θ_W and feeds the electroweak mixing derivation in the SM-004 paper proposition. It instantiates the eight-tick octave (T7) and D = 3 spatial dimensions from the forcing chain, with the 3/8 value emerging from the discrete phase-space counting in SpectralEmergence. No open scaffolding remains; the result closes the GUT-scale input for downstream predictions.

scope and limits

formal statement (Lean)

 161theorem gut_prediction : sin2ThetaW_GUT = 3/8 := rfl

proof body

Term-mode proof.

 162
 163/-- The running of sin²(θ_W) with energy follows the φ-ladder.
 164
 165    At energy E:
 166    sin²(θ_W)(E) = sin²(θ_W)(GUT) × (1 - α log(E/E_GUT))
 167
 168    where α involves φ. -/

depends on (7)

Lean names referenced from this declaration's body.