VariationalProblem
plain-language theorem explainer
The declaration introduces an inductive type that enumerates the five canonical variational problems arising from the recognition functional in Recognition Science. A researcher working on extremal principles would cite it when counting the distinct problems that exhaust the configuration dimension. The definition is a direct inductive enumeration whose finiteness and decidability follow automatically from the five listed constructors.
Claim. The inductive type enumerating the five canonical variational problems: the brachistochrone problem, the geodesic problem, the minimal-surface problem, Fermat's principle, and the minimization of the J-cost functional.
background
The module develops the calculus of variations from the recognition functional, identified with the J-cost integral. The Euler-Lagrange equation for this functional reads partial J over partial r minus the total derivative of partial J over partial r-prime equals zero. Equilibrium holds when the ratio r equals one, at which point the J-cost vanishes. The five problems listed here are stated to realize configuration dimension equal to five.
proof idea
The declaration is a bare inductive definition with five constructors. Decidable equality, representation, boolean equality, and finiteness are obtained automatically by the deriving clause. No lemmas or tactics are applied beyond the inductive structure itself.
why it matters
It supplies the finite enumeration required by the theorem that asserts exactly five variational problems and by the VariationsCert structure that records the J-cost minimum at unity together with positivity off the minimum. This realizes the configDim D equals five claim in the Recognition Science setting and feeds directly into the certificate that J equals zero at r equals one.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.