path_weight_max_at_eq
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.
claimFor 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 in Recognition Science
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/ℏ).
scope and limits
- Does not construct or prove existence of the full path-integral measure.
- Does not treat the oscillatory phase factor exp(iS/ℏ) of the complex Feynman integral.
- Does not extend the maximality statement to multi-dimensional or field-theoretic paths.
- Does not quantify the rate of decay away from r = 1.
Lean usage
path_weight_max_at_eq hbar hformal statement (Lean)
43theorem path_weight_max_at_eq (hbar : ℝ) (h : 0 < hbar) :
44 ∀ r : ℝ, path_weight r hbar ≤ path_weight 1 hbar := by
proof body
Term-mode proof.
45 intro r
46 unfold path_weight
47 apply Real.exp_le_exp.mpr
48 apply neg_le_neg
49 apply div_le_div_of_nonneg_right _ h
50 exact Jcost_nonneg (by positivity)
51
52/-- Gaussian approximation near r = 1: weight ≈ 1 - ε²/(2ℏ). -/