Green's open problem 24 - conjecture

end Bounty
noncomputable section
/- 
# Green 24: packed single-file candidate — full verification pending
Riley Sturgill — [email protected]
AI assistance: OpenAI ChatGPT/Codex assisted with the mathematics,
certificate generation,Lean formalization,verification,and presentation.
Original source attributions and licenses are retained below.
This candidate inlines the exact Bounty.target and all its project dependencies.
Its numerical data are decoded by ordinary total Lean functions and must pass
the proved checker. No external certificate file is required.
The packed checker has passed representative tests. See the accompanying reports
for current size,policy,and verification results. Submission readiness requires
a successful whole-file Lean check and the pinned validator checks.
The original 300 MB file and its running check are preserved separately.
-/
section 
namespace Green24Proof
noncomputable def rho (x y:ℝ):ℝ :=
  if max x y ≤ 3 * min x y then (x - y) ^ 2 / 4
  else x * y - 2 * (min x y) ^ 2
theorem rho_comm (x y:ℝ):rho x y = rho y x:=by
  unfold rho
  rw [max_comm y x,min_comm y x]
  split_ifs <;> ring
theorem rho_eq_balanced {x y:ℝ} (hyx:y ≤ x) (hxy:x ≤ 3 * y) :
    rho x y = (x - y) ^ 2 / 4:=by
  simp only [rho,max_eq_left hyx,min_eq_right hyx,if_pos hxy]
theorem rho_eq_unbalanced {x y:ℝ} (hyx:y ≤ x) (hxy:3 * y ≤ x) :
    rho x y = x * y - 2 * y ^ 2:=by
  simp only [rho,max_eq_left hyx,min_eq_right hyx]
  split_ifs with h
  · have:x = 3 * y:=le_antisymm h hxy
    rw [this]
    ring
  · rfl
private def zz1:"s0001"="s0001":=by decide+kernel
theorem rho_nonneg {x y:ℝ} (hx:0 ≤ x) (hy:0 ≤ y):0 ≤ rho x y:=by
  unfold rho
  split_ifs with h
  · positivity
  · rcases le_total x y with hxy | hyx
    · rw [max_eq_right hxy,min_eq_left hxy] at h
      rw [min_eq_left hxy]
      have hprod:=mul_nonneg hx (by linarith:0 ≤ y - 2 * x)
      nlinarith
    · rw [max_eq_left hyx,min_eq_right hyx] at h
      rw [min_eq_right hyx]
      have hprod:=mul_nonneg hy (by linarith:0 ≤ x - 2 * y)
      nlinarith
theorem rho_self {x:ℝ} (hx:0 ≤ x):rho x x = 0:=by
  rw [rho_eq_balanced (le_refl x) (by linarith)]
  ring
theorem rho_zero {x:ℝ} (hx:0 ≤ x):rho x 0 = 0:=by
  rw [rho_eq_unbalanced hx (by simpa using hx)]
  ring
theorem rho_zero_left {x:ℝ} (hx:0 ≤ x):rho 0 x = 0:=by
  rw [rho_comm,rho_zero hx]
private def zz2:"s0002"="s0002":=by decide+kernel
theorem rho_positive_part_identity {x y:ℝ} (hx:0 ≤ x) (hy:0 ≤ y) :
    4 * rho x y = (x - y) ^ 2 - max (x - 3 * y) 0 ^ 2 - max (y - 3 * x) 0 ^ 2:=by
  rcases le_total y x with hyx | hxy
  · have hy3x:y - 3 * x ≤ 0:=by linarith
    rw [max_eq_right hy3x]
    by_cases h:x ≤ 3 * y
    · rw [rho_eq_balanced hyx h,max_eq_right (by linarith:x - 3 * y ≤ 0)]
      ring
    · rw [rho_eq_unbalanced hyx (le_of_not_ge h),
        max_eq_left (by linarith:0 ≤ x - 3 * y)]
      ring
  · have hx3y:x - 3 * y ≤ 0:=by linarith
    rw [rho_comm,max_eq_right hx3y]
    by_cases h:y ≤ 3 * x
    · rw [rho_eq_balanced hxy h,max_eq_right (by linarith:y - 3 * x ≤ 0)]
      ring
    · rw [rho_eq_unbalanced hxy (le_of_not_ge h),
        max_eq_left (by linarith:0 ≤ y - 3 * x)]
      ring
