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

model

show as:
view Lean formalization →

This definition assembles a CPM Model for the truncated 2D Galerkin state from a supplied Hypothesis bundle that encodes the required functionals and control inequalities. Fluid dynamicists using spectral methods to approximate Navier-Stokes flows would reference it when embedding the Recognition cost structure into a discrete model. The construction is a direct record literal that transfers the defectMass, orthoMass, energyGap, tests, and the three control inequalities straight from the hypothesis fields.

claimLet $H$ be a hypothesis bundle for truncation level $N$, containing constants $C$, functionals $F$, and the three control inequalities (projection-defect bound on defect mass, energy-control bound on orthogonal mass, and dispersion bound). The CPM model for the Galerkin state at level $N$ is the instance whose cost functional is $C$, defect mass is $F$'s defect mass, orthogonal mass is $F$'s orthogonal mass, energy gap is $F$'s energy gap, tests are $F$'s tests, and whose three control inequalities are exactly the projection-defect, energy-control, and dispersion statements supplied in $H$.

background

The CPM2D module instantiates the CPM core from LawOfExistence for the finite-dimensional 2D Galerkin model. State is the abbrev for GalerkinState at truncation level $N$. The Hypothesis structure packages constants $C$, the four functionals (defectMass, orthoMass, energyGap, tests), and the three explicit inequalities: projection_defect requires defectMass $a$ ≤ $K_{net} · C_{proj} ·$ orthoMass $a$; energy_control requires orthoMass $a$ ≤ $C_{eng} ·$ energyGap $a$; dispersion requires orthoMass $a$ ≤ $C_{disp} ·$ tests $a$ for every state $a$. Upstream, CostAlgebra.H reparametrizes the base cost to $H(x) = J(x) + 1$, converting the Recognition Composition Law into the standard d'Alembert form $H(xy) + H(x/y) = 2 H(x) H(y)$.

proof idea

The definition is a direct record construction that populates every field of the Model structure by selecting the matching component from the input Hypothesis: C from H.C, defectMass from H.F.defectMass, orthoMass from H.F.orthoMass, energyGap from H.F.energyGap, tests from H.F.tests, and the three inequalities from the corresponding Hypothesis fields projection_defect, energy_control, and dispersion.

why it matters in Recognition Science

This definition supplies the concrete Model instance required by the CPMBridge structure and thereby feeds the RSNSBridgeSpec and DiscreteModel used in classical fluids approximations. It realizes milestone M4 by packaging the Galerkin-specific controls for the Recognition Science cost model, allowing traceability from the discrete state to the underlying J-cost functional without proving the inequalities here. It connects to the broader framework by instantiating the Model type from LawOfExistence for use in bridge constructions to Navier-Stokes.

scope and limits

formal statement (Lean)

  50noncomputable def model {N : ℕ} (H : Hypothesis N) : Model (State N) :=

proof body

Definition body.

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

used by (40)

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

… and 10 more

depends on (17)

Lean names referenced from this declaration's body.