`model`

definition

show as: view math explainer →

module: IndisputableMonolith.ClassicalBridge.Fluids.CPM2D
domain: ClassicalBridge
line: 50 · 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 50.

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

  47  dispersion        : ∀ a : State N, F.orthoMass a ≤ C.Cdisp * F.tests a
  48
  49/-- Build a CPM `Model` from the hypothesis bundle. -/
  50noncomputable def model {N : ℕ} (H : Hypothesis N) : Model (State N) :=
  51  { C := H.C
  52    defectMass := H.F.defectMass
  53    orthoMass  := H.F.orthoMass
  54    energyGap  := H.F.energyGap
  55    tests      := H.F.tests
  56    projection_defect := H.projection_defect
  57    energy_control    := H.energy_control
  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

papers checked against this theorem

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