Polynomial multiplication over an abstract Setoid-flavored commutative ring is commutative

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

Recorded description

For any AlgS.CommRing record R and any two coefficient functions p, q : Nat -> R.carrier, AlgS.Poly.equiv R (AlgS.Poly.mul R p q) (AlgS.Poly.mul R q p). A polynomial is a coefficient function and AlgS.Poly.equiv is coefficientwise equivalence; the product is the convolution written as an antidiagonal walk. The proof is two steps and no induction of its own: AlgS.Poly.antidiagFrom_rev at the cell family fun i j => R.mul (p i) (q j) reverses the walk, and AlgS.Poly.antidiagFrom_congr with R's own mulComm at each cell turns R.mul (p j) (q i) into R.mul (q i) (p j). This is one of the four AlgS.CommRing fields ADR-1609 left open for the polynomial ring.

Formal statement

theorem AlgS.Poly.mulComm : ((x0 : AlgS.CommRing) -> ((x1 : ((x1 : AxNat) -> AlgS.CommRing.carrier x0)) -> ((x2 : ((x2 : AxNat) -> AlgS.CommRing.carrier x0)) -> AlgS.Poly.equiv x0 (AlgS.Poly.mul x0 x1 x2) (AlgS.Poly.mul x0 x2 x1))))

Dependencies

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

1 direct dependencies 1 direct dependents

Evidence

algs-poly-mul-comm-1

Kind: kernel-term
Status: checked

Supports: AlgS.Poly.mulComm admits through the trusted Kernel::add_declaration gate with an empty Kernel::axiom_footprint, and is one of the twenty-three fields Kernel::add_declaration re-checked when admitting AlgS.Poly.commRing as an AlgS.CommRing VALUE. The suite pins the convolution's order definitionally at indices 0, 1 and 2 with negative twins that swap the summands, swap the factors and re-nest the sum, so a commuted or reordered walk fails; and the reversal this theorem rests on carries its own evaluation test at n = 2 and 3 plus a rejection control.

Checker command

out=$(RUST_MIN_STACK=1073741824 cargo test -p axeyum-lean-kernel --lib --release poly_setoid_tests -- --test-threads=4 2>&1) && test "$(printf "%s\n" "$out" | grep -cE 'test result: ok\. 17 passed; 0 failed')" -ge 1

Evidence notes

The pinned count is 17. A dropped or renamed test changes the count and fails the command. Five of the seventeen are rejection controls, each carrying a POSITIVE TWIN in the same test: a record-field or proof-term mutation poisons the whole prelude build (measured: mutating mulAssoc's join step made all 17 die on the fixture's expect), so a refusal is only evidence about the field once the honest reconstruction is shown to admit beside it. Each of the five controls was itself mutated to the honest statement and exactly those five died, the other twelve passing.

Provenance

{
  "date": "2026-09-04",
  "established_by": "axeyum-lean-kernel nat_prelude::polynomial_setoid, lane poly-commring, ADR-1618 (roadmap W2-9's residue).",
  "source": "crates/axeyum-lean-kernel/src/nat_prelude/polynomial_setoid.rs; tests nat_prelude::polynomial_setoid::poly_setoid_tests::*."
}