A finite sum indexed by a function space, with no aggregate type

Identifier: F:int-sum-maps
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

`Int.sumMaps m n F` folds `Int.add` over `F g` for every map `g : [0,m) -> [0,n)`, by structural recursion on `m` with the HIGHER-ORDER motive `fun _ : Nat => ((Nat -> Nat) -> Int) -> Int`. It is the construction behind ADR-1310's finding that this kernel's missing `List`/`Finset`/`Prod` is an INVENTORY rather than a law, and more sharply that a finite sum does not need its index set to exist as a type -- it needs a FOLD over the index set, and a fold is a function. ADR-1135 had recorded the opposite ("the index set of the outer sum is a function space, not a `Nat` range, so `Rat.sumRange` cannot express it") and used it to close determinant multiplicativity. No new inductive, no `funext`; the same higher-order-motive device `Rat.det` already uses. The map extension `cons k g` is built INLINE as a `Nat.rec` so both its equations are `Eq.refl`, avoiding the `i < m` side condition a `Nat.beq` write would put on every step. WHAT NO TYPE CHECK CAN SEE: `Nat -> Nat -> ((Nat -> Nat) -> Int) -> Int` is this type whatever the function returns, so correctness rests entirely on the evaluation evidence. `Kernel::axiom_footprint` is EMPTY.

Formal statement

def Int.sumMaps : ((x0 : AxNat) -> ((x1 : AxNat) -> ((x2 : ((x2 : ((x2 : AxNat) -> AxNat)) -> Int)) -> Int)))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

kernel-Int.sumMaps

Kind: kernel-term
Status: checked

Supports: Int.sumMaps is admitted by the trusted kernel gate with the type recorded in formal.statement.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example theorem_dependency_inventory -- Int.sumMaps 2>/dev/null | grep -cE '^Int\.sumMaps[[:space:]]'

Evidence notes

Two independent failure modes, so the exit status depends on the finding rather than on the run completing: theorem_dependency_inventory exits non-zero when a NAMED filter matches nothing, and grep -c exits 1 printing 0 when the anchored line is absent. Anchored with [[:space:]], never \t -- in a scripted (GNU) grep \t is a literal t. grep -c rather than grep -q, which would SIGPIPE the producer under pipefail. --release is MANDATORY: this tool builds creal/complex/cpoint, which overflow the default debug thread stack. Pass ONE name per invocation: this tool silently keeps only the FIRST name argument.

footprint-Int.sumMaps

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the integer prelude's trusted surface is empty, which bounds Int.sumMaps.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example nat_axiom_inventory -- --require-axiom-free integer

Evidence notes

--require-axiom-free exits non-zero when the named prelude's trusted surface (Axiom + Opaque + Quotient) is not empty, and errors rather than silently passing for a prelude the run never built. A declaration cannot depend on a trusted declaration the environment does not contain, so an empty integer surface bounds every declaration in it. This is a whole-prelude bound, not a per-declaration measurement; the per-declaration figure is the footprint column of kernel_declaration_projection, measured 0 for this row.

evaluation-Int.sumMaps

Kind: instance-pin
Status: checked

Supports: Int.sumMaps enumerates every map [0,m) -> [0,n) exactly once, checked by reducing it to a normal form at concrete arguments -- which is the only thing that can see a wrong Definition, since the trusted gate checks only the stated type.

Checker command

cargo test -p axeyum-lean-kernel --lib int_prelude::sum_maps_tests 2>&1 | grep -cE '^test result: ok\. 5 passed'

Evidence notes

grep -c on a TESTED COUNT, so the exit status depends on the finding: a suite that compiled to zero tests prints '0 passed' and the count is 0. Five tests: cardinality at seven (m,n) pairs including both n = 0 cases; the full product [0,3)x[0,3) separated from its DIAGONAL in both directions (9 against 5); both defining equations with the base map pinned as the constant zero; prodRange_sumRange_expand at a concrete instance with both sides independently 9; and an environment-read axiom-footprint check. A transposed index is deliberately NOT tested and cannot be -- a sum over every map is invariant under permuting the indices when each draws from the same range, so any such test would be vacuous (recorded in the module doc).

Provenance

{
  "date": "2026-08-31",
  "curation": "curated",
  "established_by": "axeyum-lean-kernel build_int_prelude (crates/axeyum-lean-kernel/src/int_prelude/sum_maps.rs)",
  "source": "formal.statement and axiom_footprint are taken verbatim from `cargo run -q --release -p axeyum-lean-kernel --example kernel_declaration_projection`, whose TSV rows are (prelude, kind, display name, axiom-footprint size, direct type declarations, direct declarations, direct theorems, Kernel::render_lean(declaration.ty())). depends_on is the direct-theorem column intersected with this ledger's registered facts, supplied by scripts/check-fact-depends-derived.py --fix. Nothing about the statement was hand transcribed; title, statement and the evidence notes were authored (lane aggregates)."
}