lepton_B

formal source

  88
  89/-- Lepton sector binary gauge: B = -(bilateral × E_passive) = -22.
  90    The bilateral factor (= 2) comes from reciprocal pairing (Tr4). -/
  91def lepton_B : ℤ := -((ledger_bilateral_factor : ℤ) * (MassTopology.E_passive : ℤ))
  92
  93/-- PROOF: lepton_B evaluates to -22. -/
  94theorem lepton_B_eq : lepton_B = -22 := by
  95  simp only [lepton_B, ledger_bilateral_factor, MassTopology.E_passive, passive_field_edges,
  96             cube_edges, active_edges_per_tick]
  97  norm_num
  98
  99/-- Electron baseline rung: the lowest lepton generation.
 100    Derived as active_edges_per_tick + 1 = 2 (see BaselineDerivation.lean). -/
 101def electron_baseline_rung : ℤ := 2
 102
 103/-- Lepton sector geometric origin: R0 = N_sec × W - (octave - r_baseline) = 62.
 104    - N_sec = 2^(D-1) = 4 fermion sectors
 105    - W = 17 wallpaper groups (external mathematical fact)
 106    - octave = 8, r_baseline = 2 -/
 107def lepton_R0 : ℤ := (N_sec : ℤ) * (MassTopology.W : ℤ) - ((octave_period : ℤ) - electron_baseline_rung)
 108
 109/-- PROOF: lepton_R0 evaluates to 62. -/
 110theorem lepton_R0_eq : lepton_R0 = 62 := by
 111  simp only [lepton_R0, N_sec, D, MassTopology.W, wallpaper_groups, octave_period_eq,
 112             electron_baseline_rung]
 113  norm_num
 114
 115/-- The coherence exponent: 2^D - D = 8 - 3 = 5 (Fibonacci deficit).
 116    See Foundation.CoherenceExponent for the full derivation
 117    via two independent routes (Fibonacci deficit and integration measure). -/
 118def coherence_exponent : ℕ := 2 ^ D - D
 119
 120theorem coherence_exponent_eq : coherence_exponent = 5 := by
 121  unfold coherence_exponent D; norm_num