PDEType
plain-language theorem explainer
PDEType enumerates the five canonical PDE classes that Recognition Science uses to classify laws on the recognition field. A researcher formalizing the PDE side of RS would cite it when proving that configuration dimension equals five. The declaration is a direct inductive definition with five constructors and no proof obligations.
Claim. Let PDEType be the inductive type with constructors elliptic, parabolic, hyperbolic, mixed, and integroDifferential.
background
In Recognition Science physical laws appear as PDEs on the recognition field. The module states that the five types (elliptic, parabolic, hyperbolic, mixed, integro-differential) realize configDim D = 5. Elliptic equations correspond to J-cost potentials satisfying ΔJ = 0 at equilibrium; parabolic equations describe J-cost diffusion; hyperbolic equations describe J-cost propagation. The inductive type supplies the Lean encoding of this classification.
proof idea
This is an inductive definition that directly lists the five constructors; no tactics or lemmas are applied.
why it matters
PDEType is the type whose cardinality is asserted by the structure PartialDifferentialEquationsCert and proved equal to five by the theorem pdeTypeCount. It fills the claim that five PDE types equal configDim D = 5, anchoring the classification of physical laws as PDEs on the recognition field with the J-cost interpretations given in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.