feat(Cosmology): barotropic equation of state, density scaling laws, cosmological constant as a fluid

Physlib/Cosmology/FLRW/API-map.yaml

@@ -19,15 +19,17 @@ Overview: |
     scale factor, the Hubble parameter, and the deceleration parameter with the
     relation ∂ₜ H = -H^2 (1 + q). The FLRW type itself is a placeholder; the file
     records a TODO to replace it with a structure bundling a positive scale
-    factor and a spatial geometry. Six further modules, ConformalTime.lean,
-    DensityParameters.lean, Distances.lean, Dynamics.lean, MatterContent.lean and
-    Solutions.lean, contain only TODO items: conformal time and the conformal
-    Hubble factor, the critical density and density parameters, cosmological
-    distances and redshift, energy conditions and the Big-Bang singularity, the
-    matter content with its continuity equation and scaling laws, and the exact
-    de Sitter, radiation-dominated, Einstein-de Sitter, Milne and Einstein static
-    solutions. The requirements below record the two most basic of those open
-    items. Cosmology/Basic.lean is a placeholder module doc with no declarations.
+    factor and a spatial geometry. MatterContent.lean contains the continuity
+    equation of the cosmic fluid and its relation to the two Friedmann equations,
+    the barotropic equation of state with the density scaling laws, and the
+    cosmological constant as a fluid. Solutions.lean contains the exact de
+    Sitter, radiation-dominated, Einstein-de Sitter, Milne and Einstein static
+    solutions. Four further modules, ConformalTime.lean, DensityParameters.lean,
+    Distances.lean and Dynamics.lean, contain only TODO items: conformal time and
+    the conformal Hubble factor, the critical density and density parameters,
+    cosmological distances and redshift, energy conditions and the Big-Bang
+    singularity. Cosmology/Basic.lean is a placeholder module doc with no
+    declarations.
 
 ParentAPIs:
   - Time (Physlib/SpaceAndTime/Time)
@@ -89,10 +91,27 @@ Requirements:
     location: "Physlib/Cosmology/FLRW/Basic.lean (decelerationParameter, deriv_hubbleConstant, decelerationParameter_eq_one_plus_hubbleConstant, deriv_hubbleConstant_eq_neg_sq_mul, deriv_hubbleConstant_neg_iff, exists_deriv_hubbleConstant_neg_iff)"
 
   - description: >
-      The continuity equation ∂ₜ ρ + 3 H (ρ + P/c^2) = 0 of the cosmic fluid, the
-      barotropic equation of state P = w ρ c^2, and the density scaling law
-      ρ ∝ a^(-3(1+w)) with its dust, radiation and vacuum-energy special cases.
-      Recorded as TODO items in Physlib/Cosmology/FLRW/MatterContent.lean; no
-      declarations exist yet.
-    done: false
-    location: "N/A"
+      The continuity equation ∂ₜ ρ + 3 H (ρ + P/c^2) = 0 of the cosmic fluid is
+      defined as a proposition at an instant, and the API relates it to the two
+      Friedmann equations: it follows from the first-order equation holding at all
+      times together with the second-order equation, and conversely the
+      second-order equation follows from the first-order equation and the
+      continuity equation wherever ∂ₜ a ≠ 0.
+    done: true
+    location: "Physlib/Cosmology/FLRW/MatterContent.lean (ContinuityEquation, deriv_firstOrderFriedmann, continuityEquation_of_friedmann, secondOrderFriedmann_of_continuityEquation)"
+
+  - description: >
+      The barotropic equation of state P = w ρ c^2 is defined, and the API
+      contains the density scaling law ρ t = ρ t₀ (a t / a t₀)^(-3(1+w)) under the
+      barotropic continuity equation holding at all times, its converse, and its
+      dust, radiation and vacuum-energy special cases.
+    done: true
+    location: "Physlib/Cosmology/FLRW/MatterContent.lean (barotropicPressure, deriv_of_continuityEquation_barotropic, density_scaling, continuityEquation_of_scaling, density_scaling_dust, density_scaling_radiation, density_scaling_vacuum)"
+
+  - description: >
+      The cosmological constant as a fluid: the density ρ_Λ = Λ c^2 / (8πG) and
+      the pressure p_Λ = -ρ_Λ c^2 are defined, each Friedmann equation with Λ is
+      equivalent to the same equation without Λ for the fluid ρ + ρ_Λ, p + p_Λ,
+      and p_Λ is the w = -1 barotropic pressure of ρ_Λ.
+    done: true
+    location: "Physlib/Cosmology/FLRW/MatterContent.lean (cosmologicalConstantDensity, cosmologicalConstantPressure, firstOrderFriedmann_iff_lambdaFluid, secondOrderFriedmann_iff_lambdaFluid, cosmologicalConstantPressure_eq_barotropic)"

Physlib/Cosmology/FLRW/Basic.lean

@@ -103,7 +103,11 @@ def FLRW : Type := sorry
 
 TODO "Replace the placeholder `FLRW` type with a concrete structure bundling a positive
   scale factor `a : Time → ℝ` (smooth, or at least twice differentiable) together with an
-  element of `SpatialGeometry`."
+  element of `SpatialGeometry`. If the structure also bundles the dynamics, it should carry the
+  first- and second-order Friedmann equations as fields and obtain the continuity equation as a
+  lemma through `FriedmannEquation.continuityEquation_of_friedmann`, never the other way round:
+  where `∂ₜ a = 0` the first-order and continuity equations leave the pressure unconstrained,
+  whereas the second-order equation fixes `ρ + 3 p / c²` (the Einstein static universe)."
 
 namespace FLRW