def definition def or abbrev

`wallpaper_groups`

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

formal statement (Lean)

  78def wallpaper_groups : ℕ := 17

proof body

Definition body.

  79
  80/-- Face-wallpaper pairs. -/

used by (40)

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

alpha_ingredients_from_D3_cube in IndisputableMonolith.Constants.AlphaDerivation decl_use
seam_denominator in IndisputableMonolith.Constants.AlphaDerivation decl_use
wallpaper_groups in IndisputableMonolith.Constants.AlphaDerivation decl_use
AlphaFrameworkCert in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
delta_1_neg in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
face_wallpaper_pairs in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
r0_DownQuark_eq in IndisputableMonolith.Masses.Anchor decl_use
r0_Electroweak_eq in IndisputableMonolith.Masses.Anchor decl_use
r0_Lepton_eq in IndisputableMonolith.Masses.Anchor decl_use
r0_UpQuark_eq in IndisputableMonolith.Masses.Anchor decl_use
r_lepton_values in IndisputableMonolith.Masses.Anchor decl_use
tau_values in IndisputableMonolith.Masses.Anchor decl_use
W in IndisputableMonolith.Masses.Anchor decl_use
Z in IndisputableMonolith.Masses.Anchor decl_use
r0_eq_alt in IndisputableMonolith.Masses.AnchorDerivation decl_use
Wz in IndisputableMonolith.Masses.AnchorDerivation decl_use
Wz_eq in IndisputableMonolith.Masses.AnchorDerivation decl_use
generation_ordering in IndisputableMonolith.Masses.BaselineDerivation decl_use
lepton_rungs in IndisputableMonolith.Masses.BaselineDerivation decl_use
quark_rungs in IndisputableMonolith.Masses.BaselineDerivation decl_use
total_geometric_content in IndisputableMonolith.Masses.BaselineDerivation decl_use
W_endo in IndisputableMonolith.Masses.BaselineDerivation decl_use
W_endo_at_D3 in IndisputableMonolith.Masses.BaselineDerivation decl_use
lepton_integer_slot_iff_bundle_no_hk in IndisputableMonolith.Masses.JCostPerturbation decl_use
lepton_real_scale_iff_bundle_no_hc_pos in IndisputableMonolith.Masses.JCostPerturbation decl_use
o4_slot_forcing_certificate in IndisputableMonolith.Masses.JCostPerturbation decl_use
step_mu_tau_channel_split in IndisputableMonolith.Masses.JCostPerturbation decl_use
step_mu_tau_coeff_iff_full_forced_under_dim_bound in IndisputableMonolith.Masses.JCostPerturbation decl_use
step_mu_tau_coeff_iff_full_forced_under_dim_bound_no_hk in IndisputableMonolith.Masses.JCostPerturbation decl_use
step_mu_tau_coeff_iff_kn_under_dim_bound in IndisputableMonolith.Masses.JCostPerturbation decl_use

… and 10 more

depends on (1)

Lean names referenced from this declaration's body.

wallpaper_groups in IndisputableMonolith.Constants.AlphaDerivation decl_use