noncomputable def energy {ι:Type*} [Fintype ι] (u:ι → ℝ):ℝ :=
  (∑ i, ∑ j,rho (u i) (u j)) / 2
theorem energy_nonneg {ι:Type*} [Fintype ι] {u:ι → ℝ}
    (hu:∀ i,0 ≤ u i):0 ≤ energy u:=by
  unfold energy
  exact div_nonneg (Finset.sum_nonneg fun i _ =>
    Finset.sum_nonneg fun j _ => rho_nonneg (hu i) (hu j)) (by norm_num)
theorem energy_sum_identity {ι:Type*} [Fintype ι] {u:ι → ℝ}
    (hu:∀ i,0 ≤ u i) :
    4 * energy u = (Fintype.card ι:ℝ) * (∑ i,u i ^ 2) - (∑ i,u i) ^ 2 -
      ∑ i, ∑ j,max (u i - 3 * u j) 0 ^ 2:=by
  have hid:=Finset.sum_congr rfl (fun i (_:i ∈ (Finset.univ:Finset ι)) =>
    Finset.sum_congr rfl (fun j (_:j ∈ (Finset.univ:Finset ι)) =>
      rho_positive_part_identity (hu i) (hu j)))
  have hswap:(∑ i, ∑ j,max (u j - 3 * u i) 0 ^ 2) =
      ∑ i, ∑ j,max (u i - 3 * u j) 0 ^ 2:=Finset.sum_comm
  simp_rw [sub_sq] at hid
  simp only [Finset.sum_sub_distrib,Finset.sum_add_distrib,Finset.sum_const,
    Finset.card_univ,nsmul_eq_mul, ← Finset.mul_sum, ← Finset.sum_mul] at hid
  rw [hswap] at hid
  unfold energy
  nlinarith [hid]
end Green24Proof
end 
section 
namespace Green24Proof
noncomputable def mass {ι:Type*} [Fintype ι] (u:ι → ℝ):ℝ:=∑ i,u i
noncomputable def truncatedMass {ι:Type*} [Fintype ι] (u:ι → ℝ) (t:ℝ):ℝ :=
  ∑ i,min (u i) t
noncomputable def overlap {ι:Type*} [Fintype ι] (T:ι → ι) (u:ι → ℝ):ℝ :=
  ∑ i,min (u (T i)) (3 * u i)
theorem min_threshold (x y t:ℝ):min x y ≤ max (x - t) 0 + min t y:=by
  simp only [min_def,max_def]
  split_ifs <;> linarith
private def zz3:"s0003"="s0003":=by decide+kernel
theorem sum_comp_le_card {ι:Type*} [Fintype ι] [DecidableEq ι]
    (T:ι → ι) (N:ℕ) (hT:∀ j,(Finset.univ.filter fun i => T i = j).card ≤ N)
    (f:ι → ℝ) (hf:∀ i,0 ≤ f i) :
    ∑ i,f (T i) ≤ N * ∑ i,f i:=by
  calc
    ∑ i,f (T i) = ∑ i, ∑ j,if T i = j then f j else 0:=by simp
    _ = ∑ j, ∑ i,if T i = j then f j else 0:=Finset.sum_comm
    _ ≤ ∑ j,(N:ℝ) * f j:=by
      apply Finset.sum_le_sum
      intro j _
      rw [← Finset.sum_filter]
      simp only [Finset.sum_const,nsmul_eq_mul]
      apply mul_le_mul_of_nonneg_right _ (hf j)
      exact_mod_cast hT j
    _ = N * ∑ j,f j:=(Finset.mul_sum _ _ _).symm
theorem sum_comp_le_three {ι:Type*} [Fintype ι] [DecidableEq ι]
    (T:ι → ι) (hT:∀ j,(Finset.univ.filter fun i => T i = j).card ≤ 3)
    (f:ι → ℝ) (hf:∀ i,0 ≤ f i) :
    ∑ i,f (T i) ≤ 3 * ∑ i,f i:=by
  simpa only [Nat.cast_ofNat] using sum_comp_le_card T 3 hT f hf
