Masses Mass Genesis T10 Double Entry Mass Quantum

/--
**Main theorem.** For every integer occupation the settlement load is twice a
natural number. Proof: choose integers `n t` with `occ t = n t`, put
`d t = n t - n (t-1)`, note each tick contributes `(d t)^2` to the load, the
cycle forces `∑ d = 0`, and over `ℤ` one has `m^2 ≡ m [ZMOD 2]`, so
`∑ (d t)^2 ≡ ∑ d t = 0 [ZMOD 2]`. Nonnegativity upgrades the even integer to
`2 * k` with `k : ℕ`.
-/
theorem integerOccupation_settlementLoad_even
    (occ : Fin 8 → ℂ) (hocc : IntegerOccupation occ) :
    ∃ k : ℕ, settlementLoad occ = 2 * (k : ℝ) := by
  classical
  let n : Fin 8 → ℤ := fun t => Classical.choose (hocc t)
  have hn : ∀ t, occ t = (n t : ℂ) := fun t => Classical.choose_spec (hocc t)
  let d : Fin 8 → ℤ := fun t => n t - n (t - 1)
  have hterm : ∀ t, Complex.normSq (occ t - occ (t - 1)) = ((d t : ℤ) : ℝ) ^ 2 := by
    intro t
    rw [hn t, hn (t - 1)]
    simpa [d] using integer_diff_normSq (n t) (n (t - 1))
  have hload : settlementLoad occ = ((∑ t : Fin 8, (d t) ^ 2 : ℤ) : ℝ) := by
    rw [settlementLoad_eq_sum_normSq]
    have hsum :
        (∑ t : Fin 8, Complex.normSq (occ t - occ (t - 1))) =
          ∑ t : Fin 8, ((d t : ℤ) : ℝ) ^ 2 := by
      refine Finset.sum_congr rfl ?_
      intro t _; exact hterm t
    rw [hsum]
    simp [Int.cast_sum, Int.cast_pow]
  have hsum_d : (∑ t : Fin 8, d t) = 0 := by
    change (∑ t : Fin 8, (n t - n (t - 1))) = 0
    rw [Finset.sum_sub_distrib]
    have hbij : (∑ t : Fin 8, n (t - 1)) = ∑ t : Fin 8, n t :=
      Fintype.sum_equiv (Equiv.subRight (1 : Fin 8)) _ _ (fun t => rfl)
    rw [hbij, sub_self]
  have hdiff_even : Even (∑ t : Fin 8, ((d t) ^ 2 - d t)) :=
    even_sum_of_even (fun t => (d t) ^ 2 - d t) (fun t => even_sq_sub_self (d t))
  have hsum_sq_even : Even (∑ t : Fin 8, (d t) ^ 2) := by
    have hrewrite :
        (∑ t : Fin 8, (d t) ^ 2) =
          (∑ t : Fin 8, ((d t) ^ 2 - d t)) + ∑ t : Fin 8, d t := by
      rw [← Finset.sum_add_distrib]
      refine Finset.sum_congr rfl ?_
      intro t _
      ring
    rw [hrewrite, hsum_d, add_zero]
    exact hdiff_even
  obtain ⟨kZ, hkZ⟩ := hsum_sq_even
  have hnonneg : 0 ≤ ∑ t : Fin 8, (d t) ^ 2 :=
    Finset.sum_nonneg (fun _ _ => sq_nonneg _)
  have hkZ_nonneg : 0 ≤ kZ := by
    have : 0 ≤ kZ + kZ := by
      rw [← hkZ]
      exact hnonneg
    linarith
  refine ⟨kZ.toNat, ?_⟩
  have hkZ_eq : (kZ : ℝ) = (kZ.toNat : ℝ) := by
    exact_mod_cast (Int.toNat_of_nonneg hkZ_nonneg).symm
  rw [hload, hkZ, Int.cast_add, ← two_mul, hkZ_eq]

