pathIntegralDeepCert_inhabited
plain-language theorem explainer
The declaration asserts that the PathIntegralDeepCert structure is inhabited. Researchers formalizing the J-cost derivation of the Feynman path integral cite it to confirm existence of a certificate enforcing positivity of the path weight, its maximum at the equilibrium point r=1, and normalization there. The proof is a one-line term that directly supplies the explicit construction pathIntegralDeepCert.
Claim. There exists a certificate $C$ such that the path weight $w(r, hbar)$ satisfies $w(r, hbar) > 0$ for all real $r, hbar$, $w(r, hbar) ≤ w(1, hbar)$ whenever $hbar > 0$, and $w(1, hbar) = 1$.
background
The module derives the path integral $Z = ∫ exp(iS/ℏ) Dγ$ from the J-cost action $S[γ] = ∫ J(γ(t)) dt$, with the measure concentrated near the classical path because J is convex and $J''(1) = 1$. PathIntegralDeepCert is the structure whose three fields encode the required properties of the path weight: positivity for all $r, hbar$, maximality at $r=1$ for $hbar > 0$, and exact normalization $w(1, hbar) = 1$. The upstream definition pathIntegralDeepCert assembles these fields from the lemmas path_weight_pos, path_weight_max_at_eq and gaussian_approx_at_eq.
proof idea
The proof is a one-line term wrapper that applies the definition pathIntegralDeepCert to inhabit the structure.
why it matters
It closes the existence claim for the master certificate PathIntegralDeepCert inside the structural theorem of the J-cost path integral. The module doc states that this certificate underpins the four listed results (partition_function_positive through classical_limit) and the concentration of the measure near the stationary action. No downstream uses are recorded, so the declaration functions as a terminal existence statement within the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.