`W`

definition

show as: view math explainer →

module: IndisputableMonolith.Masses.Anchor
domain: Masses
line: 55 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Masses.Anchor on GitHub at line 55.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  52abbrev E_passive : ℕ := passive_field_edges D
  53
  54/-- Wallpaper groups: 17 -/
  55abbrev W : ℕ := wallpaper_groups
  56
  57/-- Total cube edges: 12 -/
  58abbrev E_total : ℕ := cube_edges D
  59
  60/-- Active edges per tick: 1 -/
  61abbrev A : ℕ := active_edges_per_tick
  62
  63/-- Coherence energy unit: `E_coh = φ⁻⁵` (dimensionless; multiply by eV externally). -/
  64@[simp] noncomputable def E_coh : ℝ := Constants.phi ^ (-(5 : ℤ))
  65
  66/-- Sector identifiers. -/
  67inductive Sector | Lepton | UpQuark | DownQuark | Electroweak
  68  deriving DecidableEq, Repr
  69
  70/-! ## Sector Constants — DERIVED from Cube Geometry -/
  71
  72/-- Derived powers of two for each sector.
  73    These are NOT arbitrary—they come from cube edge counting. -/
  74@[simp] def B_pow : Sector → ℤ
  75  | .Lepton      => -(2 * (E_passive : ℤ))     -- = -(2 × 11) = -22
  76  | .UpQuark     => -(A : ℤ)                    -- = -1
  77  | .DownQuark   => 2 * (E_total : ℤ) - 1       -- = 2 × 12 - 1 = 23
  78  | .Electroweak => (A : ℤ)                     -- = 1
  79
  80/-- Derived φ-exponent offsets per sector.
  81    These are NOT arbitrary—they come from wallpaper + cube geometry. -/
  82@[simp] def r0 : Sector → ℤ
  83  | .Lepton      => 4 * (W : ℤ) - 6             -- = 4 × 17 - (8 - 2) = 62
  84  | .UpQuark     => 2 * (W : ℤ) + (A : ℤ)       -- = 2 × 17 + 1 = 35
  85  | .DownQuark   => (E_total : ℤ) - (W : ℤ)     -- = 12 - 17 = -5

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.