Summing an appended list Nat is the sum of the two sums

Identifier: F:list-sum-append
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For lists of naturals, the sum of the elements of the concatenation of l1 and l2 equals the sum of the elements of l1 plus the sum of the elements of l2.

Formal statement

theorem List.sum_append : ((x0 : List.{0} AxNat) -> ((x1 : List.{0} AxNat) -> Eq.{1} AxNat (List.sum (List.append AxNat x0 x1)) (AxNat.add (List.sum x0) (List.sum x1))))

Dependencies

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

2 direct dependencies 0 direct dependents

Evidence

kernel-list-sum-append

Kind: kernel-term
Status: checked

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

Checker command

test "$(cargo run -q --release -p axeyum-lean-kernel --example list_theorem_inventory -- List.sum_append 2>/dev/null | grep -Fc '((x0 : List.{0} AxNat) -> ((x1 : List.{0} AxNat) -> Eq.{1} AxNat (List.sum (List.append AxNat x0 x1)) (AxNat.add (List.sum x0) (List.sum x1))))')" -ge 1

Evidence notes

The pattern is the FULL admitted type (rendered by Kernel::render_lean via list_theorem_inventory), not the theorem's name -- a drifted statement would fail this check. build_list_nat_bridge admits this theorem only through the trusted kernel gate, so a successful build IS the type-check.

footprint-list-sum-append

Kind: instance-pin
Status: checked

Supports: axiom_footprint: [] -- read from Kernel::axiom_footprint for this declaration, not from a maintained list

Checker command

cargo test -q --release -p axeyum-lean-kernel --lib -- list_prelude::bridge::bridge_tests::the_bridge_theorems_declare_no_axioms --test-threads=1

Evidence notes

list_prelude::bridge::bridge_tests::the_bridge_theorems_declare_no_axioms asserts Kernel::axiom_footprint(name).is_empty() for this declaration (among others in the same coverage sweep), read directly from the kernel rather than asserted from a list.

evaluation-list-sum-append

Kind: instance-pin
Status: checked

Supports: The List operations this statement is about COMPUTE the intended values, with negative controls -- the kernel cannot tell a Definition is wrong.

Checker command

cargo test -q --release -p axeyum-lean-kernel --lib -- list_prelude:: --test-threads=4

Evidence notes

list_prelude_tests.rs and bridge_tests.rs reduce List.length/append/map/foldr/reverse/sum/toMultiset/count to a concrete numeral or nil/cons skeleton at tiny discriminating arguments and pair every positive with the specific wrong formula its negative control rules out.

Provenance

{
  "date": "2026-09-03",
  "established_by": "axeyum-lean-kernel build_list_nat_bridge",
  "source": "theorem name and canonical type read directly via list_theorem_inventory, which prints render_lean of the admitted type; declared by list_prelude.rs/theorems.rs/bridge.rs (lane list-carrier-1, ADR-1579)."
}