variationalProblemCount
plain-language theorem explainer
The theorem establishes that the inductive enumeration of variational problems in the Recognition Science calculus of variations has exactly five elements. A researcher deriving extrema of the J-cost functional would cite this to fix the configuration dimension at five. The proof is a direct one-line application of the decide tactic to the automatically generated Fintype instance.
Claim. The set consisting of the brachistochrone problem, the geodesic problem, the minimal-surface problem, Fermat's principle, and J-cost minimization has cardinality five: $5$.
background
The module identifies the recognition functional with the integral of J-cost and recalls that the Euler-Lagrange equation for J yields equilibrium at r = 1 with J = 0. The upstream cost definitions supply the concrete J-cost: one as the derived cost of a multiplicative recognizer's comparator on positive ratios, the other as the non-negative cost of any recognition event. The local inductive type VariationalProblem enumerates precisely the five canonical problems (brachistochrone, geodesic, minimalSurface, fermat, jCostMin) and carries an automatic Fintype instance.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype.card computation on VariationalProblem.
why it matters
This result supplies the five_problems field of the VariationsCert definition, which also records the J minimum at r = 1 and positivity off the minimum. It directly implements the module claim that five problems equal configDim D = 5 and anchors the variational layer of the Recognition Science forcing chain. No open scaffolding remains for this cardinality statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.