theorem overlap_le_truncation {ι:Type*} [Fintype ι] [DecidableEq ι]
    (T:ι → ι) (hT:∀ j,(Finset.univ.filter fun i => T i = j).card ≤ 3)
    (u:ι → ℝ) (t:ℝ) :
    overlap T u ≤ 3 * mass u - 3 * (truncatedMass u t - truncatedMass u (t / 3)):=by
  have hthreshold:=Finset.sum_le_sum (s:=Finset.univ) (fun i _ =>
    min_threshold (u (T i)) (3 * u i) t)
  have hpreimages:=sum_comp_le_three T hT (fun i => max (u i - t) 0)
    (fun i => le_max_right _ _)
  have hmax (x:ℝ):max (x - t) 0 = x - min x t:=by
    simp only [max_def,min_def]
    split_ifs <;> linarith
  have hmin (x:ℝ):min t (3 * x) = 3 * min x (t / 3):=by
    simp only [min_def]
    split_ifs <;> linarith
  simp_rw [hmax] at hpreimages hthreshold
  simp_rw [hmin] at hthreshold
  simp only [Finset.sum_add_distrib,Finset.sum_sub_distrib, ← Finset.mul_sum] at hpreimages hthreshold
  unfold overlap mass truncatedMass
  linarith
theorem truncation_difference_bounds {ι:Type*} [Fintype ι]
    (u:ι → ℝ) (hu:∀ i,0 ≤ u i) {t:ℝ} (ht:0 ≤ t) :
    0 ≤ truncatedMass u t - truncatedMass u (t / 3) ∧
      truncatedMass u t - truncatedMass u (t / 3) ≤ (2 / 3) * truncatedMass u t:=by
  have h₁:truncatedMass u (t / 3) ≤ truncatedMass u t:=by
    apply Finset.sum_le_sum
    intro i _
    exact min_le_min_left _ (by linarith)
  have h₂:truncatedMass u t ≤ 3 * truncatedMass u (t / 3):=by
    unfold truncatedMass
    rw [Finset.mul_sum]
    apply Finset.sum_le_sum
    intro i _
    have hi:=hu i
    simp only [min_def]
    split_ifs <;> linarith
  constructor <;> linarith
end Green24Proof
end 
section 
namespace Green24Proof
noncomputable def Q12 (A B:ℝ):ℝ :=
  -(97 / 0x64) * A ^ 2 + (61 / 25) * A * B - (79 / 50) * B ^ 2
noncomputable def Q18 (A B:ℝ):ℝ :=
  -(17 / 25) * A ^ 2 + (0x6d / 50) * A * B - (93 / 50) * B ^ 2
private def zz4:"s0004"="s0004":=by decide+kernel
theorem Q12_interval_identity (A B:ℝ) :
    Q12 A B + (9 / 0x100) * (A + B) ^ 2 =
      (0x175f / 0x1900) * (A - B) * ((8 / 5) * B - A) +
      (49 / 0x640) * B ^ 2 + (0x1de5 / 0x27100) * (5 / 3) * B * (A - B):=by
  unfold Q12
  ring
theorem Q12_lower {A B:ℝ} (hB:0 ≤ B) (hAB:B ≤ A)
    (hupper:A ≤ (8 / 5) * B) :
    -(9 / 0x100) * (A + B) ^ 2 ≤ Q12 A B:=by
  have h₁:=mul_nonneg (sub_nonneg.mpr hAB) (sub_nonneg.mpr hupper)
  have h₂:=mul_nonneg hB (sub_nonneg.mpr hAB)
  have hid:=Q12_interval_identity A B
  nlinarith [sq_nonneg B]
theorem Q18_interval_identity (A B:ℝ) :
    Q18 A B + (9 / 0x100) * (A + B) ^ 2 =
      (0x101f / 0x1900) * (A - (8 / 5) * B) * ((0x83 / 61) * B - A) +
      (0x4e09 / 0x27100) * B * (((0x83 / 61) * B - A) / (0x83 / 61 - 8 / 5)) +
      (0xc4a / 0x16b61) * B * ((A - (8 / 5) * B) / (0x83 / 61 - 8 / 5)):=by
  unfold Q18
  ring
