In an abstract ring, any element times zero is zero

Identifier: F:alg-ring-mul-zero
Proof route: kernel-lean
External status: unknown
Axiom footprint: Empty

Recorded description

For any ring record R (an abstract carrier, additive commutative group, multiplication, distributive laws) and any a of R's carrier, mul a zero = zero -- derived from the additive-group and distributive axioms alone, without ever using a multiplicative identity.

Formal statement

theorem Alg.ringMulZero : ((x0 : Alg.Ring) -> ((x1 : Alg.Ring.carrier x0) -> Eq.{1} (Alg.Ring.carrier x0) (Alg.Ring.mul x0 x1 (Alg.Ring.zero x0)) (Alg.Ring.zero x0)))

Dependencies

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

2 direct dependencies 2 direct dependents

Evidence

alg-ring-mul-zero-1

Kind: kernel-term
Status: checked

Supports: Alg.ringMulZero admits through the trusted kernel gate and, applied at TWO CONCRETE Alg.Ring instances (Int.ring, Rat.ring, each built independently of the Alg.CommRing/Alg.Field instances from the same underlying Int.*/Rat.* lemma constants -- no inheritance) closed over a symbolic a, type-checks to a term def_eq to `mul a zero = zero` with mul/zero iota-reduced through each instance's own selectors.

Checker command

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

Evidence notes

The pattern is anchored on cargo's own pass/fail summary line with BOTH counts pinned ('1 passed; 0 failed'), so a wrong reduced type (a def_eq assertion failure) or a kernel refusal of the instantiation both make the test panic and the pattern stop matching.

Provenance

{
  "date": "2026-09-03",
  "established_by": "axeyum-lean-kernel build_rat_prelude, lane structures-1, ADR-1578 -- proved once over the abstract Alg.Ring record from the additive-group and distributive axioms alone, and instantiated at two independently-built carriers.",
  "source": "crates/axeyum-lean-kernel/src/rat_prelude/algebra_instances.rs (build_ring_mul_zero, declared as Alg.ringMulZero); test rat_prelude::algebra_instances::algebra_instances_tests::ring_mul_zero_applies_at_int_and_rat_instances."
}