mechanics_equilibrium
plain-language theorem explainer
The theorem records that the J-cost function equals zero at argument 1, identifying the equilibrium point in the Recognition Science recasting of classical mechanics. Workers assembling the depth certificate for Hamiltonian mechanics from the J-functional would cite this fact. The proof is a direct one-line application of the unit lemma for Jcost.
Claim. $J(1) = 0$, where $J(x) = (x-1)^2/(2x)$ is the J-cost function.
background
The module recasts classical mechanics with five formulations (Newtonian through Hamilton-Jacobi) equal to configDim D = 5. The Hamiltonian is identified with the J-cost energy function, and the phase-space minimum occurs where this cost reaches zero at equilibrium. Three conservation laws (energy, momentum, angular momentum) are set equal to D = 3.
proof idea
The proof is a one-line wrapper that applies the Jcost_unit0 lemma from the Cost module. That lemma itself follows by direct simplification of the J-cost definition J(x) = (x-1)^2/(2x).
why it matters
This supplies the equilibrium field to the classicalMechanicsDepthCert definition, which bundles five formulations, three conservation laws, and the J = 0 fact to certify classical mechanics depth from RS. It completes the phase-space minimum step in the module's framework, where the Hamiltonian is the J-cost energy function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.