MechanicsFormulation
plain-language theorem explainer
An inductive enumeration defines the five canonical formulations of classical mechanics as Newtonian, Lagrangian, Hamiltonian, Poisson bracket, and Hamilton-Jacobi. This supplies the finite set whose cardinality equals five, matching the configuration dimension in Recognition Science. Researchers tracing classical mechanics to the J-cost functional would cite the enumeration to ground the count before certifying equilibrium at J equal to zero. The definition is a bare inductive construction with automatic derivation of finite type structure.
Claim. Let $F$ be the set of classical mechanics formulations, defined as the inductive collection $F = $ {Newtonian, Lagrangian, Hamiltonian, Poisson bracket, Hamilton-Jacobi}, equipped with decidable equality and finite cardinality five.
background
The module identifies five canonical formulations of classical mechanics with configuration dimension D equal to five. In Recognition Science the Hamiltonian formulation is identified with the J-cost energy function, where phase-space equilibrium occurs at J equal to zero. Three conservation laws (energy, momentum, angular momentum) are set equal to the three spatial dimensions. The definition supplies the enumeration that downstream structures use to certify the match between formulation count and D.
proof idea
The declaration is a direct inductive definition listing the five variants, with instances for DecidableEq, Repr, BEq, and Fintype derived automatically by Lean.
why it matters
This definition is consumed by the ClassicalMechanicsDepthCert structure, which asserts five_formulations cardinality equals five together with three conservation laws and J-cost equilibrium at zero, and by the mechanicsFormulationCount theorem. It fills the step that links the five formulations to the J-cost function inside the Recognition Science forcing chain, consistent with T5 J-uniqueness and T8 D equal to three for the conservation laws. It supports the claim that classical mechanics depth arises directly from the Recognition Composition Law and the phi fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.