theorem Q18_lower {A B:ℝ} (hB:0 ≤ B)
    (hlower:(8 / 5) * B ≤ A) (hupper:A ≤ (0x83 / 61) * B) :
    -(9 / 0x100) * (A + B) ^ 2 ≤ Q18 A B:=by
  have h₁:=mul_nonneg (sub_nonneg.mpr hlower) (sub_nonneg.mpr hupper)
  have h₂:=mul_nonneg hB (sub_nonneg.mpr hupper)
  have h₃:=mul_nonneg hB (sub_nonneg.mpr hlower)
  have hid:=Q18_interval_identity A B
  norm_num at hid
  nlinarith
private def zz5:"s0005"="s0005":=by decide+kernel
theorem height_cover {A B H d:ℝ} (hB:0 ≤ B) (hAB:B ≤ A)
    (hupper:A ≤ (0x83 / 61) * B)
    (h12:(2 / 5) * H + Q12 A B ≤ d)
    (h18:(2 / 5) * H + Q18 A B ≤ d) :
    (2 / 5) * H - (9 / 0x100) * (A + B) ^ 2 ≤ d:=by
  by_cases hcut:A ≤ (8 / 5) * B
  · linarith [Q12_lower hB hAB hcut]
  · linarith [Q18_lower hB (le_of_not_ge hcut) hupper]
theorem overlap_of_energy_estimate {U A H R:ℝ}
    (hH:(2 * U - 3 * A) ^ 2 ≤ 8 * H)
    (hR:R ≤ 3 * U - 3 * A) :
    R ≤ U + Real.sqrt (8 * H):=by
  have hnonneg:0 ≤ 8 * H:=(sq_nonneg _).trans hH
  have hsqrt:=Real.sq_sqrt hnonneg
  have hsqrt_nonneg:=Real.sqrt_nonneg (8 * H)
  have hle:2 * U - 3 * A ≤ Real.sqrt (8 * H):=by
    nlinarith
  linarith
theorem weighted_overlap {U H R C:ℝ} (hU:0 ≤ U) (hH:0 ≤ H)
    (hC:0 < C) (hR:R ≤ U + Real.sqrt (8 * H)) :
    U * R ≤ (1 + 2 / C) * U ^ 2 + C * H:=by
  have hsqrt:=Real.sq_sqrt (mul_nonneg (by norm_num:(0:ℝ) ≤ 8) hH)
  have hmul:=mul_le_mul_of_nonneg_left hR hU
  have hsq:=sq_nonneg (C * Real.sqrt (8 * H) - 4 * U)
  have hyoung:C * U * Real.sqrt (8 * H) ≤ 2 * U ^ 2 + C ^ 2 * H:=by
    nlinarith [hsqrt]
  apply (mul_le_mul_iff_right₀ hC).mp
  have hmulC:=mul_le_mul_of_nonneg_right hmul hC.le
  have hdiv:(2 / C:ℝ) * C = 2:=div_mul_cancel₀ 2 (ne_of_gt hC)
  nlinarith [hdiv]
theorem overlap_bound_of_height {U H R d:ℝ} (hU:0 ≤ U) (hH:0 ≤ H)
    (hoverlap:R ≤ U + Real.sqrt (8 * H))
    (hheight:(2 / 5) * H - (9 / 0x100) * U ^ 2 ≤ d) :
    U * R ≤ (61 / 32) * U ^ 2 + 8 * d:=by
  have h:=weighted_overlap hU hH (by norm_num:(0:ℝ) < 16 / 5) hoverlap
  norm_num at h
  linarith
private def zz6:"s0006"="s0006":=by decide+kernel
theorem overlap_bound_of_mass_imbalance {A B R d:ℝ}
    (hA:0 ≤ A) (hB:0 ≤ B) (hratio:(0x83 / 61) * B ≤ A)
    (hR:R ≤ 6 * B) (hd:0 ≤ d) :
    (A + B) * R ≤ (61 / 32) * (A + B) ^ 2 + 8 * d:=by
  have hlinear:R ≤ (61 / 32) * (A + B):=by linarith
  have hmul:=mul_le_mul_of_nonneg_left hlinear (add_nonneg hA hB)
  nlinarith
