classical_path
plain-language theorem explainer
The theorem shows that the J-cost vanishes at the unit element, marking the classical stationary trajectory in the RS path integral. Physicists deriving QFT from Recognition Science cite it to isolate the minimum-weight contribution. The proof is a direct term application of the Jcost unit lemma.
Claim. The J-cost function satisfies $J(1)=0$, where $J(x)=(x-1)^2/(2x)$.
background
The PathIntegralFromRS module recasts the Feynman path integral as a sum over recognition paths weighted by J-cost, with the classical trajectory at the J-cost minimum. J-cost is defined by the formula $J(x)=(x-1)^2/(2x)$ from the Cost module. The local setting states that the dominant path carries weight exp(0)=1. This rests on the upstream Jcost_unit0 lemma, which states Jcost 1 = 0 by direct simplification of the J-cost definition.
proof idea
The proof is a one-line term wrapper that applies the Jcost_unit0 lemma from the Cost module.
why it matters
This supplies the classical component to the pathIntegralCert definition, which assembles the five path-integral formulations in RS. It realizes the module statement that the dominant path is the J-cost minimum. The result anchors the zero point of the J-function within the Recognition Composition Law and the T5 J-uniqueness step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.