classical_path
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the explicit path-integral measure.
- Does not evaluate J-cost on non-unit paths.
- Does not address the quantum fluctuation term beyond naming it.
formal statement (Lean)
30theorem classical_path : Jcost 1 = 0 := Jcost_unit0
proof body
Term-mode proof.
31
32/-- Quantum fluctuations: J > 0 (off-classical paths). -/