theorem overlap_bound {A B H R d:ℝ} (hB:0 ≤ B) (hAB:B ≤ A)
    (hH:0 ≤ H) (hd:0 ≤ d)
    (hoverlap:R ≤ A + B + Real.sqrt (8 * H)) (hparity:R ≤ 6 * B)
    (h12:(2 / 5) * H + Q12 A B ≤ d)
    (h18:(2 / 5) * H + Q18 A B ≤ d) :
    (A + B) * R ≤ (61 / 32) * (A + B) ^ 2 + 8 * d:=by
  by_cases hratio:A ≤ (0x83 / 61) * B
  · exact overlap_bound_of_height (by linarith) hH hoverlap
      (height_cover hB hAB hratio h12 h18)
  · exact overlap_bound_of_mass_imbalance (hB.trans hAB) hB
      (le_of_not_ge hratio) hparity hd
theorem boundary_descent {U V R du dv dg:ℝ} (hU:0 < U) (hV:0 ≤ V)
    (hoverlap:U * R ≤ (61 / 32) * U ^ 2 + 8 * du)
    (hexpansion:du + dv + 4 * U * V - 3 * V ^ 2 - 2 * V * R ≤ dg) :
    (1 - 16 * V / U) * du + dv + V * ((3 / 16) * U - 3 * V) ≤ dg:=by
  have hscaled:=mul_le_mul_of_nonneg_left hoverlap (by positivity:0 ≤ 2 * V)
  apply (mul_le_mul_iff_right₀ hU).mp
  have hexpansionU:=mul_le_mul_of_nonneg_right hexpansion hU.le
  have hcancel:(16 * V / U) * U = 16 * V:=div_mul_cancel₀ _ (ne_of_gt hU)
  nlinarith [congrArg (fun x:ℝ => x * du) hcancel]
theorem boundary_nonneg {U V R du dv dg:ℝ} (hU:0 < U) (hV:0 ≤ V)
    (hratio:16 * V ≤ U) (hdu:0 ≤ du) (hdv:0 ≤ dv)
    (hoverlap:U * R ≤ (61 / 32) * U ^ 2 + 8 * du)
    (hexpansion:du + dv + 4 * U * V - 3 * V ^ 2 - 2 * V * R ≤ dg) :
    0 ≤ dg:=by
  have hdesc:=boundary_descent hU hV hoverlap hexpansion
  have hcoef:0 ≤ 1 - 16 * V / U:=by
    have hdiv:16 * V / U ≤ 1:=(div_le_one hU).mpr hratio
    linarith
  have h₁:=mul_nonneg hcoef hdu
  have h₂:0 ≤ V * ((3 / 16) * U - 3 * V) :=
    mul_nonneg hV (by linarith)
  linarith
end Green24Proof
end 
section 
open Set Filter MeasureTheory
open scoped Topology
namespace Green24Proof
noncomputable def tailCount {ι:Type*} [Fintype ι] (u:ι → ℝ) (t:ℝ):ℝ :=
  ∑ i,if t < u i then 1 else 0
private def zz7:"s0007"="s0007":=by decide+kernel
theorem tailCount_nonneg {ι:Type*} [Fintype ι] (u:ι → ℝ) (t:ℝ) :
    0 ≤ tailCount u t:=by
  unfold tailCount
  exact Finset.sum_nonneg (fun _ _ => by split_ifs <;> norm_num)
theorem tailCount_antitone {ι:Type*} [Fintype ι] (u:ι → ℝ) :
    Antitone (tailCount u):=by
  intro s t hst
  unfold tailCount
  apply Finset.sum_le_sum
  intro i _
  split_ifs <;> norm_num at *; linarith
theorem truncatedMass_continuous {ι:Type*} [Fintype ι] (u:ι → ℝ) :
    Continuous (truncatedMass u):=by
  unfold truncatedMass
  fun_prop
theorem hasDerivWithinAt_min_right (a t:ℝ) :
    HasDerivWithinAt (fun s:ℝ => min a s) (if t < a then 1 else 0) (Ioi t) t:=by
  by_cases h:t < a
  · simp only [if_pos h]
    apply (hasDerivAt_id t).hasDerivWithinAt.congr_of_eventuallyEq
    · filter_upwards [nhdsWithin_le_nhds (Iio_mem_nhds h)] with s hs
      exact min_eq_right (le_of_lt hs)
    · exact min_eq_right h.le
  · simp only [if_neg h]
    apply (hasDerivWithinAt_const t (Ioi t) a).congr
    · intro s hs
      exact min_eq_left ((le_of_not_gt h).trans hs.le)
    · exact min_eq_left (le_of_not_gt h)
