classical_path
plain-language theorem explainer
The theorem establishes that the J-cost vanishes on the unit path, which is the classical stationary trajectory in the RS path integral. A physicist working on RS-derived QFT would cite this to anchor the classical limit with weight 1. The proof is a direct term application of the upstream Jcost unit lemma.
Claim. The cost function on recognition paths satisfies $J(1) = 0$, where $J(x) = (x-1)^2/(2x)$.
background
In the Path Integral from RS module the Feynman path integral is recast as a sum over recognition paths weighted by exp(-J[φ]) in Euclidean signature, with the classical trajectory at the J-cost minimum. The J-cost is the squared-ratio function J(x) = (x-1)^2/(2x) that vanishes at the unit path. The local setting is the Euclidean path integral in RS where the dominant path carries weight exp(0) = 1, and five canonical formulations correspond to configDim D = 5.
proof idea
One-line wrapper that applies the Jcost_unit0 lemma from the Cost module (and its JcostCore sibling), which states Jcost 1 = 0 by simp [Jcost].
why it matters
This supplies the classical component to the pathIntegralCert definition, which bundles five_formulations, classical, and quantum. It realizes the Euler-Lagrange stationary point as the J=0 minimum inside the RS path-integral formulation, consistent with the module statement that the dominant path is the J-cost minimum. It touches the classical-to-quantum transition within the five-formulation structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.