def
definition
N_sec
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.ElectronMass.Defs on GitHub at line 83.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
80def ledger_bilateral_factor : ℕ := 2
81
82/-- Number of fermion sectors: 2^(D-1) at D = 3. -/
83def N_sec : ℕ := 2 ^ (D - 1)
84
85theorem N_sec_eq : N_sec = 4 := by unfold N_sec D; norm_num
86
87/-! ## Lepton Sector Geometry (DERIVED, not hardcoded) -/
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