private def zz8:"s0008"="s0008":=by decide+kernel
theorem truncatedMass_hasDeriv_right {ι:Type*} [Fintype ι] (u:ι → ℝ) (t:ℝ) :
    HasDerivWithinAt (truncatedMass u) (tailCount u t) (Ioi t) t:=by
  unfold truncatedMass tailCount
  exact HasDerivWithinAt.fun_sum fun i _ => hasDerivWithinAt_min_right (u i) t
theorem integral_tailCount {ι:Type*} [Fintype ι] (u:ι → ℝ) {a b:ℝ}
    (hab:a ≤ b) :
    (∫ t in a..b,tailCount u t) = truncatedMass u b - truncatedMass u a:=by
  exact intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le hab
    (truncatedMass_continuous u).continuousOn
    (fun t _ => truncatedMass_hasDeriv_right u t) (tailCount_antitone u).intervalIntegrable
theorem integral_tailCount_mul_mass {ι:Type*} [Fintype ι] (u:ι → ℝ) {a b:ℝ}
    (hab:a ≤ b) :
    (∫ t in a..b,tailCount u t * truncatedMass u t) =
      (truncatedMass u b ^ 2 - truncatedMass u a ^ 2) / 2:=by
  have hderiv (t:ℝ):HasDerivWithinAt (fun s => truncatedMass u s ^ 2 / 2)
      (tailCount u t * truncatedMass u t) (Ioi t) t:=by
    convert ((truncatedMass_hasDeriv_right u t).pow 2).div_const 2 using 1
    all_goals first | rfl | ring
  have h:=intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le hab
    (f:=fun s => truncatedMass u s ^ 2 / 2)
    (((truncatedMass_continuous u).pow 2).div_const 2).continuousOn (fun t _ => hderiv t)
    ((tailCount_antitone u).intervalIntegrable.mul_continuousOn
      (truncatedMass_continuous u).continuousOn)
  convert h using 1
  ring
theorem posSquare_hasDeriv_right (c t:ℝ) :
    HasDerivWithinAt (fun s:ℝ => max (s - c) 0 ^ 2)
      (2 * max (t - c) 0) (Ioi t) t:=by
  by_cases h:t < c
  · rw [max_eq_right (by linarith:t - c ≤ 0),mul_zero]
    apply (hasDerivWithinAt_const t (Ioi t) (0:ℝ)).congr_of_eventuallyEq
    · filter_upwards [nhdsWithin_le_nhds (Iio_mem_nhds h)] with s hs
      rw [max_eq_right (by linarith [show s < c from hs]:s - c ≤ 0)]
      norm_num
    · rw [max_eq_right (by linarith:t - c ≤ 0)]
      norm_num
  · rw [max_eq_left (by linarith:0 ≤ t - c)]
    have hpoly:=(((hasDerivAt_id t).sub_const c).pow 2).hasDerivWithinAt (s:=Ioi t)
    simp only [Nat.reduceSub,pow_one,mul_one,id_eq] at hpoly
    apply hpoly.congr
    · intro s hs
      rw [max_eq_left (by linarith [show t < s from hs]:0 ≤ s - c)]
      rfl
    · rw [max_eq_left (by linarith:0 ≤ t - c)]
      rfl
private def zz9:"s0009"="s0009":=by decide+kernel
theorem integral_min_linear {x c:ℝ} (hx:0 ≤ x) (hc:0 ≤ c) :
    (∫ t in (0:ℝ)..x,min t c) = (x ^ 2 - max (x - c) 0 ^ 2) / 2:=by
  have hderiv (t:ℝ):HasDerivWithinAt
      (fun s:ℝ => (s ^ 2 - max (s - c) 0 ^ 2) / 2) (min t c) (Ioi t) t:=by
    have h:=(((hasDerivAt_id t).pow 2).hasDerivWithinAt.sub
      (posSquare_hasDeriv_right c t)).div_const 2
    convert h using 1
    all_goals first | rfl | (simp only [id_eq,Nat.reduceSub,pow_one,mul_one,min_def,max_def]; split_ifs <;> linarith)
  have h:=intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le hx
    (f:=fun s:ℝ => (s ^ 2 - max (s - c) 0 ^ 2) / 2)
    (by fun_prop) (fun t _ => hderiv t)
    ((continuous_id.min continuous_const).intervalIntegrable 0 x)
  simpa [max_eq_right (neg_nonpos.mpr hc)] using h
