RSNSBridgeSpec
plain-language theorem explainer
RSNSBridgeSpec packages the interface requirements for deriving Navier-Stokes regularity from Recognition Science at the specification level. It collects NS parameters, a discrete model, LNAL program with encode/decode maps, a simulation proposition, CPM bridge, and three key propositions for bounds, limit, and regularity. Workers on RS-native fluid proofs would cite this structure to organize the bridge components. The declaration is a plain structure definition whose verified abbreviation simply conjoins the four propositions.
Claim. A structure consisting of NS parameters, a time step, a discrete model, an LNAL program, spatial semantics, encoding and decoding maps between discrete states and LNAL fields, a proposition asserting that LNAL simulates the discrete model, a CPM bridge on the discrete state, and propositions asserting uniform bounds, the discrete-to-continuum limit, and global regularity.
background
The module supplies an interface for an RS-native proof of Navier-Stokes properties. It requires a DiscreteModel for the discrete approximation, an LNAL program together with SpatialSemantics and encode/decode maps, a simulation statement, a CPMBridge instantiation, and three propositions that must later be proved: uniformBounds, continuumLimit, and globalRegularity. The module doc states that the file intentionally avoids proving these statements up front and instead defines the objects to be implemented later.
proof idea
The declaration is a structure definition that assembles the listed fields. The accompanying verified abbreviation is a one-line wrapper that returns the conjunction of simulates, uniformBounds, continuumLimit, and globalRegularity.
why it matters
This structure serves as the central specification for the RS-NS bridge inside the Recognition framework. It records the exact sequence of objects and statements needed to pass from a discrete RS model through LNAL semantics and CPM to a continuum regularity result. No downstream theorems yet reference it, leaving the concrete discharge of the three propositions as an open implementation task.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.