`RSNSBridgeSpec`

definition

show as: view math explainer →

module: IndisputableMonolith.ClassicalBridge.Fluids.Bridge
domain: ClassicalBridge
line: 26 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.ClassicalBridge.Fluids.Bridge on GitHub at line 26.

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

formal source

  23-/
  24
  25/-- Bundle of RS↔NS bridge requirements (spec-level). -/
  26structure RSNSBridgeSpec where
  27  /- Parameters and discrete approximation -/
  28  params   : NSParams
  29  dt       : TimeStep
  30  discrete : DiscreteModel
  31
  32  /- LNAL side -/
  33  program   : IndisputableMonolith.LNAL.LProgram
  34  semantics : SpatialSemantics
  35  encode    : discrete.State → LNALField
  36  decode    : LNALField → discrete.State
  37
  38  /- Correctness statements (to be proved, or made explicit hypotheses) -/
  39  /-- LNAL simulates the discrete model (exactly or with a stated error model). -/
  40  simulates : Prop
  41
  42  /- CPM instantiation -/
  43  cpm : CPMBridge discrete.State
  44
  45  /- Analysis-layer outcomes -/
  46  /-- Uniform bounds needed to pass to the continuum (typically independent of truncation). -/
  47  uniformBounds : Prop
  48  /-- Discrete → continuum limit theorem in the chosen solution concept. -/
  49  continuumLimit : Prop
  50  /-- The final global regularity statement (the target theorem). -/
  51  globalRegularity : Prop
  52
  53/-- “Verified” just means all declared bridge properties hold. -/
  54@[simp] def RSNSBridgeSpec.verified (S : RSNSBridgeSpec) : Prop :=
  55  S.simulates ∧ S.uniformBounds ∧ S.continuumLimit ∧ S.globalRegularity
  56

papers checked against this theorem

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