Constraint Resonance State Evolution
Constraint Resonance State Evolution
CRSE · Public Package 001
This package formalizes a restricted, unforced, constant-density, incompressible, viscous Navier–Stokes source in operator form and certifies its correspondence with CRSE's pre-existing generic constant-inertia evolution interface.
Native Structure
The source model uses constant density ρ > 0, dynamic viscosity μ ≥ 0, incompressibility, a recorded Eulerian time derivative, and the native aggregate momentum balance. Spatial gradient, divergence, advection and viscous actions are represented at an operator/classical-solution interface rather than constructed here from a full PDE function-space development.
Certified Crossing
The adapter sends ρ → inertia, u → velocity, and F_NS → the aggregate force channel. Resistance, memory and constraint channels remain zero. The correspondence therefore does not identify viscosity with CRSE resistance or advection with CRSE memory.
Representation Loss
For a spatially constant, possibly time-dependent shift C(t), the package proves that the pressure gradient, aggregate effective force and assembled mechanical representation are unchanged. It also gives an explicit noninjectivity witness and proves that absolute pressure cannot be recovered from the pressure-gradient readout without fixing a gauge.
Conditional Classical Layer
Under separately named classical hypotheses for differentiability, advection cancellation, pressure cancellation, viscous integration by parts and the velocity-paired momentum identity, the package derives the differential and integrated kinetic-energy laws.
These analytic receipts are explicit assumptions of the energy layer; they are not hidden inside a monolithic “energy decreases” premise.
Formal Surface
Load-Bearing Conditions
Full Artifact
Source: RequestProject/NavierStokesReduction.lean
Namespace: ResonantEvolution.NavierStokesReduction
import Mathlib
import RequestProject.ReductionAdapter
/-!
# Navier–Stokes reduction: operator-form classical-solution correspondence
This module formalizes a *restricted* source model — unforced, constant-density,
incompressible, viscous Navier–Stokes in operator form —
```
∂ₜu + (u·∇)u = -(1/ρ)∇p + ν∆u, ∇·u = 0,
```
equivalently, with constant density `ρ > 0` and dynamic viscosity `µ ≥ 0`,
```
ρ ∂ₜu = -ρ(u·∇)u - ∇p + µ∆u =: F_NS,
```
and certifies its correspondence with the *existing* generic constant-inertia evolution
interface of this repository (`MechanicalData`, `SatisfiesGeneralEvolution`,
`Adapter`, `PreservesEvolution`). No new notion of general evolution is introduced.
## Contents
* **Block A (momentum correspondence).** The native aggregate force `nsEffectiveForce`, the
native momentum balance, the constant-density identity `d(ρu)/dt = ρ ∂ₜu`, and the crossing
into the existing generic evolution law, both at the level of the assembled mechanical data
and at the level of the existing adapter interface.
* **Block B (pressure-gauge information boundary).** The pressure enters the dynamics only
through its gradient; adding a spatially constant (possibly time-dependent) shift leaves the
gradient, the aggregate force, the assembled mechanical data and the evolution readout
unchanged, and absolute pressure is therefore not a function of that readout.
* **Block C (kinetic energy and viscous dissipation).** Under explicit, individually named
classical hypotheses — advection cancellation, pressure cancellation, viscous integration by
parts, and differentiability of the velocity `L²` profile — the kinetic energy has derivative
`-D_visc`, the dissipation is nonnegative, and the kinetic energy is nonincreasing.
* **Block D (integrated energy balance).** Under an explicit interval-integrability
hypothesis, `E_kin(t₂) + D[t₁,t₂] = E_kin(t₁)`, hence `E_kin(t₂) ≤ E_kin(t₁)`.
## Modelling posture
The package is deliberately operator-form: spatial differential operators (`∇`, `∆`, `∇·`) and
the spatial integral pairings appearing in the energy identities are supplied as data, and the
classical facts about them (cancellation of the advection and pressure pairings, integration by
parts for the viscous term) appear as *explicit named hypotheses*, never as a single opaque
"energy decreases" premise. Nothing here addresses existence, uniqueness, regularity or
smoothness of solutions, and nothing here is a statement about the three-dimensional
Navier–Stokes global regularity problem.
Each Navier–Stokes term keeps its own native identity: the aggregate `F_NS` is what crosses the
interface, and no individual term is given a further interpretation.
-/
namespace ResonantEvolution.NavierStokesReduction
open ResonantEvolution.NewtonianReduction
open ResonantEvolution.NewtonianReduction.MechanicalData
open ResonantEvolution.ReductionAdapter
/-! ## 1. Operator surface
`U` is the space of velocity-type fields, `P` the space of pressure-type fields, `W` the target
of the divergence operator. All spatial operators are supplied as linear maps. -/
variable {U P W : Type} [NormedAddCommGroup U] [NormedSpace ℝ U]
[AddCommGroup P] [Module ℝ P] [AddCommGroup W] [Module ℝ W]
/-- The pressure representation: a linear gradient operator, the spatially constant fields, and
the two facts that make the gauge block meaningful — constants are annihilated by the gradient,
and at least one constant field is nonzero. -/
structure PressureModel (P U : Type) [AddCommGroup P] [Module ℝ P]
[AddCommGroup U] [Module ℝ U] where
/-- The spatial gradient `∇ : P → U`. -/
grad : P →ₗ[ℝ] U
/-- The spatially constant pressure field with value `c`. -/
constField : ℝ → P
/-- Constants have vanishing gradient. -/
grad_constField : ∀ c, grad (constField c) = 0
/-- The constant shifts are not all trivial. -/
constField_nontrivial : ∃ c, constField c ≠ 0
/-- One time-instant of the native Navier–Stokes state: the velocity, its time derivative, the
advection field `(u·∇)u`, the viscous action `∆u`, and the pressure. -/
structure FlowState (U P : Type) where
/-- The velocity field `u`. -/
velocity : U
/-- The Eulerian time derivative `∂ₜu`. -/
timeDeriv : U
/-- The advection field `(u·∇)u`. -/
advection : U
/-- The viscous action `∆u`. -/
viscousAction : U
/-- The pressure `p`. -/
pressure : P
/-- The pressure gradient readout `∇p` of a flow state. -/
def pressureGradient (M : PressureModel P U) (s : FlowState U P) : U := M.grad s.pressure
/-- The native aggregate Navier–Stokes force `F_NS = -ρ(u·∇)u - ∇p + µ∆u`. -/
def nsEffectiveForce (rho mu : ℝ) (M : PressureModel P U) (s : FlowState U P) : U :=
-(rho • s.advection) - pressureGradient M s + mu • s.viscousAction
/-- Incompressibility `∇·u = 0`, declared along a trajectory. -/
def IsIncompressible (divOp : U →ₗ[ℝ] W) (x : ℝ → FlowState U P) : Prop :=
∀ t, divOp (x t).velocity = 0
/-- The restricted Navier–Stokes source law: constant positive density, nonnegative viscosity,
incompressibility, differentiability of the velocity with the recorded time derivative, and the
native momentum balance `ρ ∂ₜu = F_NS`. -/
structure SatisfiesNS (rho mu : ℝ) (M : PressureModel P U) (divOp : U →ₗ[ℝ] W)
(x : ℝ → FlowState U P) : Prop where
/-- Constant density is positive. -/
density_pos : 0 < rho
/-- Dynamic viscosity is nonnegative. -/
viscosity_nonneg : 0 ≤ mu
/-- The flow is incompressible. -/
incompressible : IsIncompressible divOp x
/-- The recorded field `timeDeriv` is the time derivative of the velocity. -/
velocity_hasDerivAt : ∀ t, HasDerivAt (fun s => (x s).velocity) (x t).timeDeriv t
/-- The native momentum balance `ρ ∂ₜu = F_NS`. -/
momentum_balance : ∀ t, rho • (x t).timeDeriv = nsEffectiveForce rho mu M (x t)
/-! ## 2. Block A — momentum correspondence -/
/-- **Native momentum equation.** Along a solution, `ρ ∂ₜu = -ρ(u·∇)u - ∇p + µ∆u`. -/
theorem ns_momentum_balance {rho mu : ℝ} {M : PressureModel P U} {divOp : U →ₗ[ℝ] W}
{x : ℝ → FlowState U P} (h : SatisfiesNS rho mu M divOp x) (t : ℝ) :
rho • (x t).timeDeriv
= -(rho • (x t).advection) - M.grad (x t).pressure + mu • (x t).viscousAction :=
h.momentum_balance t
/-- **Constant-density momentum derivative.** `d(ρu)/dt = ρ ∂ₜu`. -/
theorem ns_constantDensity_momentum_derivative {rho mu : ℝ} {M : PressureModel P U}
{divOp : U →ₗ[ℝ] W} {x : ℝ → FlowState U P} (h : SatisfiesNS rho mu M divOp x) (t : ℝ) :
HasDerivAt (fun s => rho • (x s).velocity) (rho • (x t).timeDeriv) t :=
(h.velocity_hasDerivAt t).const_smul rho
/-- The Navier–Stokes adapter into the existing Construct layer: constant inertia `ρ`, the
native velocity, the aggregate force `F_NS` as the single force channel, and explicitly zero
remaining channels. No individual Navier–Stokes term is identified with any particular
channel. -/
def nsAdapter (rho mu : ℝ) (M : PressureModel P U) : Adapter (FlowState U P) U where
encode := fun s =>
{ inertia := rho
velocity := s.velocity
drive := nsEffectiveForce rho mu M s
resistance := 0
memory := 0
constraint := 0 }
/-- The mechanical data of the existing generic interface obtained from a Navier–Stokes
trajectory. -/
def nsMechanical (rho mu : ℝ) (M : PressureModel P U) (x : ℝ → FlowState U P) :
MechanicalData U :=
(nsAdapter rho mu M).mech x
@[simp] theorem nsMechanical_inertia (rho mu : ℝ) (M : PressureModel P U)
(x : ℝ → FlowState U P) (t : ℝ) : (nsMechanical rho mu M x).inertia t = rho := rfl
@[simp] theorem nsMechanical_velocity (rho mu : ℝ) (M : PressureModel P U)
(x : ℝ → FlowState U P) (t : ℝ) :
(nsMechanical rho mu M x).velocity t = (x t).velocity := rfl
@[simp] theorem nsMechanical_effectiveForce (rho mu : ℝ) (M : PressureModel P U)
(x : ℝ → FlowState U P) (t : ℝ) :
(nsMechanical rho mu M x).effectiveForce t = nsEffectiveForce rho mu M (x t) := by
simp [nsMechanical, Adapter.mech, Adapter.push, nsAdapter, MechanicalData.effectiveForce,
toMechanical]
/-- **Crossing into the existing generic evolution law.** A solution of the restricted
Navier–Stokes source satisfies the repository's generic constant-inertia evolution predicate
`d/dt (𝓘 v) = F_eff`, with `𝓘 = ρ` and `F_eff = F_NS`. -/
theorem ns_generalEvolution {rho mu : ℝ} {M : PressureModel P U} {divOp : U →ₗ[ℝ] W}
{x : ℝ → FlowState U P} (h : SatisfiesNS rho mu M divOp x) :
SatisfiesGeneralEvolution (nsMechanical rho mu M x) := by
intro t
have hmom : HasDerivAt (nsMechanical rho mu M x).momentum (rho • (x t).timeDeriv) t :=
hasDerivAt_momentum_of_constant_inertia _ rho t _ (fun _ => rfl) (h.velocity_hasDerivAt t)
rw [nsMechanical_effectiveForce, ← h.momentum_balance t]
exact hmom
/-- The restricted Navier–Stokes source, packaged as a source system of the existing adapter
interface. -/
def nsSource (rho mu : ℝ) (M : PressureModel P U) (divOp : U →ₗ[ℝ] W) :
SourceSystem (FlowState U P) where
Law := fun x => SatisfiesNS rho mu M divOp x
/-- **Adapter-level preservation.** The Navier–Stokes adapter carries every solution of the
source law to data satisfying the existing generic evolution law. -/
theorem ns_adapter_preservesEvolution (rho mu : ℝ) (M : PressureModel P U)
(divOp : U →ₗ[ℝ] W) :
PreservesEvolution (nsSource rho mu M divOp) (nsAdapter rho mu M) :=
fun _ hx => ns_generalEvolution hx
/-! ## 3. Block B — pressure-gauge information boundary -/
/-- **Gauge invariance of the pressure gradient**: `∇(p + C) = ∇p` for a spatially constant
`C`. -/
@[simp] theorem pressureGradient_addConstant (M : PressureModel P U) (p : P) (c : ℝ) :
M.grad (p + M.constField c) = M.grad p := by
simp [M.grad_constField c]
/-- The admissible gauge shift of a flow state: add a spatially constant pressure. -/
def gaugeShift (M : PressureModel P U) (c : ℝ) (s : FlowState U P) : FlowState U P :=
{ s with pressure := s.pressure + M.constField c }
/-- The gauge shift of a trajectory by a spatially constant, possibly time-dependent, `C`. -/
def gaugeShiftTrajectory (M : PressureModel P U) (C : ℝ → ℝ) (x : ℝ → FlowState U P) :
ℝ → FlowState U P := fun t => gaugeShift M (C t) (x t)
@[simp] theorem pressureGradient_gaugeShift (M : PressureModel P U) (c : ℝ)
(s : FlowState U P) : pressureGradient M (gaugeShift M c s) = pressureGradient M s := by
simp [pressureGradient, gaugeShift]
/-- **Gauge invariance of the aggregate force.** -/
@[simp] theorem effectiveForce_pressureGaugeInvariant (rho mu : ℝ) (M : PressureModel P U)
(c : ℝ) (s : FlowState U P) :
nsEffectiveForce rho mu M (gaugeShift M c s) = nsEffectiveForce rho mu M s := by
simp [nsEffectiveForce, pressureGradient, gaugeShift, map_add, M.grad_constField]
/-- **Gauge invariance of the assembled mechanical data.** -/
theorem nsMechanical_pressureGaugeInvariant (rho mu : ℝ) (M : PressureModel P U) (C : ℝ → ℝ)
(x : ℝ → FlowState U P) :
nsMechanical rho mu M (gaugeShiftTrajectory M C x) = nsMechanical rho mu M x := by
simp [nsMechanical, Adapter.mech, Adapter.push, nsAdapter, toMechanical,
gaugeShiftTrajectory, gaugeShift, nsEffectiveForce, pressureGradient, map_add,
M.grad_constField]
/-- **Gauge invariance of the source law**: a gauge-shifted solution is a solution. -/
theorem satisfiesNS_gaugeShift {rho mu : ℝ} {M : PressureModel P U} {divOp : U →ₗ[ℝ] W}
{x : ℝ → FlowState U P} (h : SatisfiesNS rho mu M divOp x) (C : ℝ → ℝ) :
SatisfiesNS rho mu M divOp (gaugeShiftTrajectory M C x) where
density_pos := h.density_pos
viscosity_nonneg := h.viscosity_nonneg
incompressible := fun t => h.incompressible t
velocity_hasDerivAt := fun t => h.velocity_hasDerivAt t
momentum_balance := fun t => by
simpa [gaugeShiftTrajectory] using h.momentum_balance t
/-- **Gauge invariance of the evolution readout.** The generic evolution predicate produced by
the correspondence is unchanged by an admissible pressure shift. -/
theorem evolution_pressureGaugeInvariant {rho mu : ℝ} {M : PressureModel P U}
{divOp : U →ₗ[ℝ] W} {x : ℝ → FlowState U P} (h : SatisfiesNS rho mu M divOp x)
(C : ℝ → ℝ) :
SatisfiesGeneralEvolution (nsMechanical rho mu M (gaugeShiftTrajectory M C x))
∧ nsMechanical rho mu M (gaugeShiftTrajectory M C x) = nsMechanical rho mu M x :=
⟨ns_generalEvolution (satisfiesNS_gaugeShift h C),
nsMechanical_pressureGaugeInvariant rho mu M C x⟩
/-- **Explicit noninjectivity witness**: two distinct pressures with the same gradient. -/
theorem exists_distinct_pressures_same_gradient (M : PressureModel P U) :
∃ p₁ p₂ : P, p₁ ≠ p₂ ∧ M.grad p₁ = M.grad p₂ := by
obtain ⟨c, hc⟩ := M.constField_nontrivial
refine ⟨0, M.constField c, ?_, ?_⟩
· exact fun h => hc h.symm
· simp [M.grad_constField c]
/-- **Absolute pressure is not reconstructible from the gradient channel.** There is no map
recovering the pressure of a flow state from its pressure-gradient readout; a gauge must be
fixed first. -/
theorem absolutePressure_not_reconstructible (M : PressureModel P U) :
¬ ∃ recover : U → P, ∀ s : FlowState U P, recover (pressureGradient M s) = s.pressure := by
rintro ⟨recover, hrec⟩
obtain ⟨c, hc⟩ := M.constField_nontrivial
have h₁ := hrec ⟨0, 0, 0, 0, 0⟩
have h₂ := hrec ⟨0, 0, 0, 0, M.constField c⟩
simp [pressureGradient, M.grad_constField c] at h₁ h₂
exact hc (h₂.symm.trans h₁)
/-! ## 4. Block C — native kinetic energy and viscous dissipation
The spatial integrals appearing in the classical energy computation are supplied as scalar
profiles; the classical facts relating them are the explicit hypotheses of
`ClassicalEnergyHypotheses`. -/
/-- The scalar spatial readouts used by the energy block:
`velocitySq t = ∫_Ω |u(t,x)|² dx`, `gradientSq t = ∫_Ω |∇u(t,x)|² dx`,
`advectionPairing t = ∫_Ω u·(u·∇)u dx`, `pressurePairing t = ∫_Ω u·∇p dx`,
`viscousPairing t = ∫_Ω u·∆u dx`, and `velocitySqDeriv` the time derivative of
`velocitySq`. -/
structure EnergyProfile where
/-- `∫_Ω |u(t,x)|² dx`. -/
velocitySq : ℝ → ℝ
/-- The time derivative of `velocitySq`. -/
velocitySqDeriv : ℝ → ℝ
/-- `∫_Ω |∇u(t,x)|² dx`. -/
gradientSq : ℝ → ℝ
/-- `∫_Ω u·(u·∇)u dx`. -/
advectionPairing : ℝ → ℝ
/-- `∫_Ω u·∇p dx`. -/
pressurePairing : ℝ → ℝ
/-- `∫_Ω u·∆u dx`. -/
viscousPairing : ℝ → ℝ
/-- Kinetic energy `E_kin(t) = (ρ/2) ∫_Ω |u(t,x)|² dx`. -/
noncomputable def kineticEnergy (rho : ℝ) (E : EnergyProfile) : ℝ → ℝ :=
fun t => rho / 2 * E.velocitySq t
/-- Viscous dissipation `D_visc(t) = µ ∫_Ω |∇u(t,x)|² dx`. -/
def viscousDissipation (mu : ℝ) (E : EnergyProfile) : ℝ → ℝ := fun t => mu * E.gradientSq t
/-- The explicit classical hypotheses used by the energy block: nonnegativity of the Dirichlet
profile, differentiability of the velocity `L²` profile, the two cancellation receipts, the
viscous integration-by-parts receipt, and the pairing of the momentum equation with the
velocity. Each requirement is a separate named field. -/
structure ClassicalEnergyHypotheses (rho mu : ℝ) (E : EnergyProfile) : Prop where
/-- `∫_Ω |∇u|² dx ≥ 0`. -/
gradientSq_nonneg : ∀ t, 0 ≤ E.gradientSq t
/-- `∫_Ω |u|² dx` is differentiable in time with derivative `velocitySqDeriv`. -/
velocitySq_hasDerivAt : ∀ t, HasDerivAt E.velocitySq (E.velocitySqDeriv t) t
/-- Advection cancellation `∫_Ω u·(u·∇)u dx = 0` (incompressibility and boundary behaviour). -/
advection_cancellation : ∀ t, E.advectionPairing t = 0
/-- Pressure cancellation `∫_Ω u·∇p dx = 0` (incompressibility and boundary behaviour). -/
pressure_cancellation : ∀ t, E.pressurePairing t = 0
/-- Viscous integration by parts `µ ∫_Ω u·∆u dx = -µ ∫_Ω |∇u|² dx`. -/
viscous_integrationByParts : ∀ t, mu * E.viscousPairing t = -(mu * E.gradientSq t)
/-- Pairing the momentum equation with `u` and integrating:
`(ρ/2) d/dt ∫|u|² = -ρ ∫u·(u·∇)u - ∫u·∇p + µ ∫u·∆u`. -/
energy_pairing : ∀ t, rho / 2 * E.velocitySqDeriv t
= -(rho * E.advectionPairing t) - E.pressurePairing t + mu * E.viscousPairing t
/-- **Nonnegativity of the viscous dissipation** for `µ ≥ 0`. -/
theorem viscousDissipation_nonnegative {rho mu : ℝ} {E : EnergyProfile} (hmu : 0 ≤ mu)
(h : ClassicalEnergyHypotheses rho mu E) (t : ℝ) : 0 ≤ viscousDissipation mu E t :=
mul_nonneg hmu (h.gradientSq_nonneg t)
/-- **Advection receipt**: `∫_Ω u·(u·∇)u dx = 0`. -/
theorem advection_energy_neutral {rho mu : ℝ} {E : EnergyProfile}
(h : ClassicalEnergyHypotheses rho mu E) (t : ℝ) : E.advectionPairing t = 0 :=
h.advection_cancellation t
/-- **Pressure receipt**: `∫_Ω u·∇p dx = 0`. -/
theorem pressure_energy_neutral {rho mu : ℝ} {E : EnergyProfile}
(h : ClassicalEnergyHypotheses rho mu E) (t : ℝ) : E.pressurePairing t = 0 :=
h.pressure_cancellation t
/-- **Viscosity receipt**: `µ ∫_Ω u·∆u dx = -D_visc`. -/
theorem viscosity_energy_identity {rho mu : ℝ} {E : EnergyProfile}
(h : ClassicalEnergyHypotheses rho mu E) (t : ℝ) :
mu * E.viscousPairing t = -viscousDissipation mu E t :=
h.viscous_integrationByParts t
/-- **Energy balance in differential form**: `dE_kin/dt = -D_visc`, obtained by combining the
three receipts with the pairing identity. -/
theorem kineticEnergy_derivative_eq_neg_dissipation {rho mu : ℝ} {E : EnergyProfile}
(h : ClassicalEnergyHypotheses rho mu E) (t : ℝ) :
HasDerivAt (kineticEnergy rho E) (-viscousDissipation mu E t) t := by
have hd : HasDerivAt (kineticEnergy rho E) (rho / 2 * E.velocitySqDeriv t) t :=
((h.velocitySq_hasDerivAt t).const_mul (rho / 2))
have hval : rho / 2 * E.velocitySqDeriv t = -viscousDissipation mu E t := by
rw [h.energy_pairing t, h.advection_cancellation t, h.pressure_cancellation t,
h.viscous_integrationByParts t]
simp [viscousDissipation]
rwa [hval] at hd
/-- The kinetic energy is differentiable in time. -/
theorem kineticEnergy_differentiable {rho mu : ℝ} {E : EnergyProfile}
(h : ClassicalEnergyHypotheses rho mu E) : Differentiable ℝ (kineticEnergy rho E) :=
fun t => (kineticEnergy_derivative_eq_neg_dissipation (mu := mu) h t).differentiableAt
/-- **Kinetic energy is nonincreasing** for `µ ≥ 0`. -/
theorem kineticEnergy_nonincreasing {rho mu : ℝ} {E : EnergyProfile} (hmu : 0 ≤ mu)
(h : ClassicalEnergyHypotheses rho mu E) : Antitone (kineticEnergy rho E) := by
refine antitone_of_deriv_nonpos (kineticEnergy_differentiable (mu := mu) h) (fun t => ?_)
rw [(kineticEnergy_derivative_eq_neg_dissipation (mu := mu) h t).deriv]
exact neg_nonpos.mpr (viscousDissipation_nonnegative hmu h t)
/-! ## 5. Block D — integrated energy balance -/
/-- Accumulated viscous dissipation `D[t₁,t₂] = ∫_{t₁}^{t₂} D_visc(s) ds`. -/
noncomputable def accumulatedViscousDissipation (mu : ℝ) (E : EnergyProfile) (t₁ t₂ : ℝ) : ℝ :=
∫ s in t₁..t₂, viscousDissipation mu E s
/-- **Nonnegativity of the accumulated dissipation** on `t₁ ≤ t₂`. -/
theorem accumulatedViscousDissipation_nonnegative {rho mu : ℝ} {E : EnergyProfile}
(hmu : 0 ≤ mu) (h : ClassicalEnergyHypotheses rho mu E) {t₁ t₂ : ℝ} (hle : t₁ ≤ t₂) :
0 ≤ accumulatedViscousDissipation mu E t₁ t₂ :=
intervalIntegral.integral_nonneg hle
(fun s _ => viscousDissipation_nonnegative hmu h s)
/-- **Interval energy balance**: `E_kin(t₂) + D[t₁,t₂] = E_kin(t₁)`, under the explicit
interval-integrability hypothesis for the dissipation. -/
theorem kineticEnergy_interval_balance {rho mu : ℝ} {E : EnergyProfile}
(h : ClassicalEnergyHypotheses rho mu E) {t₁ t₂ : ℝ}
(hint : IntervalIntegrable (viscousDissipation mu E) MeasureTheory.volume t₁ t₂) :
kineticEnergy rho E t₂ + accumulatedViscousDissipation mu E t₁ t₂
= kineticEnergy rho E t₁ := by
have hFTC : (∫ s in t₁..t₂, -viscousDissipation mu E s)
= kineticEnergy rho E t₂ - kineticEnergy rho E t₁ :=
intervalIntegral.integral_eq_sub_of_hasDerivAt
(fun s _ => kineticEnergy_derivative_eq_neg_dissipation (mu := mu) h s) hint.neg
rw [intervalIntegral.integral_neg] at hFTC
have : accumulatedViscousDissipation mu E t₁ t₂
= kineticEnergy rho E t₁ - kineticEnergy rho E t₂ := by
rw [accumulatedViscousDissipation]; linarith [hFTC]
rw [this]; ring
/-- **Interval monotonicity**: `E_kin(t₂) ≤ E_kin(t₁)` for `t₁ ≤ t₂`. -/
theorem kineticEnergy_interval_nonincreasing {rho mu : ℝ} {E : EnergyProfile} (hmu : 0 ≤ mu)
(h : ClassicalEnergyHypotheses rho mu E) {t₁ t₂ : ℝ} (hle : t₁ ≤ t₂)
(hint : IntervalIntegrable (viscousDissipation mu E) MeasureTheory.volume t₁ t₂) :
kineticEnergy rho E t₂ ≤ kineticEnergy rho E t₁ := by
have hbal := kineticEnergy_interval_balance h hint
have hnn := accumulatedViscousDissipation_nonnegative hmu h hle
linarith
/-! ## 6. Non-vacuity witnesses
The hypothesis packages above are satisfiable: a one-dimensional pressure representation with a
nontrivial constant channel exists, and both `SatisfiesNS` and `ClassicalEnergyHypotheses` have
explicit models. This rules out the possibility that the results hold only vacuously. -/
/-- A minimal pressure representation: pressures are pairs (value, slope), the gradient reads the
slope, and the constant field of value `c` has zero slope. -/
def samplePressureModel : PressureModel (ℝ × ℝ) ℝ where
grad := (LinearMap.snd ℝ ℝ ℝ)
constField := fun c => (c, 0)
grad_constField := fun _ => rfl
constField_nontrivial := ⟨1, by simp⟩
/-- The rest state is a solution of the restricted source law, for every `ρ > 0` and `µ ≥ 0`. -/
theorem satisfiesNS_rest {rho mu : ℝ} (hrho : 0 < rho) (hmu : 0 ≤ mu) :
SatisfiesNS rho mu samplePressureModel (0 : ℝ →ₗ[ℝ] ℝ)
(fun _ => ⟨0, 0, 0, 0, (0, 0)⟩) where
density_pos := hrho
viscosity_nonneg := hmu
incompressible := fun _ => rfl
velocity_hasDerivAt := fun _ => hasDerivAt_const _ _
momentum_balance := fun _ => by simp [nsEffectiveForce, pressureGradient, samplePressureModel]
/-- The identically vanishing energy profile satisfies the classical energy hypotheses. -/
theorem classicalEnergyHypotheses_zero (rho mu : ℝ) :
ClassicalEnergyHypotheses rho mu ⟨0, 0, 0, 0, 0, 0⟩ where
gradientSq_nonneg := fun _ => le_rfl
velocitySq_hasDerivAt := fun _ => hasDerivAt_const _ _
advection_cancellation := fun _ => rfl
pressure_cancellation := fun _ => rfl
viscous_integrationByParts := fun _ => by simp
energy_pairing := fun _ => by simp
/-! ## 7. Axiom audit for the headline results -/
#print axioms ns_momentum_balance
#print axioms ns_constantDensity_momentum_derivative
#print axioms ns_generalEvolution
#print axioms ns_adapter_preservesEvolution
#print axioms effectiveForce_pressureGaugeInvariant
#print axioms evolution_pressureGaugeInvariant
#print axioms absolutePressure_not_reconstructible
#print axioms kineticEnergy_derivative_eq_neg_dissipation
#print axioms kineticEnergy_nonincreasing
#print axioms kineticEnergy_interval_balance
#print axioms kineticEnergy_interval_nonincreasing
end ResonantEvolution.NavierStokesReduction
Verification
The source includes #print axioms checks for the headline correspondence, gauge, energy and interval results. The reported audit contains no new project axioms and only the standard dependencies propext, Classical.choice, and Quot.sound.
Claim Boundary
This package does not address existence, uniqueness, regularity, smoothness, weak solutions, compressible flow, turbulence closure, relativistic hydrodynamics, or the Navier–Stokes Millennium Prize problem.
It is a restricted operator-form classical-solution correspondence and a formal accounting of the stated preservation, information-boundary and conditional energy results.