The generalized distributive law: a product of sums expands into a sum over the function space

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

Recorded description

`prodRange (fun i => sumRange (c i) n) m = sumMaps m n (fun g => prodRange (fun i => c i (g i)) m)` at symbolic `m`, `n` and `c` -- a product of `m` sums of `n` terms each expands into a sum over all `n^m` functions `[0,m) -> [0,n)`. This is EXACTLY the expansion step of the Cauchy-Binet / multilinearity proof of `det (A*B) = det A * det B`, and it is the step ADR-1135 recorded as not expressible in this kernel: "the index set of the outer sum is a function space, not a `Nat` range, so `Rat.sumRange` cannot express it". Proved by an ordinary induction on `m` with the motive quantified over `c`, because the successor step applies the induction hypothesis at `fun i => c (succ i)` -- a DIFFERENT coefficient family. That is the same shape `Int.prodRange_permute` needs for its sigma and `Rat.det_congr` for its matrices. Both ends of the step peel their FIRST factor with `Int.prodRange_shiftFront`, which is what makes the inline `cons`'s two `Eq.refl` equations line up with no side conditions. No new inductive type, no `List`, no `Finset`, no `Prod`, no `funext`. `Kernel::axiom_footprint` is EMPTY. Admitted by the trusted gate on the first attempt.

Formal statement

theorem Int.prodRange_sumRange_expand : ((x0 : AxNat) -> ((x1 : AxNat) -> ((x2 : ((x2 : AxNat) -> ((x3 : AxNat) -> Int))) -> Eq.{1} Int (Int.prodRange (fun (x3 : AxNat) => Int.sumRange (x2 x3) x0) x1) (Int.sumMaps x1 x0 (fun (x3 : ((x3 : AxNat) -> AxNat)) => Int.prodRange (fun (x4 : AxNat) => x2 x4 (x3 x4)) x1)))))

Dependencies

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

2 direct dependencies 0 direct dependents

Evidence

kernel-Int.prodRange_sumRange_expand

Kind: kernel-term
Status: checked

Supports: Int.prodRange_sumRange_expand 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.prodRange_sumRange_expand 2>/dev/null | grep -cE '^Int\.prodRange_sumRange_expand[[: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.prodRange_sumRange_expand

Kind: exhaustive-enumeration
Status: checked

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

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.

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)."
}