theorem proved term proof

`r0_Electroweak_eq`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 118theorem r0_Electroweak_eq : r0 .Electroweak = 55 := by

Term-mode proof.

 119  simp only [r0, W, wallpaper_groups]
 120  norm_num
 121
 122/-- Sector yardstick `A_s = 2^{B_pow} * E_coh * φ^{r0}`. -/

From the project-wide theorem graph. These declarations reference this one in their body.

electroweak_sector_params in IndisputableMonolith.Masses.BosonVerification decl_use
z_pred_eq in IndisputableMonolith.Masses.ElectroweakMasses decl_use

Lean names referenced from this declaration's body.

wallpaper_groups in IndisputableMonolith.Constants.AlphaDerivation decl_use
wallpaper_groups in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
B_pow in IndisputableMonolith.Masses.Anchor decl_use
r0 in IndisputableMonolith.Masses.Anchor decl_use
Sector in IndisputableMonolith.Masses.Anchor decl_use
W in IndisputableMonolith.Masses.Anchor decl_use
yardstick in IndisputableMonolith.Masses.Anchor decl_use
yardstick in IndisputableMonolith.Masses.AnchorPolicy decl_use
Sector in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
Sector in IndisputableMonolith.Masses.RungConstructor.Basic decl_use
W in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
W in IndisputableMonolith.Physics.MassTopology decl_use
Sector in IndisputableMonolith.RSBridge.Anchor decl_use