pith. machine review for the scientific record. sign in
def definition def or abbrev

bridge

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  61noncomputable def bridge {N : ℕ} (H : Hypothesis N) : ClassicalBridge.Fluids.CPMBridge (State N) :=

proof body

Definition body.

  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. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (40)

Lean names referenced from this declaration's body.

… and 10 more