def definition def or abbrev

`W_endo`

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

formal statement (Lean)

  29def W_endo (d : ℕ) : ℕ := passive_field_edges d + cube_faces d

Definition body.

  30
  31/-- At D = 3: W_endo = 11 + 6 = 17. -/

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

generation_ordering_general in IndisputableMonolith.Masses.BaselineDerivation decl_use
W_endo in IndisputableMonolith.Masses.BaselineDerivation decl_use
W_endo_at_D3 in IndisputableMonolith.Masses.BaselineDerivation decl_use
dimension_unique_from_W_endo in IndisputableMonolith.Physics.WEndoForcing decl_use
W_decomposition in IndisputableMonolith.Physics.WEndoForcing decl_use
W_endo_at_1 in IndisputableMonolith.Physics.WEndoForcing decl_use
W_endo_at_2 in IndisputableMonolith.Physics.WEndoForcing decl_use
W_endo_at_3 in IndisputableMonolith.Physics.WEndoForcing decl_use
W_endo_at_4 in IndisputableMonolith.Physics.WEndoForcing decl_use
W_endo_at_5 in IndisputableMonolith.Physics.WEndoForcing decl_use
W_endo_eq_17_iff in IndisputableMonolith.Physics.WEndoForcing decl_use
W_endo_eq_wallpaper in IndisputableMonolith.Physics.WEndoForcing decl_use
W_endo_gt_17_of_ge_4 in IndisputableMonolith.Physics.WEndoForcing decl_use

Lean names referenced from this declaration's body.

cube_faces in IndisputableMonolith.Constants.AlphaDerivation decl_use
passive_field_edges in IndisputableMonolith.Constants.AlphaDerivation decl_use
cube_faces in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
W_endo in IndisputableMonolith.Masses.BaselineDerivation decl_use
cube_faces in IndisputableMonolith.Physics.PMNSCorrections decl_use