path_weight_max_at_eq
plain-language theorem explainer
The theorem shows that the path weight exp(-J(r)/ℏ) attains its global maximum at the equilibrium point r = 1 for every positive ℏ. Researchers deriving the concentration of the path-integral measure around the classical trajectory in Recognition Science would cite it when justifying the classical limit. The proof is a short algebraic chain that unfolds the definition, invokes non-negativity of J-cost, and applies monotonicity of the exponential.
Claim. For any real number $ℏ > 0$, the path weight $w(r) := exp(-J(r)/ℏ)$ satisfies $w(r) ≤ w(1)$ for all real $r$.
background
The Path Integral from J-Cost Action module constructs the Feynman path integral from the J-action $S[γ] = ∫ J(γ(t)) dt$, where J is the convex cost function satisfying the Recognition Composition Law. The path weight is defined as $exp(-Jcost(r)/ℏ)$ with $Jcost(r) = (r + r^{-1})/2 - 1$, which equals zero at the fixed point r = 1. The module proves structural facts including positivity of the partition function and peaking at minimum action. This theorem depends on the upstream lemma that Jcost(x) ≥ 0 for x > 0, obtained by rewriting Jcost as $(x-1)^2/(2x)$ and applying non-negativity of squares and denominators.
proof idea
The term proof introduces an arbitrary real r, unfolds the path_weight definition, and reduces the target inequality via the monotonicity of the exponential (Real.exp_le_exp.mpr) and negation (neg_le_neg). The remaining comparison -Jcost(r)/ℏ ≤ -Jcost(1)/ℏ follows from Jcost(r) ≥ 0 (by the Jcost_nonneg lemma) together with Jcost(1) = 0 and division by the positive constant ℏ.
why it matters
The result supplies the maximality field of the master certificate PathIntegralDeepCert, which also records positivity and the Gaussian approximation near r = 1. It directly implements the module's claim that the path-integral measure concentrates at the stationary action because J is convex with calibrated Hessian. In the broader framework this step supports the classical limit ℏ → 0 and the eight-tick octave structure by ensuring fluctuations are suppressed by exp(-J/ℏ).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.