IndisputableMonolith.ClassicalBridge.Fluids.CPM

   1import Mathlib
   2import IndisputableMonolith.CPM.LawOfExistence
   3
   4namespace IndisputableMonolith
   5namespace ClassicalBridge
   6namespace Fluids
   7
   8/-!
   9# Fluids Bridge: CPM interface
  10
  11The CPM core (`IndisputableMonolith/CPM/LawOfExistence.lean`) is domain-agnostic.
  12For Navier–Stokes we must *instantiate* it with:
  13
  14- a state type (discrete NS state),
  15- concrete functionals (defectMass, orthoMass, energyGap, tests), and
  16- proofs of the required inequalities (A/B/C).
  17
  18This file defines a minimal bundle to carry such an instantiation for later reuse.
  19-/
  20
  21open IndisputableMonolith.CPM.LawOfExistence
  22
  23/-- A CPM instantiation for a particular state type. -/
  24structure CPMBridge (State : Type) where
  25  /-- The fully packaged CPM model (includes the A/B/C inequality proofs). -/
  26  model : Model State
  27  /-- Human-readable interpretation notes (kept here for traceability). -/
  28  defectMeaning : String := ""
  29  energyMeaning  : String := ""
  30  testsMeaning   : String := ""
  31
  32end Fluids
  33end ClassicalBridge
  34end IndisputableMonolith
  35