rs_hierarchy
plain-language theorem explainer
The theorem establishes that the observed electroweak vacuum expectation value lies more than fifteen orders of magnitude below the Planck scale. Researchers addressing the hierarchy problem in the Standard Model would cite this numerical bound when comparing the Higgs VEV to gravitational scales. The proof is a direct tactic application that unfolds the observed VEV definition and reduces the inequality by numerical normalization.
Claim. Let $M_{Planck} = 1.22 times 10^{19}$ GeV. Then the observed vacuum expectation value $v_{obs}$ satisfies $v_{obs}/M_{Planck} < 10^{-15}$.
background
The module derives electroweak symmetry breaking from the J-cost functional, identifying the Higgs potential with the Recognition Science cost and the vacuum expectation value with its minimum. In this setting the spontaneous breaking SU(2)_L times U(1)_Y to U(1)_EM follows from ledger selection of a J-cost-minimizing configuration. Upstream results supply the RS-native units (c = 1, tau_0 = 1 tick) and the phi-ladder structure of physical quantities used to interpret scale ratios.
proof idea
The tactic proof unfolds the definition of the observed VEV and applies norm_num to discharge the numerical inequality directly.
why it matters
The result anchors the RS hierarchy discussion inside the electroweak module by confirming the extreme scale separation required for naturalness via phi-ladder rungs. It feeds the broader claim that v/M_Pl is a high negative power of phi, although the exact exponent remains under investigation as noted in the module documentation. The declaration therefore closes a concrete numerical step in the T5-T8 forcing chain while leaving the precise phi-power matching open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.