Multiplication on the integers is commutative

Identifier: F:int-mul-comm
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For all integers a and b, a * b = b * a.

Formal statement

theorem Int.mul_comm : ((x0 : Int) -> ((x1 : Int) -> Eq.{1} Int (Int.mul x0 x1) (Int.mul x1 x0)))

Dependencies

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

1 direct dependencies 85 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-Int.mul_comm

Kind: kernel-term
Status: checked

Supports: For all integers a and b, a * b = b * a.

Checker command

cargo test -p axeyum-lean-kernel --lib int_prelude

Evidence notes

`build_int_prelude` admits this theorem through the trusted `Kernel::add_declaration` gate, which re-checks the proof term against the stated type, so a green run of the command is a machine-checked proof. Measured 2026-08-14: 12 tests pass (a nonzero count -- the filter is not inert).

footprint-Int.mul_comm

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- this theorem's trusted closure is empty

Checker command

test "$(cargo run -q -p axeyum-lean-kernel --example int_theorem_inventory -- mul_comm 2>/dev/null | grep -Ec '^theorem[[:space:]]+Int\.mul_comm[[:space:]]')" -ge 1

Evidence notes

Two independent bounds, because either alone would be weaker than it looks. (1) `Kernel::axiom_footprint` walks THIS declaration's transitive dependencies and prints an empty footprint column -- this is the kernel's `#print axioms`, and it is the check that matters, since an integer law IS still asserted (`Int.euclidean_decomposition`; it was 6 until lane int-remainder proved the `subNatNat` borrow, and the check mattered more then) and Int.mul_comm could have reached for one and still type-checked. (2) `nat_axiom_inventory` reports `nat: axiom=0 opaque=0 quotient=0` for the development ZZ is constructed over, so the foundation admits no trusted declaration at all. Counting `Declaration::Axiom` alone would not have sufficed: `Opaque` has no proof body and `Quotient` admits `Quot.sound`, which is exactly the declaration the quotient-of-NxN construction would have added -- the enumeration covers all three kinds and reports zero for each.

Provenance

{
  "date": "2026-08-14",
  "established_by": "axeyum-lean-kernel build_int_prelude, lane int-keystone",
  "source": "one of the 34 propositions build_int_prelude previously ASSERTED; this lane constructed ZZ over the proved Nat development and derived it"
}