`bridge`

definition

show as: view math explainer →

module: IndisputableMonolith.ClassicalBridge.Fluids.CPM2D
domain: ClassicalBridge
line: 61 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.ClassicalBridge.Fluids.CPM2D on GitHub at line 61.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  58    dispersion        := H.dispersion }
  59
  60/-- Pack the `Model` into the bridge-local `CPMBridge` structure (for traceability notes). -/
  61noncomputable def bridge {N : ℕ} (H : Hypothesis N) : ClassicalBridge.Fluids.CPMBridge (State N) :=
  62  { model := model H
  63    defectMeaning := "Galerkin2D defectMass: discrete distance to structured (e.g. divergence-free / low-cost) subspace."
  64    energyMeaning := "Galerkin2D energyGap: discrete kinetic energy gap above the structured baseline."
  65    testsMeaning  := "Galerkin2D tests: supremum of local dispersion / window tests on the discrete state." }
  66
  67/-!
  68## A fully proved (but minimal) concrete instantiation
  69
  70To reduce the hypothesis layer, we provide an explicit choice of CPM constants and functionals
  71for which the A/B/C inequalities are **provable by reflexivity**.
  72
  73This is not yet the physically meaningful CPM for fluids; it is a useful “base instance” that
  74lets downstream modules stop carrying `Hypothesis` when they only need a concrete CPM model.
  75-/
  76
  77/-- A convenient all-ones constant bundle. -/
  78noncomputable def constantsOne : Constants :=
  79  { Knet := 1
  80    Cproj := 1
  81    Ceng := 1
  82    Cdisp := 1
  83    Knet_nonneg := by norm_num
  84    Cproj_nonneg := by norm_num
  85    Ceng_nonneg := by norm_num
  86    Cdisp_nonneg := by norm_num }
  87
  88/-- Concrete functionals: everything is measured by `‖u‖^2` (a nonnegative scalar). -/
  89noncomputable def functionalsNormSq (N : ℕ) : Functionals N :=
  90  { defectMass := fun u => ‖u‖ ^ 2
  91    orthoMass  := fun u => ‖u‖ ^ 2

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.