T_min

formal source

  93m ∝ φ^(r − r_vac), giving offset −T_min = −8. -/
  94
  95/-- The Hamiltonian cycle period on Q_D equals the vertex count 2^D. -/
  96def T_min (d : ℕ) : ℕ := cube_vertices d
  97
  98/-- At D = 3: T_min = 8. -/
  99theorem T_min_at_D3 : T_min D = 8 := by native_decide
 100
 101/-- **B-15 DERIVED**: The octave offset is −T_min.
 102    The vacuum rung equals one complete Hamiltonian cycle period. -/
 103def octave_offset : ℤ := -(T_min D : ℤ)
 104
 105theorem octave_offset_eq : octave_offset = -8 := by
 106  unfold octave_offset T_min cube_vertices D
 107  norm_num
 108
 109/-! ## B-13: Neutrino baseline rung = −(V + E + F + E_pass + W)
 110
 111The neutrino sector is neutral (Q = 0, gap = 0) and probes the total
 112geometric content of Q₃. The baseline rung magnitude equals the sum
 113of ALL independent cube-geometric integers. The sign is negative because
 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