PathIntegralDeepCert
PathIntegralDeepCert packages three properties of the path weight w(r, ħ) = exp(-J(r)/ħ) derived from the J-cost action: strict positivity for all real inputs, maximization at the classical point r=1 when ħ>0, and unit value at that point. Researchers deriving the Feynman path integral from Recognition Science J-action convexity would cite the certificate to anchor measure concentration near stationary paths. The structure is populated by a direct constructor that invokes path_weight_pos, path_weight_max_at_eq, and gaussian_approx_at_eq.
claimThe structure asserts that the path weight function $w(r, ħ) = exp(-J(r)/ħ)$ satisfies $w(r, ħ) > 0$ for all real $r, ħ$, $w(r, ħ) ≤ w(1, ħ)$ whenever $ħ > 0$, and $w(1, ħ) = 1$ for all real $ħ$.
background
The module derives the path integral $Z = ∫ exp(iS/ℏ) Dγ$ from the J-cost action $S[γ] = ∫ J(γ(t)) dt$, where J is the convex function from the forcing chain with J(1) = 0 and J''(1) = 1. The path weight is defined as path_weight r hbar := Real.exp (-(Jcost r) / hbar). Upstream theorem path_weight_pos states 0 < path_weight r hbar by Real.exp_pos, while path_weight_max_at_eq and gaussian_approx_at_eq establish the peak and normalization.
proof idea
The declaration is the structure definition. Downstream pathIntegralDeepCert constructs an instance by direct field assignment: path_weight_pos from the eponymous lemma, path_weight_max from path_weight_max_at_eq, and weight_one_at_eq from gaussian_approx_at_eq. No tactics intervene beyond the structure constructor.
why it matters in Recognition Science
The certificate records the three properties required for the module's structural theorem on path-integral positivity and classical-limit concentration. It is consumed by pathIntegralDeepCert_inhabited to witness Nonempty PathIntegralDeepCert and supports the listed results on partition_function_positive and path_integral_peaks_at_action_min. In the Recognition framework it anchors the emergence of Born-rule probabilities from path weights under the J-convexity and ħ = φ^{-5} calibration.
scope and limits
- Does not prove convergence of the infinite-dimensional path measure.
- Does not incorporate the oscillatory phase factor exp(iS/ħ).
- Does not derive the explicit form of J from T5-T8.
- Does not treat multi-particle or entangled path ensembles.
formal statement (Lean)
56structure PathIntegralDeepCert where
57 path_weight_pos : ∀ r hbar : ℝ, 0 < path_weight r hbar
58 path_weight_max : ∀ hbar : ℝ, 0 < hbar → ∀ r : ℝ, path_weight r hbar ≤ path_weight 1 hbar
59 weight_one_at_eq : ∀ hbar : ℝ, path_weight 1 hbar = 1
60