Right fold distributes over append

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

Recorded description

Folding a binary operation from the right over the concatenation of two lists l1 and l2 equals folding first over l2 (to get the seed for the second fold) and then over l1.

Formal statement

theorem List.foldr_append : ((x0 : Sort (1)) -> ((x1 : Sort (1)) -> ((x2 : ((x2 : x0) -> ((x3 : x1) -> x1))) -> ((x3 : x1) -> ((x4 : List.{0} x0) -> ((x5 : List.{0} x0) -> Eq.{1} x1 (List.foldr x0 x1 x2 x3 (List.append x0 x4 x5)) (List.foldr x0 x1 x2 (List.foldr x0 x1 x2 x3 x5) x4)))))))

Dependencies

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

0 direct dependencies 1 direct dependents

Evidence

kernel-list-foldr-append

Kind: kernel-term
Status: checked

Supports: List.foldr_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.foldr_append 2>/dev/null | grep -Fc '((x0 : Sort (1)) -> ((x1 : Sort (1)) -> ((x2 : ((x2 : x0) -> ((x3 : x1) -> x1))) -> ((x3 : x1) -> ((x4 : List.{0} x0) -> ((x5 : List.{0} x0) -> Eq.{1} x1 (List.foldr x0 x1 x2 x3 (List.append x0 x4 x5)) (List.foldr x0 x1 x2 (List.foldr x0 x1 x2 x3 x5) x4)))))))')" -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-foldr-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::list_prelude_tests::the_list_prelude_declares_no_axioms --test-threads=1

Evidence notes

list_prelude::list_prelude_tests::the_list_prelude_declares_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-foldr-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_prelude",
  "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)."
}