theorem indicator_lt_antitone (x:ℝ) :
    Antitone (fun t:ℝ => if t < x then (1:ℝ) else 0):=by
  intro s t hst
  dsimp only
  split_ifs <;> norm_num at *; linarith
theorem integral_indicator_lt_mul {x M:ℝ} (hx:0 ≤ x) (hxM:x ≤ M)
    (f:ℝ → ℝ) :
    (∫ t in (0:ℝ)..M,(if t < x then 1 else 0) * f t) = ∫ t in (0:ℝ)..x,f t:=by
  rw [← intervalIntegral.integral_indicator (f:=f) ⟨hx,hxM⟩]
  apply intervalIntegral.integral_congr_ae
  filter_upwards [volume.ae_ne x] with t ht _
  simp only [Set.indicator_apply,mem_ofPred_eq]
  by_cases h:t < x
  · simp [h,h.le]
  · have hnot:¬t ≤ x:=fun hle => h (lt_of_le_of_ne hle ht)
    simp [h,hnot]
theorem mass_nonneg {ι:Type*} [Fintype ι] {u:ι → ℝ} (hu:∀ i,0 ≤ u i) :
    0 ≤ mass u:=Finset.sum_nonneg (fun i _ => hu i)
private def zz10:"s000a"="s000a":=by decide+kernel
theorem height_le_mass {ι:Type*} [Fintype ι] {u:ι → ℝ} (hu:∀ i,0 ≤ u i) (i:ι) :
    u i ≤ mass u:=Finset.single_le_sum (fun j _ => hu j) (Finset.mem_univ i)
theorem truncatedMass_zero {ι:Type*} [Fintype ι] {u:ι → ℝ} (hu:∀ i,0 ≤ u i) :
    truncatedMass u 0 = 0:=by
  simp [truncatedMass,min_eq_right (hu _)]
theorem truncatedMass_mass {ι:Type*} [Fintype ι] {u:ι → ℝ} (hu:∀ i,0 ≤ u i) :
    truncatedMass u (mass u) = mass u:=by
  unfold truncatedMass mass
  apply Finset.sum_congr rfl
  intro i _
  exact min_eq_left (height_le_mass hu i)
theorem truncatedMass_le_mass {ι:Type*} [Fintype ι] (u:ι → ℝ) (t:ℝ) :
    truncatedMass u t ≤ mass u:=Finset.sum_le_sum (fun i _ => min_le_left (u i) t)
private def zz11:"s000b"="s000b":=by decide+kernel
theorem integral_tail_mul {ι:Type*} [Fintype ι] {u:ι → ℝ}
    (hu:∀ i,0 ≤ u i) (f:ℝ → ℝ) (hf:Continuous f) :
    (∫ t in (0:ℝ)..mass u,tailCount u t * f t) =
      ∑ i, ∫ t in (0:ℝ)..u i,f t:=by
  simp only [tailCount,Finset.sum_mul]
  rw [intervalIntegral.integral_finsetSum]
  · apply Finset.sum_congr rfl
    intro i _
    exact integral_indicator_lt_mul (hu i) (height_le_mass hu i) f
  · intro i _
    exact (indicator_lt_antitone (u i)).intervalIntegrable.mul_continuousOn hf.continuousOn
theorem integral_min_third {x y:ℝ} (hx:0 ≤ x) (hy:0 ≤ y) :
    (∫ t in (0:ℝ)..x,min y (t / 3)) = (x ^ 2 - max (x - 3 * y) 0 ^ 2) / 6:=by
  have hmin (t:ℝ):min y (t / 3) = min t (3 * y) / 3:=by
    simp only [min_def]
    split_ifs <;> linarith
  simp_rw [hmin]
  rw [intervalIntegral.integral_div,integral_min_linear hx (by linarith:0 ≤ 3 * y)]
  ring
