def
definition
ledger_bilateral_factor
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.ElectronMass.Defs on GitHub at line 80.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
77- Factor 4 = N_sec = 2^(D-1) = number of fermion sectors at D = 3 -/
78
79/-- Ledger bilateral factor: reciprocal pairing (Tr4) doubles the passive count. -/
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