Integrand congruence holds in every integration space, from monotonicity alone

Identifier: F:intspace-integral-congr
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

In any integration space S -- a carrier of functions with a preorder `fle`, a linear structure, a set-indexed integrability family `Integrable`, and an integral that is monotone, additive, homogeneous and evaluates constants -- two integrable functions that bound each other pointwise have `CReal.Equiv` integrals. The proof consumes only monotonicity (`integralLe`) and antisymmetry of the real order (`CReal.equiv_of_le_le`); it uses no property of the space beyond the record's fields, so it holds equally of the Riemann integral on an interval, of a finite sum, and of evaluation at a point. Two consequences follow immediately and are separately declared: integral WITNESS INDEPENDENCE (the value does not depend on which integrability datum is supplied, taking f = g and `fleRefl` twice), and, at the interval instance, a statement about `CReal.integral` that the real prelude did not have -- it carried `CReal.integral_le` for eight days with no way to turn a two-sided pointwise bound into an equality of integrals.

Formal statement

theorem IntSpace.integral_congr : ((x0 : IntSpace) -> ((x1 : IntSpace.carrier x0) -> ((x2 : IntSpace.carrier x0) -> ((x3 : IntSpace.Integrable x0 x1) -> ((x4 : IntSpace.Integrable x0 x2) -> ((x5 : IntSpace.fle x0 x1 x2) -> ((x6 : IntSpace.fle x0 x2 x1) -> CReal.Equiv (IntSpace.integral x0 x1 x3) (IntSpace.integral x0 x2 x4))))))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 3 direct dependents

Evidence

kernel-IntSpace.integral_congr

Kind: kernel-term
Status: checked

Supports: The generic congruence is admitted by Kernel::add_declaration with an empty axiom footprint, along with the other 69 IntSpace declarations.

Checker command

out=$(cargo test -q --release -p axeyum-lean-kernel --lib intspace::intspace_tests::every_intspace_declaration_is_axiom_free 2>&1) && test "$(printf '%s\n' "$out" | grep -c '1 passed')" -ge 1

Evidence notes

The test derives its declaration list from the IntSpacePrelude handle and the record's own RecordNames, not from a literal list of names, so a declaration cannot be added without entering the footprint sweep. It also pins the total at 54 + FIELD_COUNT, so a silent drop is a failure rather than a smaller sweep.

intspace-congr-instantiates-on-creal

Kind: kernel-term
Status: checked

Supports: The generic theorem produces a statement about CReal.integral alone -- no IntSpace in the type -- when applied to IntSpace.crealInterval, which is what makes the genericity claim a fact about the real prelude and not only about the record.

Checker command

out=$(cargo test -q --release -p axeyum-lean-kernel --lib intspace::intspace_tests::intspace_headline_types_render 2>&1) && test "$(printf '%s\n' "$out" | grep -c '1 passed')" -ge 1

Evidence notes

The test asserts the rendered type of the re-derived statement CONTAINS CReal.integral and does NOT contain IntSpace; a statement that leaked the record into its own conclusion would fail.

intspace-congr-is-not-vacuous-two-instances

Kind: kernel-term
Status: checked

Supports: The theorem is not vacuously generic: the SAME generic congruence is instantiated at a second, structurally unrelated integration space (CReal.sumRange over a finite index set) and yields a statement about CReal.sumRange with no IntSpace in it. A record with one instance proves nothing about genericity.

Checker command

out=$(cargo test -q --release -p axeyum-lean-kernel --lib intspace::intspace_tests::intspace_headline_types_render 2>&1) && test "$(printf '%s\n' "$out" | grep -c '1 passed')" -ge 1

Evidence notes

The two instances share no machinery -- one is built from Riemann sums with a modulus of continuity, the other from Nat.rec -- so the congruence holding at both is evidence about the record rather than about the interval integral.

intspace-fields-are-load-bearing

Kind: exhaustive-enumeration
Status: checked

Supports: Six one-slot mutations of IntSpace.crealInterval's constructor arguments are each REFUSED by the trusted gate, with the unmutated instance admitted as a positive twin in the same test. Without the twin, a refusal would be indistinguishable from a broken harness.

Checker command

out=$(cargo test -q --release -p axeyum-lean-kernel --lib intspace::intspace_tests::every_swapped_interval_field_is_refused 2>&1) && test "$(printf '%s\n' "$out" | grep -c '1 passed')" -ge 1

Evidence notes

A record field mutation poisons the shared prelude build, so it cannot be shown to kill exactly one test the usual way; the positive twin in the same test is the substitute criterion. Each swap replaces one field with another field of the record, so the term is well formed and the refusal is about the field's ROLE, not about garbage.

Provenance

{
  "date": "2026-09-04",
  "established_by": "axeyum-lean-kernel intspace::generic module (integration-space lane, roadmap W3-1)",
  "source": "Derived from the IntSpace record's integralLe field plus CReal.equiv_of_le_le. See docs/research/09-decisions/adr-1612-the-integral-is-primitive-and-measure-is-derived-predicatively.md for the design and the measurement."
}