`Hypothesis`

definition

show as: view math explainer →

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

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

  36
  37This is *exactly* the data needed to build a `CPM.LawOfExistence.Model`.
  38-/
  39structure Hypothesis (N : ℕ) where
  40  C : Constants
  41  F : Functionals N
  42  /- Projection-Defect (A): D ≤ K_net · C_proj · ||proj_{S⊥}||² -/
  43  projection_defect : ∀ a : State N, F.defectMass a ≤ C.Knet * C.Cproj * F.orthoMass a
  44  /- Energy control (B): ||proj_{S⊥}||² ≤ C_eng · (E−E₀) -/
  45  energy_control    : ∀ a : State N, F.orthoMass a ≤ C.Ceng * F.energyGap a
  46  /- Dispersion/interface (C): ||proj_{S⊥}||² ≤ C_disp · sup tests -/
  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

papers checked against this theorem

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