/-- Boolean settlement loads lie in `{0, 2, 4, 6, 8}`. -/
theorem booleanOccupation_settlementLoad_mem
    (occ : Fin 8 → ℂ) (h : BooleanOccupation occ) :
    settlementLoad occ ∈ ({0, 2, 4, 6, 8} : Set ℝ) := by
  obtain ⟨k, hk⟩ :=
    integerOccupation_settlementLoad_even occ h.integerOccupation
  have hle : settlementLoad occ ≤ 8 :=
    booleanOccupation_settlementLoad_le_eight occ h
  have hk_le : (k : ℝ) ≤ 4 := by
    have : 2 * (k : ℝ) ≤ 8 := by rw [← hk]; exact hle
    linarith
  have hk_nat : k ≤ 4 := by exact_mod_cast hk_le
  rw [hk]
  interval_cases k <;> norm_num

theorem t10DoubleEntryUnitFreeMassWallCert :
    T10DoubleEntryUnitFreeMassWallCert where
  unit_factors_out := twoValuedOccupation_settlementLoad_eq_normSq_mul_cutCount
  cutCount_even := twoValuedOccupation_cutCount_even
  cutCount_le_eight_field := cutCount_le_eight
  load_cutCount_cancel := twoValuedOccupation_load_cutCount_cancel
  unit_free_mass_ratio_le_four := twoValuedOccupation_mass_ratio_le_four
  wall_tight_at_cuts_two_and_eight := twoValuedOccupation_mass_ratio_wall_tight
  vacuum_and_full_cycle_massless :=
    ⟨twoValuedVacuum_settlementLoad, twoValuedFull_settlementLoad⟩
  three_valued_discriminates_R9 :=
    ⟨threeValuedDiscriminatingWitness_settlementLoad,
      threeValuedDiscriminatingWitness_cutCount,
      threeValuedDiscriminatingWitness_R9_fails_at_one⟩
  scope_one_eight_tick_voxel := trivial
  scope_lepton_ratios_not_addressed := trivial
  scope_posting_unit_not_derived := trivial

theorem settlementLoad_mul (lam : ℂ) (occ : Fin 8 → ℂ) :
    settlementLoad (fun t => lam * occ t) =
      Complex.normSq lam * settlementLoad occ := by
  have hsw := settlementWindow_mul lam occ
  unfold settlementLoad
  have hneut : IsNeutral (fun t => lam * settlementWindow occ t) := by
    unfold IsNeutral
    rw [← Finset.mul_sum, settlementWindow_neutral, mul_zero]
  rw [hsw, neutralize_of_neutral _ hneut, neutralize_settlementWindow]
  change
      (∑ t : Fin 8, Complex.normSq (lam * settlementWindow occ t)) =
        Complex.normSq lam *
          ∑ t : Fin 8, Complex.normSq (settlementWindow occ t)
  simp_rw [Complex.normSq_mul, ← Finset.mul_sum]

theorem scaledHalfSupportOccupation_settlementLoad
    (r : ℝ) (hr : 0 ≤ r) :
    settlementLoad (scaledHalfSupportOccupation r) = r := by
  have hnonneg : 0 ≤ r / 2 := by linarith
  set s : ℝ := Real.sqrt (r / 2)
  have hs : s * s = r / 2 := Real.mul_self_sqrt hnonneg
  have hnorm : Complex.normSq (s : ℂ) = r / 2 := by
    simp [Complex.normSq, Complex.ofReal_re, Complex.ofReal_im, hs]
  have hneg : Complex.normSq (-(s : ℂ)) = r / 2 := by
    rw [Complex.normSq_neg, hnorm]
  unfold settlementLoad
  rw [neutralize_settlementWindow, scaledHalfSupportOccupation_settlementWindow]
  -- Rephrase the window through the local `s`.
  change normSq8
      (fun t => if t = 0 then (s : ℂ) else if t = 1 then -(s : ℂ) else 0) = r
  unfold normSq8
  rw [Fin.sum_univ_eight]
  simp [hnorm, hneg]