quantum_fluctuation
plain-language theorem explainer
The theorem establishes that J-cost is strictly positive for any positive real r different from 1. Physicists formalizing path integrals in Recognition Science cite it to confirm that non-classical paths carry positive cost and receive exponentially suppressed weights. The proof is a direct one-line application of the J-cost positivity lemma from the Cost module.
Claim. For any real number $r > 0$ with $r ≠ 1$, the J-cost satisfies $0 < J(r)$.
background
The Path Integral from RS module reinterprets the Feynman path integral as a sum over recognition paths weighted by J-cost, with the classical trajectory as the unique minimum where J equals zero. J-cost is the function that quantifies deviation from this minimum; upstream lemmas establish its positivity precisely when the ratio differs from one. The module imports the Cost module, where Jcost_pos_of_ne_one is proved by rewriting Jcost as a square divided by a positive term.
proof idea
This is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one from IndisputableMonolith.Cost.
why it matters
The result is used directly in the pathIntegralCert definition to bundle quantum fluctuations with classical paths and the count of five formulations. It fills the quantum component of the RS path-integral certification, consistent with the framework's view that quantum effects arise from positive J-cost deviations off the classical trajectory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.