all_threes_unified

formal source

 327    Fintype.card (Fin D) = D := Fintype.card_fin D
 328
 329/-- All the "3"s are the same "3". -/
 330theorem all_threes_unified :
 331    -- Number of winding charges
 332    Fintype.card (Fin 3) = 3 ∧
 333    -- Number of face-pairs
 334    ParticleGenerations.face_pairs 3 = 3 ∧
 335    -- Number of colors
 336    QuarkColors.N_colors 3 = 3 ∧
 337    -- Number of SM charges
 338    Fintype.card SMCharge = 3 ∧
 339    -- Topological charge count
 340    independent_charge_count 3 = 3 := by
 341  exact ⟨Fintype.card_fin 3, rfl, rfl, sm_charge_count, three_charges_at_D3⟩
 342
 343/-! ## Part 9: Closed Paths and Linking -/
 344
 345/-- A path is **closed** if its total displacement is zero along every axis.
 346    Closed paths on ℤ³ are the analogues of loops in topology. -/
 347def is_closed {D : ℕ} (p : LatticePath D) : Prop :=
 348  ∀ k : Fin D, winding_number p k = 0
 349
 350/-- The empty path is closed. -/
 351theorem empty_is_closed {D : ℕ} : is_closed ([] : LatticePath D) :=
 352  fun k => winding_empty k
 353
 354/-- A cancelling pair is a closed path. -/
 355theorem cancelling_pair_closed {D : ℕ} (a : Fin D) :
 356    is_closed ([LatticeStep.plus a, LatticeStep.minus a] : LatticePath D) := by
 357  intro k
 358  simp [winding_number, step_displacement]
 359  split <;> simp
 360