pathIntegralDeepCert
plain-language theorem explainer
The definition constructs an explicit witness for the PathIntegralDeepCert structure, which encodes positivity of the path weight, its maximization at the equilibrium point r=1, and normalization to unity there. Researchers deriving the concentration of the Feynman path integral around classical trajectories from the J-cost action would cite this witness to invoke the three properties at once. The construction is a direct record literal that delegates each field to a prior theorem.
Claim. Let $w(r, ħ)$ denote the path weight function derived from the J-cost action. There exists a term of type PathIntegralDeepCert witnessing that $w(r, ħ) > 0$ for all real $r, ħ$, that $w(r, ħ) ≤ w(1, ħ)$ whenever $ħ > 0$, and that $w(1, ħ) = 1$ for every $ħ$.
background
The module establishes the path integral from the J-cost action $S[γ] = ∫ J(γ(t)) dt$, with the path weight defined by $w(r, ħ) = exp(-J(r)/ħ)$. The structure PathIntegralDeepCert packages the three analytic properties needed to conclude that the measure concentrates at the stationary point of the action. Upstream results supply the individual facts: path_weight_pos proves strict positivity via the exponential, path_weight_max_at_eq proves the maximum at r=1 by monotonicity of the exponential, and gaussian_approx_at_eq proves normalization at equilibrium from Jcost_unit0 and exp(0)=1.
proof idea
This is a definition that directly constructs the PathIntegralDeepCert record by assigning the path_weight_pos field to the theorem path_weight_pos, the path_weight_max field to path_weight_max_at_eq, and the weight_one_at_eq field to gaussian_approx_at_eq.
why it matters
The definition supplies the concrete inhabitant of PathIntegralDeepCert that is immediately used to prove pathIntegralDeepCert_inhabited, establishing nonemptiness of the certificate. It completes the master structural theorem of the module, which shows that the Feynman path integral measure follows from convexity of J and the calibration J''(1)=1, consistent with the Recognition Science forcing chain that fixes ħ = φ^{-5}. It touches the classical limit ħ → 0 without further scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.