total_geometric_content

formal source

 114neutrinos sit deep below the vacuum on the φ-ladder. -/
 115
 116/-- Total geometric content of Q_D: sum of all independent structural integers. -/
 117def total_geometric_content (d : ℕ) : ℕ :=
 118  cube_vertices d + cube_edges d + cube_faces d +
 119  passive_field_edges d + wallpaper_groups
 120
 121/-- At D = 3: total geometric content = 8 + 12 + 6 + 11 + 17 = 54. -/
 122theorem total_geometric_at_D3 : total_geometric_content D = 54 := by native_decide
 123
 124/-- **B-13 DERIVED**: The neutrino baseline integer rung. -/
 125def neutrino_baseline_int : ℤ := -(total_geometric_content D : ℤ)
 126
 127theorem neutrino_baseline_eq : neutrino_baseline_int = -54 := by
 128  unfold neutrino_baseline_int
 129  rw [total_geometric_at_D3]
 130  norm_num
 131
 132/-! ## B-11: Lepton baseline rung = A + 1
 133
 134The electron is the lightest charged particle. A charged state must
 135traverse at least one edge of Q₃ (the active edge A = 1) to register
 136a charge. The active edge itself is the transition mechanism, not a
 137stable particle. The minimal stable charged state sits one rung above:
 138r_e = A + 1 = 2. -/
 139
 140/-- **B-11 DERIVED**: The lepton baseline rung from cube geometry. -/
 141def lepton_baseline : ℕ := active_edges_per_tick + 1
 142
 143theorem lepton_baseline_eq : lepton_baseline = 2 := by
 144  unfold lepton_baseline active_edges_per_tick
 145  norm_num
 146
 147/-- Consistency: matches the hardcoded value in Anchor.lean. -/