Cosmology Grand Potential Potential Gibbs Duhem

/-- **Gibbs–Duhem relation (derived).** Along any temperature trajectory
`T(t)`, the pressure obeys `p′ = s(T)·T′`: this is the chain rule applied to
`s = dP/dT`, not an independent postulate. -/
theorem potential_gibbs_duhem
    {P s T : ℝ → ℝ} {T' t : ℝ}
    (hP : HasDerivAt P (s (T t)) (T t))
    (hT : HasDerivAt T T' t) :
    HasDerivAt (fun u => P (T u)) (s (T t) * T') t := by
  simpa [Function.comp] using hP.comp t hT

/-- **Euler relation (derived).** `T·s = ρ + P` is an algebraic identity of
the Legendre-transform structure — not an independent equilibrium postulate. -/
theorem potential_euler (P s : ℝ → ℝ) (x : ℝ) :
    x * s x = energyOf P s x + P x := by
  simp only [energyOf]
  ring

/-- **Fundamental relation `dρ = T·ds` (derived).** The energy density of a
potential fluid has temperature derivative `ρ′(T) = T·s′(T)`:
differentiating `ρ = T·s − P` gives `s + T·s′ − s`. -/
theorem energy_deriv
    {P s : ℝ → ℝ} {sT x : ℝ}
    (hP : HasDerivAt P (s x) x)
    (hs : HasDerivAt s sT x) :
    HasDerivAt (energyOf P s) (x * sT) x := by
  have hid : HasDerivAt (fun y : ℝ => y) 1 x := hasDerivAt_id x
  have hxs : HasDerivAt (fun y => y * s y) (1 * s x + x * sT) x := hid.mul hs
  have h : HasDerivAt (fun y => y * s y - P y)
      (1 * s x + x * sT - s x) x := hxs.sub hP
  have hval : 1 * s x + x * sT - s x = x * sT := by ring
  rw [hval] at h
  exact h

/-- **THEOREM (entropy conservation from the potential alone).** For a fluid
whose pressure is a differentiable potential with `s = dP/dT` — the definition
of local equilibrium at zero chemical potential — the FRW continuity equation
forces `d/dt (s·a³) = 0`.  The Euler and Gibbs–Duhem hypotheses of
`EntropyConservationFRW.comoving_entropy_conserved` are *derived* here
(`potential_euler`, `potential_gibbs_duhem`), not assumed. -/
theorem potential_entropy_conserved
    {P s : ℝ → ℝ} {T a : ℝ → ℝ} {sT T' a' t : ℝ}
    (hTt : T t ≠ 0)
    (hP : HasDerivAt P (s (T t)) (T t))
    (hs : HasDerivAt s sT (T t))
    (hT : HasDerivAt T T' t) (ha : HasDerivAt a a' t)
    (hcont : a t * (T t * sT * T')
        = -3 * a' * (energyOf P s (T t) + P (T t))) :
    HasDerivAt (fun u => s (T u) * a u ^ 3) 0 t :=
  EntropyConservationFRW.comoving_entropy_conserved hTt
    (potential_energy_deriv hP hs hT)
    (potential_gibbs_duhem hP hT)
    (potential_entropy_deriv hs hT)
    ha hT
    (fun u => potential_euler P s (T u))
    rfl
    hcont

/-- **CAPSTONE (dilution from the potential).** `(T_ν/T_γ)³ = 4/11` from:
the coupled sector has a pressure potential with `s = dP/dT` (local
equilibrium, the *only* thermodynamic input), both sectors satisfy their FRW
continuity equations, and the boundary data (plasma dof `2+4 → 2` across e±
annihilation, shared temperature at decoupling).  Compared with
`EntropyConservationFRW.dilution_from_frw`, the Euler and Gibbs–Duhem
hypotheses are gone — they are theorems of the potential structure. -/
theorem dilution_from_potential
    {P s : ℝ → ℝ} {T a Tν : ℝ → ℝ} {sT T' a' Tν' ρν' : ℝ → ℝ}
    {t₁ t₂ : ℝ} {T₁ Tγ αν : ℝ}
    (hTt : ∀ t, T t ≠ 0) (hαν : αν ≠ 0) (hTνt : ∀ t, Tν t ≠ 0)
    (ha₂ : a t₂ ≠ 0) (hTγ : Tγ ≠ 0)
    (hP : ∀ t, HasDerivAt P (s (T t)) (T t))
    (hs : ∀ t, HasDerivAt s (sT t) (T t))
    (hT : ∀ t, HasDerivAt T (T' t) t) (ha : ∀ t, HasDerivAt a (a' t) t)
    (hTν : ∀ t, HasDerivAt Tν (Tν' t) t)
    (hρν : ∀ t, HasDerivAt (fun u => αν * Tν u ^ 4) (ρν' t) t)
    (hcont : ∀ t, a t * (T t * sT t * T' t)
        = -3 * a' t * (energyOf P s (T t) + P (T t)))
    (hcontν : ∀ t, a t * ρν' t
        = -3 * a' t * (αν * Tν t ^ 4 + αν * Tν t ^ 4 / 3))
    (hbefore : s (T t₁) = NeutrinoDilution.radiationEntropy 2 4 T₁)
    (hafter : s (T t₂) = NeutrinoDilution.radiationEntropy 2 0 Tγ)
    (hshare : Tν t₁ = T₁) :
    (Tν t₂ / Tγ) ^ 3 = 4 / 11 := by
  -- Adiabaticity of the coupled sector: derived from the potential structure.
  have hcons : NeutrinoDilution.radiationEntropy 2 4 T₁ * a t₁ ^ 3
      = NeutrinoDilution.radiationEntropy 2 0 Tγ * a t₂ ^ 3 := by
    have h := potential_entropy_constant hTt hP hs hT ha hcont t₁ t₂
    rw [hbefore, hafter] at h
    exact h
  -- Free streaming of the neutrino sector (derived in EntropyConservationFRW).
  have hfree : a t₂ * Tν t₂ = a t₁ * T₁ := by
    have h := EntropyConservationFRW.radiation_aT_constant hαν hTνt hTν ha
      hρν hcontν t₂ t₁
    rw [hshare] at h
    exact h
  exact NeutrinoDilution.dilution_from_entropy_conservation ha₂ hTγ hcons hfree