`Sector`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Masses.Anchor on GitHub at line 67.

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

  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
  86  | .Electroweak => 3 * (W : ℤ) + 4             -- = 3 × 17 + 4 = 55
  87
  88/-! ## Verification: Derived values match expected integers -/
  89
  90theorem B_pow_Lepton_eq : B_pow .Lepton = -22 := by
  91  simp only [B_pow, E_passive, passive_field_edges, cube_edges, active_edges_per_tick, D]
  92  norm_num
  93
  94theorem B_pow_UpQuark_eq : B_pow .UpQuark = -1 := by
  95  simp only [B_pow, A, active_edges_per_tick]
  96  norm_num
  97

papers checked against this theorem

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