piecewise_path_integral_additive_integrable
plain-language theorem explainer
The result establishes additivity of the interval integral for a real function over adjacent segments from a to b and b to c, provided separate integrability holds on each piece. Cost analysts formalizing path decompositions in the Recognition Science framework cite it to split J-cost integrals along composite trajectories. The proof is a one-line wrapper applying the symmetric form of Mathlib's adjacent-intervals addition lemma.
Claim. Let $f : ℝ → ℝ$ and $a, b, c ∈ ℝ$. If $f$ is Lebesgue integrable over the interval from $a$ to $b$ and from $b$ to $c$, then the integral from $a$ to $c$ equals the sum of the integrals from $a$ to $b$ and from $b$ to $c$.
background
This theorem resides in the ClassicalResults module, which collects standard facts from real analysis for the cost domain. The module presents such results as established infrastructure justified by textbook references including Rudin and Apostol, rather than deriving them from Recognition Science primitives. The local setting supplies reliable tools for later formalization of path integrals and defect measures without rebuilding basic analysis inside Lean.
proof idea
The proof is a one-line wrapper that invokes the adjacent intervals addition lemma from the interval integral library and applies symmetry to obtain the stated orientation.
why it matters
It licenses decomposition of integrals along piecewise paths, a prerequisite for computing total cost over trajectories with direction changes in the Recognition framework. No immediate parent theorems appear in the used-by graph, yet the result aligns with the classical results needed to embed the Recognition Composition Law and phi-ladder constructions. The module context stresses that these facts are not physical assumptions but standard mathematical tools, here supplied in provable rather than axiomatic form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.