partialDifferentialEquationsCert
plain-language theorem explainer
This definition supplies a Lean certificate asserting that the Recognition Science framework produces exactly five canonical partial differential equation types when the configuration dimension is five. A researcher deriving continuum equations from the J-cost functional would cite it to fix the classification of elliptic, parabolic, hyperbolic, mixed, and integro-differential forms. It is realized as a one-line wrapper that populates the structure field with the decidable cardinality result.
Claim. Let PDEType be the finite type of canonical partial differential equations. The certificate satisfies Fintype.card(PDEType) = 5.
background
The module states that physical laws appear as PDEs on the recognition field, with five types matching configDim D = 5. These comprise the elliptic Laplace equation for J-cost potential at equilibrium, the parabolic heat equation for J-cost diffusion, the hyperbolic wave equation for J-cost propagation, and the mixed and integro-differential cases. The structure PartialDifferentialEquationsCert packages the claim as a single field requiring the cardinality of PDEType to equal five. The upstream theorem pdeTypeCount establishes this equality by direct decision procedure.
proof idea
The definition is a one-line wrapper that directly assigns the theorem pdeTypeCount to the five_types field of the PartialDifferentialEquationsCert structure.
why it matters
This definition completes the PDE classification step that links discrete recognition steps to continuum dynamics in the Recognition Science framework. It anchors the five equation types that govern J-cost behavior under the Recognition Composition Law. No downstream uses are recorded, leaving open its integration into explicit derivations of field equations from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.