In an abstract ring, x*(-1)=-x

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

Recorded description

For any ring record R (an abstract carrier, additive/multiplicative structure, negation) and element x of R's carrier, mul x (neg one) = neg x.

Formal statement

theorem Alg.mul_neg_one : ((x0 : Alg.Ring) -> ((x1 : Alg.Ring.carrier x0) -> Eq.{1} (Alg.Ring.carrier x0) (Alg.Ring.mul x0 x1 (Alg.Ring.neg x0 (Alg.Ring.one x0))) (Alg.Ring.neg x0 x1)))

Dependencies

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

3 direct dependencies 0 direct dependents

Evidence

alg-mul-neg-one-1

Kind: kernel-term
Status: checked

Supports: Alg.mul_neg_one admits through the trusted kernel gate. Built by projecting R's additive structure to a Group (Ring.toCommGroup then CommGroup.toGroup -- the payoff Alg.CommMonoid.toMonoid/etc exist for) and applying Alg.groupInvUnique there at (x, mul x (neg one), neg x), rather than deriving `mul a (neg b) = neg (mul a b)` directly. FACT1 (add (mul x (neg one)) x = zero) is derived from distribL, Alg.ringMulZero, and mulOneR; FACT2 is R.negAdd x directly. Type-checks symbolically (closed over free x) at both Int.ring and Rat.ring.

Checker command

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

alg-mul-neg-one-2

Kind: kernel-term
Status: checked

Supports: NO retirement target under this exact name/direction on either carrier: Int's `neg_one_mul` is the MIRRORED LEFT form ((-1)*x=-x, not x*(-1)=-x) and Rat has no `mul_neg_one`/`neg_one_mul` at all. Bridging the two directions needs mul_comm (a CommRing fact this theorem is deliberately stated without, since it is proved at the Ring level). Confirmed by a compiled reference to Int.neg_one_mul (a field that would fail to compile if renamed/removed), not by a text grep alone.

Checker command

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

Provenance

{
  "date": "2026-09-03",
  "established_by": "axeyum-lean-kernel build_rat_prelude, lane structures-2, ADR-1584.",
  "source": "crates/axeyum-lean-kernel/src/rat_prelude/algebra_ext.rs (build_mul_neg_one, declared as Alg.mul_neg_one); tests rat_prelude::algebra_ext::algebra_ext_tests::sub_self_and_mul_neg_one_apply_symbolically_at_int_and_rat_rings, ::mul_neg_one_has_no_retirement_target."
}