Masses Mass Genesis T10 Double Entry Posting Wall

/-- **A window is a balanced posting exactly when it is neutral.** This is the
reason neutralization is the right operation: it is the projection onto the
windows that balanced postings can produce, and the discarded DC component is
precisely the part that no collection of balanced postings can make.

The reverse direction is where the content sits: neutrality is not merely implied
by double entry, it is *sufficient* for it, so nothing neutral is out of reach of
balanced posting and the projection discards exactly the unreachable part. -/
theorem isBalancedPosting_iff_neutral (w : PhotonWindow) :
    IsBalancedPosting w ↔ (∑ t : Fin 8, w t) = 0 := by
  constructor
  · rintro ⟨q, rfl⟩
    exact sum_coboundary q
  · intro hsum
    have hexp : w 0 + w 1 + w 2 + w 3 + w 4 + w 5 + w 6 + w 7 = 0 := by
      rw [← hsum]; simp [Fin.sum_univ_eight]
    refine ⟨accumulate w, ?_⟩
    funext i
    fin_cases i
    · simp [coboundary, accumulate]
    · simp [coboundary, accumulate]
    · simp [coboundary, accumulate]
    · simp [coboundary, accumulate]
    · simp [coboundary, accumulate]
    · simp [coboundary, accumulate]
    · simp [coboundary, accumulate]
    · -- the wrap-around tick: this is the only case that consumes neutrality
      have e1 : accumulate w 7 = -(w 0 + w 1 + w 2 + w 3 + w 4 + w 5 + w 6) := by
        norm_num [accumulate]
      have hw : (7 : Fin 8) + 1 = 0 := by decide
      have e2 : accumulate w 0 = 0 := by norm_num [accumulate]
      show w 7 = coboundary (accumulate w) 7
      simp only [coboundary, hw, e1, e2, sub_zero]
      linear_combination hexp

/-- **Integer postings summing to zero have an even total square.** Modulo two a
square is its own root, so the total square is congruent to the total, which the
balance condition sets to zero. -/
theorem even_postingLoadInt (p : Fin 8 → ℤ) : Even (postingLoadInt p) := by
  have hzero : (∑ t : Fin 8, (p t - p (t + 1))) = 0 := by
    rw [Finset.sum_sub_distrib]
    have h : (∑ t : Fin 8, p (t + 1)) = ∑ t : Fin 8, p t :=
      Fintype.sum_equiv (Equiv.addRight (1 : Fin 8)) _ _ (fun _ => rfl)
    rw [h]; ring
  have key : ((postingLoadInt p : ℤ) : ZMod 2) = 0 := by
    have hsq : ∀ x : ZMod 2, x ^ 2 = x := by decide
    have hz : ((∑ t : Fin 8, (p t - p (t + 1)) : ℤ) : ZMod 2) = 0 := by
      rw [hzero]; simp
    unfold postingLoadInt
    push_cast at hz ⊢
    rw [Finset.sum_congr rfl (fun t (_ : t ∈ Finset.univ) =>
      hsq ((p t : ZMod 2) - (p (t + 1) : ZMod 2)))]
    exact hz
  obtain ⟨k, hk⟩ := (ZMod.intCast_zmod_eq_zero_iff_dvd (postingLoadInt p) 2).mp key
  exact ⟨k, by rw [hk]; ring⟩

/-- **The floor, sharpened from `7/8` to `2`, with no Boolean hypothesis.** A
positive even integer is at least two. -/
theorem postingLoadInt_ge_two_of_pos {p : Fin 8 → ℤ} (h : 0 < postingLoadInt p) :
    2 ≤ postingLoadInt p := by
  obtain ⟨k, hk⟩ := even_postingLoadInt p
  omega

/-- **The assumed Boolean window condition, derived.** Under double entry the
window entry at a tick *is* the change in occupancy across it, so a unit posting
rate gives entries in `{0, 1, -1}`. -/
theorem booleanWindow_of_onePostingPerTick {w : PhotonWindow} {p : Fin 8 → ℤ}
    (hp : ∀ t, w t = ((p t - p (t + 1) : ℤ) : ℂ)) (hrate : OnePostingPerTick p) :
    BooleanDifferenceSettlementWindow w := by
  intro t
  have h1 : (p t - p (t + 1)).natAbs ≤ 1 := hrate t
  have : p t - p (t + 1) = 0 ∨ p t - p (t + 1) = 1 ∨ p t - p (t + 1) = -1 := by
    omega
  rw [hp t]
  rcases this with h | h | h
  · exact Or.inl (by rw [h]; simp)
  · exact Or.inr (Or.inl (by rw [h]; simp))
  · exact Or.inr (Or.inr (by rw [h]; simp))

/-- **The double-entry mass ratio wall.** Deriving the posting alphabet instead of
assuming it tightens the ceiling from `512/7 ≈ 73.14` to exactly `32`. -/
theorem doubleEntry_restMass_ratio_le {ψ χ : LightPattern (Fin 8)}
    (hsψ : StableClosedLightPattern ψ) (hsχ : StableClosedLightPattern χ)
    (hdψ : DoubleEntrySettledPattern ψ) (hdχ : DoubleEntrySettledPattern χ) :
    restMass ψ ≤ 32 * restMass χ := by
  rw [restMass_eq_integratedMeaningLoad_of_stable ψ hsψ,
      restMass_eq_integratedMeaningLoad_of_stable χ hsχ]
  have hup : integratedMeaningLoad ψ ≤ 64 := doubleEntry_integratedLoad_le_sixtyFour hdψ
  have hlo : 2 ≤ integratedMeaningLoad χ := doubleEntry_integratedLoad_ge_two hdχ hsχ.2.1
  nlinarith [hup, hlo]

/-- **The instantiated refutation, tighter than the phased-posting one.** No two
double-entry settled stable patterns on `Fin 8` can stand in the measured
muon-to-electron mass ratio, which exceeds 32 by a factor of 6.46. -/
theorem doubleEntry_excludes_measured_muonElectron {ψ χ : LightPattern (Fin 8)}
    (hsψ : StableClosedLightPattern ψ) (hsχ : StableClosedLightPattern χ)
    (hdψ : DoubleEntrySettledPattern ψ) (hdχ : DoubleEntrySettledPattern χ) :
    restMass ψ ≠ measuredMuonElectronMassRatio * restMass χ := by
  intro hEq
  have hle := doubleEntry_restMass_ratio_le hsψ hsχ hdψ hdχ
  have hpos : 0 < restMass χ := by
    rw [restMass_eq_integratedMeaningLoad_of_stable χ hsχ]
    have := doubleEntry_integratedLoad_ge_two hdχ hsχ.2.1
    linarith
  rw [hEq] at hle
  have hr : (32 : ℝ) < measuredMuonElectronMassRatio := by
    unfold measuredMuonElectronMassRatio; norm_num
  nlinarith [hle, hpos, hr]