theorem proved term proof

`B_pow_Electroweak_eq`

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

formal statement (Lean)

 102theorem B_pow_Electroweak_eq : B_pow .Electroweak = 1 := by

Term-mode proof.

 103  simp only [B_pow, A, active_edges_per_tick]
 104  norm_num
 105

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.

active_edges_per_tick in IndisputableMonolith.Constants.AlphaDerivation decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
B_pow in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use