z_pred_eq
plain-language theorem explainer
z_pred_eq establishes the explicit form of the Recognition Science Z boson mass prediction as exactly 2 phi^51 over one million in MeV units. Researchers verifying electroweak sector outputs against the phi-ladder mass formula would cite this equality when bounding numerical predictions. The tactic proof unfolds the rs_mass_MeV definition, substitutes the Electroweak sector constants, and reduces the resulting phi powers via zpow addition and norm_num.
Claim. $z_{pred} = 2 phi^{51} / 10^6$ (in MeV), where $z_{pred}$ denotes the Recognition Science mass prediction for the Z boson obtained by evaluating the sector mass formula at rung 1.
background
In the ElectroweakMasses module the Z boson occupies rung 1 of the phi-ladder inside the Electroweak sector. The helper rs_mass_MeV(s, r) is defined as (2)^(B_pow s) * phi^(-5) * phi^(r0 s) * phi^r / 1000000. The upstream theorems B_pow_Electroweak_eq and r0_Electroweak_eq fix B_pow .Electroweak = 1 and r0 .Electroweak = 55, so z_pred reduces to the stated power after exponent arithmetic. These constants descend from the Anchor module and ultimately from the Constants structure in LawOfExistence together with the structural conditions extracted by PrimitiveDistinction.from.
proof idea
The tactic proof first unfolds z_pred and rs_mass_MeV, then simp-substitutes B_pow_Electroweak_eq and r0_Electroweak_eq. It introduces an auxiliary equality that merges the three phi powers via zpow_add₀ and norm_num. A conv_lhs block reassociates the product, applies the merged exponent, converts via zpow_natCast, and finishes with simp on zpow_one.
why it matters
The equality supplies the closed expression required by the downstream theorem z_mass_bounds, which locates the prediction inside the interval (91075.09, 91075.10) MeV. It realizes the MODULE_DOC mechanism that assigns the Z boson directly to rung 1 while deriving W and Higgs masses from it via the Weinberg angle. Within the Recognition Science framework the result instantiates the mass formula yardstick * phi^(rung) on the phi-ladder after the eight-tick octave and D=3 have fixed the sector parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.