A

formal source

  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
  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]