PathIntegralDeepCert
plain-language theorem explainer
PathIntegralDeepCert packages three analytic properties of the path weight function w(r, ħ) = exp(-J(r)/ħ) derived from the J-cost action. Researchers deriving the Feynman path integral from Recognition Science's J-action cite this record to assert positivity, maximality at the classical path r=1, and unit normalization at equilibrium. The declaration is a pure structure definition that bundles existing lemmas without additional computation.
Claim. A record type certifying three properties of the weight function $w(r, ħ) = e^{-J(r)/ħ}$: (i) positivity $∀ r, ħ ∈ ℝ, 0 < w(r, ħ)$; (ii) maximality $∀ ħ > 0, ∀ r, w(r, ħ) ≤ w(1, ħ)$; (iii) normalization $∀ ħ, w(1, ħ) = 1$.
background
The module derives the path integral from the J-cost action $S[γ] = ∫ J(γ(t)) dt$, with the path weight defined as $w(r, ħ) = exp(-J(r)/ħ)$. Here ħ denotes the reduced Planck constant in RS-native units, ħ = φ^{-5}. The J-cost function J is the convex cost from the Recognition Composition Law, with minimum J(1) = 0 at the self-similar fixed point.
proof idea
Structure definition that directly references the path_weight function and its positivity theorem (proved via Real.exp_pos). The maximality and normalization fields are supplied by sibling results path_weight_max_at_eq and gaussian_approx_at_eq in the same module.
why it matters
This record is the master certificate for the structural theorem that the path integral concentrates on the classical path. It is instantiated by pathIntegralDeepCert and shown inhabited by pathIntegralDeepCert_inhabited. The construction supports the classical limit ħ → 0 and the emergence of the Born rule from path weights, consistent with the eight-tick octave and D = 3 framework landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.