PathIntegralDeepCert
plain-language theorem explainer
PathIntegralDeepCert bundles three properties of the path weight w(r, ħ) = exp(−J(r)/ħ): positivity for all real inputs, maximality at r = 1 when ħ > 0, and normalization to 1 at r = 1. Researchers deriving the Feynman path integral from the J-cost action cite this certificate to guarantee measure concentration at the classical path. The declaration is a structure definition whose fields are later filled by upstream positivity and maximality lemmas.
Claim. Let $w(r, ħ) = exp(−J(r)/ħ)$. The certificate asserts: (i) $w(r, ħ) > 0$ for all real $r, ħ$; (ii) if $ħ > 0$ then $w(r, ħ) ≤ w(1, ħ)$ for all real $r$; (iii) $w(1, ħ) = 1$ for all real $ħ$.
background
The module derives the path integral from the J-cost action $S[γ] = ∫ J(γ(t)) dt$, with weight $w(r, ħ) = exp(−J(r)/ħ)$ where J is the Recognition Science cost function. The constant ħ is taken from Constants.hbar as φ^{-5} in native units. MODULE_DOC states the partition function is positive, peaks at minimum action J(1) = 0, and admits Gaussian approximation near equilibrium.
proof idea
This is a structure definition with no proof body. Its three fields receive their values downstream in the definition pathIntegralDeepCert, which assigns the upstream results path_weight_pos, path_weight_max_at_eq, and gaussian_approx_at_eq directly to the respective slots.
why it matters
PathIntegralDeepCert is the master certificate for the path-integral construction. It is instantiated by pathIntegralDeepCert and shown nonempty by pathIntegralDeepCert_inhabited. The certificate supports the module's claim that the measure concentrates at the classical path, linking to J-convexity and the forcing chain (T5–T8) through the calibrated Hessian J''(1) = 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.