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

RSNSBridgeSpec

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)

  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 :=

proof body

Definition body.

  55  S.simulates ∧ S.uniformBounds ∧ S.continuumLimit ∧ S.globalRegularity
  56
  57end Fluids
  58end ClassicalBridge
  59end IndisputableMonolith

depends on (24)

Lean names referenced from this declaration's body.