Encyclopedia Cost Cost Classical Results Piecewise Path Integral Additive Integrable

ARTICLE 2 claims 2 theorems

Cost Classical Results Piecewise Path Integral Additive Integrable

A theorem about integrals that lets you split a path into pieces and add the results, a standard tool in calculus.

Verify this page

The Additivity Rule

In calculus, the integral of a function over an interval can be broken into parts. If you integrate from a to c, and b lies between them, the integral from a to c equals the integral from a to b plus the integral from b to c. This is the additivity rule for definite integrals. The declaration piecewise_path_integral_additive_integrable formalizes this rule in the framework's machine-checked library of formal theorems.

The theorem states that for a real-valued function f and real numbers a, b, and c, if f is integrable on the intervals from a to b and from b to c, then the integral from a to c is the sum of the two integrals. The condition of integrability is essential: it ensures the integrals exist and the rule applies. The rule holds for any real numbers a, b, and c, not just those in increasing order, as long as the integrability conditions are met.

This result is a standard fact in real analysis, found in textbooks such as Apostol's Mathematical Analysis. It is used routinely in mathematical physics and other fields without being re-proved each time. The framework's library declares it as an axiom pending full formalization, meaning it is a well-established mathematical fact that the framework relies on, but has not yet been proved from first principles within the library itself.

In Recognition Science, this additivity rule is a piece of the mathematical infrastructure. The framework models recognition as a discrete record of events with a forced cost, and the cost function J(x) = (x + 1/x)/2 - 1 is derived from five plain conditions. The additivity rule for integrals is a separate, classical result that the framework uses as a tool, not a new physical assumption. It is a theorem about real functions, not about recognition events themselves.

The declaration does not claim that the additivity rule is unique to Recognition Science, nor that it is a new discovery. It does not claim that the rule applies to all functions without integrability conditions. It also does not claim that the rule is derived from the framework's axioms; it is declared as a classical result pending formalization. The rule is a standard property of integrals, and the framework's library acknowledges it as such.

THEOREM piecewise_path_integral_additive_integrable · IndisputableMonolith/Cost/ClassicalResults.lean
piecewise_path_integral_additive_integrable · IndisputableMonolith/Cost/ClassicalResults.lean:55 
/-- Provable version with integrability hypotheses -/
theorem piecewise_path_integral_additive_integrable (f : ℝ → ℝ) (a b c : ℝ)
    (hab : IntervalIntegrable f MeasureTheory.volume a b)
    (hbc : IntervalIntegrable f MeasureTheory.volume b c) :
    ∫ x in a..c, f x = (∫ x in a..b, f x) + (∫ x in b..c, f x) :=
  (intervalIntegral.integral_add_adjacent_intervals hab hbc).symm
THEOREM piecewise_path_integral_additive_integrable · IndisputableMonolith/Cost/ClassicalResults.lean
piecewise_path_integral_additive_integrable · IndisputableMonolith/Cost/ClassicalResults.lean:55 
/-- Provable version with integrability hypotheses -/
theorem piecewise_path_integral_additive_integrable (f : ℝ → ℝ) (a b c : ℝ)
    (hab : IntervalIntegrable f MeasureTheory.volume a b)
    (hbc : IntervalIntegrable f MeasureTheory.volume b c) :
    ∫ x in a..c, f x = (∫ x in a..b, f x) + (∫ x in b..c, f x) :=
  (intervalIntegral.integral_add_adjacent_intervals hab hbc).symm

What this page does not claim

The declaration does not claim that the additivity rule is unique to Recognition Science. It does not claim that the rule applies to all functions without integrability conditions. It does not claim that the rule is derived from the framework's axioms; it is declared as a classical result pending formalization.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cost/ClassicalResults.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND