mechanicsFormulationCount
plain-language theorem explainer
The theorem asserts that the inductive type enumerating canonical formulations of classical mechanics has cardinality exactly five. A researcher deriving classical mechanics from the J-cost functional equation would cite this to fix the configuration dimension at five. The proof is a direct decision procedure that enumerates the five constructors of the type.
Claim. The set of canonical formulations of classical mechanics has cardinality five, consisting of the Newtonian, Lagrangian, Hamiltonian, Poisson-bracket, and Hamilton-Jacobi formulations.
background
The module Classical Mechanics Depth from RS identifies five formulations with the configuration dimension D = 5. The Hamiltonian case is identified with the J-cost energy function whose minimum is J = 0 at equilibrium. Three conservation laws are separately tied to D = 3 spatial dimensions. The sole upstream dependency is the inductive definition of the type MechanicsFormulation whose five constructors are newtonian, lagrangian, hamiltonian, poissonBracket, and hamiltonJacobi.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic computes Fintype.card by exhaustive enumeration of the five constructors of the inductive type MechanicsFormulation.
why it matters
The result populates the five_formulations field of the classicalMechanicsDepthCert definition that bundles formulation count, conservation-law count, and equilibrium condition. It supplies the concrete integer 5 required by the framework step that forces D = 3 and by the Recognition Composition Law that underlies all classical mechanics derivations. No open scaffolding remains in this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.