module
public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
public import Mathlib.Tactic

@[expose] public section
noncomputable section
namespace VibeQCCore
open scoped BigOperators

/-- An explicit bijection certifies that each physical orbit has two directed entries. -/
theorem pair_orbit_accounting {P R : Type*} [Fintype P] [Fintype R]
    (encode : R × Bool ≃ P) (e : P → ℝ)
    (symmetric : ∀ r, e (encode (r, false)) = e (encode (r, true))) :
    (1 / 2 : ℝ) * (∑ p, e p) = ∑ r, e (encode (r, false)) := by
  rw [← Equiv.sum_comp encode]
  simp only [Fintype.sum_prod_type, Fintype.sum_bool]
  simp_rw [← symmetric]
  rw [Finset.sum_add_distrib]
  ring

/-- Molecular ordered pairs, with the diagonal excluded explicitly. -/
theorem molecular_pair_accounting {n : ℕ} (e : Fin n → Fin n → ℝ)
    (symmetric : ∀ i j, e i j = e j i) :
    (1 / 2 : ℝ) * (∑ i, ∑ j, if i ≠ j then e i j else 0) =
      ∑ i, ∑ j, if i < j then e i j else 0 := by
  classical
  have split : ∀ i j : Fin n,
      (if i ≠ j then e i j else 0) =
      (if i < j then e i j else 0) + (if j < i then e i j else 0) := by
    intro i j
    rcases lt_trichotomy i j with h | h | h <;> simp [ne_of_lt, ne_of_gt, not_lt_of_ge, le_of_lt, *]
  simp_rw [split, Finset.sum_add_distrib]
  have swap : (∑ i, ∑ j, if j < i then e i j else 0) =
      ∑ i, ∑ j, if i < j then e i j else 0 := by
    rw [Finset.sum_comm]
    apply Finset.sum_congr rfl
    intro i hi
    apply Finset.sum_congr rfl
    intro j hj
    rw [symmetric]
  rw [swap]
  ring

theorem normalization_sum {I : Type*} [Fintype I] (e : I → ℝ) (count : ℝ) :
    (∑ i, e i) / count = ∑ i, e i / count := by
  simp [div_eq_mul_inv, Finset.sum_mul]

theorem normalized_components (electronic nuclear count : ℝ) :
    (electronic + nuclear) / count = electronic / count + nuclear / count := by ring

/-- This proves normalization only; the selected set must separately be shown complete. -/
theorem uniform_boundary_weights {I : Type*} (s : Finset I) (nonempty : s.Nonempty) :
    (∑ _i ∈ s, (1 / (s.card : ℝ))) = 1 := by
  have hn : (s.card : ℝ) ≠ 0 := by exact_mod_cast (Finset.card_ne_zero.mpr nonempty)
  simp [Finset.sum_const, nsmul_eq_mul, hn]

end VibeQCCore