PartialDifferentialEquationsCert
plain-language theorem explainer
Recognition Science expresses physical laws as partial differential equations on the recognition field, and this structure certifies that exactly five canonical types exist. A researcher classifying continuum limits from the J-cost functional would cite the count to confirm agreement with configuration dimension five. The structure is realized by a direct definition that records the cardinality of the five-constructor enumeration of equation classes.
Claim. Let PDEType be the finite set whose elements are the elliptic, parabolic, hyperbolic, mixed, and integro-differential classes. Then the cardinality of PDEType equals 5.
background
The module derives partial differential equations from Recognition Science by treating physical laws as equations on the recognition field. The J-cost potential produces the Laplace equation at equilibrium (elliptic), diffusion produces the heat equation (parabolic), and propagation produces the wave equation (hyperbolic); mixed and integro-differential forms complete the list. This matches the configuration dimension D = 5 stated in the module header.
proof idea
The declaration is a structure definition. Its single field is filled by the cardinality of the inductive type whose five constructors are the listed PDE classes.
why it matters
The structure supplies the type count required by the certification definition in the same module. It supports the framework claim that laws appear in one of five PDE forms, consistent with the forcing chain that fixes D = 3 spatial dimensions and the eight-tick octave. No open questions are resolved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.