pdeTypeCount
plain-language theorem explainer
The declaration asserts that the inductive type of canonical PDE classes has exactly five elements. A researcher classifying equation forms arising from the J-cost functional on the recognition field would cite this cardinality when enumerating physical law types. The proof is a single decision tactic that computes the finite cardinality directly from the five constructors.
Claim. The set of partial differential equation types has cardinality 5, where the types comprise elliptic, parabolic, hyperbolic, mixed, and integro-differential.
background
In the Recognition Science setting, physical laws appear as partial differential equations on the recognition field. The module enumerates five canonical classes: elliptic for the Laplace equation with vanishing J-cost potential, parabolic for J-cost diffusion, hyperbolic for J-cost wave propagation, together with mixed and integro-differential forms. These classes are formalized as the inductive type PDEType whose five constructors derive DecidableEq, Repr, BEq, and Fintype instances, and the count is identified with the configuration dimension D = 5.
proof idea
The proof applies the decide tactic, which automatically enumerates the five constructors of the inductive type PDEType and confirms that its Fintype cardinality equals 5.
why it matters
The result supplies the five_types field of the partialDifferentialEquationsCert definition, which certifies the PDE enumeration inside the mathematics module. It directly implements the module statement that five canonical PDE types equal configDim D = 5 and thereby closes the classification step for equations generated by the J-cost functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.