theorem integral_tail_mul_third {ι:Type*} [Fintype ι] {u:ι → ℝ}
    (hu:∀ i,0 ≤ u i) :
    (∫ t in (0:ℝ)..mass u,tailCount u t * truncatedMass u (t / 3)) =
      (4 * energy u + mass u ^ 2) / 6:=by
  rw [integral_tail_mul hu (fun t => truncatedMass u (t / 3))
    ((truncatedMass_continuous u).comp (continuous_id.div_const 3))]
  have hscalar (i:ι):(∫ t in (0:ℝ)..u i,truncatedMass u (t / 3)) =
      ∑ j,(u i ^ 2 - max (u i - 3 * u j) 0 ^ 2) / 6:=by
    unfold truncatedMass
    rw [intervalIntegral.integral_finsetSum]
    · exact Finset.sum_congr rfl (fun j _ => integral_min_third (hu i) (hu j))
    · intro j _
      exact (continuous_const.min (continuous_id.div_const 3)).intervalIntegrable 0 (u i)
  simp_rw [hscalar]
  simp only [← Finset.sum_div,Finset.sum_sub_distrib,Finset.sum_const,Finset.card_univ,
    nsmul_eq_mul, ← Finset.mul_sum]
  have he:=energy_sum_identity hu
  unfold mass
  linarith
theorem energy_integral_identity {ι:Type*} [Fintype ι] {u:ι → ℝ}
    (hu:∀ i,0 ≤ u i) :
    energy u = mass u ^ 2 / 2 - (3 / 2) *
      (∫ t in (0:ℝ)..mass u,
        tailCount u t * (truncatedMass u t - truncatedMass u (t / 3))):=by
  simp_rw [mul_sub]
  rw [intervalIntegral.integral_sub]
  · rw [integral_tailCount_mul_mass u (mass_nonneg hu),truncatedMass_mass hu,
      truncatedMass_zero hu,integral_tail_mul_third hu]
    ring
  · exact (tailCount_antitone u).intervalIntegrable.mul_continuousOn
      (truncatedMass_continuous u).continuousOn
  · exact (tailCount_antitone u).intervalIntegrable.mul_continuousOn
      ((truncatedMass_continuous u).comp (continuous_id.div_const 3)).continuousOn
private def zz12:"s000c"="s000c":=by decide+kernel
theorem energyIntegrand_intervalIntegrable {ι:Type*} [Fintype ι]
    (u:ι → ℝ) (a b:ℝ) :
    IntervalIntegrable
      (fun t => tailCount u t * (truncatedMass u t - truncatedMass u (t / 3)))
      volume a b :=
  (tailCount_antitone u).intervalIntegrable.mul_continuousOn
    ((truncatedMass_continuous u).sub
      ((truncatedMass_continuous u).comp (continuous_id.div_const 3))).continuousOn
theorem energy_integral_upper {ι:Type*} [Fintype ι] {u:ι → ℝ}
    (hu:∀ i,0 ≤ u i) {A:ℝ} (hA:0 ≤ A) (hAU:A ≤ (2 / 3) * mass u)
    (hbound:∀ t ∈ Icc (0:ℝ) (mass u),
      truncatedMass u t - truncatedMass u (t / 3) ≤ A) :
    (∫ t in (0:ℝ)..mass u,
      tailCount u t * (truncatedMass u t - truncatedMass u (t / 3))) ≤
      A * mass u - (3 / 4) * A ^ 2:=by
  have hU:=mass_nonneg hu
  have hvalue:(3 / 2) * A ∈ Icc (truncatedMass u 0) (truncatedMass u (mass u)):=by
    rw [truncatedMass_zero hu,truncatedMass_mass hu]
    constructor <;> linarith
  obtain ⟨s,hs,hLs⟩ :=
    (intermediate_value_Icc hU (truncatedMass_continuous u).continuousOn) hvalue
  have hleft:(∫ t in (0:ℝ)..s,
      tailCount u t * (truncatedMass u t - truncatedMass u (t / 3))) ≤
      (2 / 3) * ((truncatedMass u s ^ 2 - truncatedMass u 0 ^ 2) / 2):=by
    have hmono:=intervalIntegral.integral_mono_on hs.1
      (energyIntegrand_intervalIntegrable u 0 s)
      (((tailCount_antitone u).intervalIntegrable.mul_continuousOn
        (truncatedMass_continuous u).continuousOn).const_mul (2 / 3))
      (fun t (ht:t ∈ Icc (0:ℝ) s) => ?_)
    · simpa only [intervalIntegral.integral_const_mul,integral_tailCount_mul_mass u hs.1]
        using hmono