gaussian_approx_at_eq
plain-language theorem explainer
The declaration establishes that the path weight equals exactly 1 at the equilibrium ratio r=1 for arbitrary ħ. Researchers deriving the classical limit or partition function from the J-cost action would cite this normalization at the action minimum. The proof is a direct one-line wrapper that unfolds the path_weight definition and substitutes the Jcost zero lemma.
Claim. For any real number $ħ$, the path weight at equilibrium satisfies $w(1, ħ) = 1$, where $w(r, ħ) := exp(-J(r)/ħ)$ and $J$ is the J-cost function obeying $J(1) = 0$.
background
The J-cost function satisfies J(1) = 0 with explicit form J(x) = (x-1)²/(2x). The path weight is defined as exp(-J(r)/ħ) and supplies the Boltzmann factor for each path ratio r in the construction. This module derives the path integral Z = ∫ exp(-J(γ)/ħ) Dγ from the J-action S[γ] = ∫ J(γ(t)) dt, with the measure concentrating near the classical path because J is convex and J''(1) = 1.
proof idea
The proof is a one-line wrapper that unfolds the definition of path_weight and rewrites using the lemma Jcost_unit0 together with the arithmetic facts that -0/ħ = 0 and exp(0) = 1.
why it matters
This supplies the weight_one_at_eq field inside the PathIntegralDeepCert structure that certifies positivity, maximum weight at equilibrium, and unit weight at r=1. It completes the normalization step required for the structural theorem that the path integral peaks at the J-cost minimum, supporting the classical limit ħ → 0 in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.