Negating the RIGHT factor is a separate theorem from negating the left one, in a ring without commutative multiplication

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

Recorded description

Let R be an AlgS.OrderedRing and a, b elements of R. Then a*(-b) is equivalent to -(a*b). ADR-1616 proved only the LEFT-handed form, (-a)*b ~ -(a*b), and without mulComm -- which AlgS.OrderedRing deliberately does not carry -- the right-handed form does not follow from it: the two are different statements, which the accompanying test asserts by requiring the kernel to refuse to identify their types. The proof goes through AlgS.mul_neg_one on the ring projection rather than through a second additive-cancellation argument: a*(-b) ~ a*(b*(-1)) ~ (a*b)*(-1) ~ -(a*b), of which the middle step is just associativity.

Formal statement

theorem AlgS.OrderedRing.mul_neg : forall (R : AlgS.OrderedRing) (a b : R.carrier), R.equiv (R.mul a (R.neg b)) (R.neg (R.mul a b))

Dependencies

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

1 direct dependencies 1 direct dependents

Evidence

kernel-axiom-free

Kind: kernel-term
Status: checked

Supports: The declaration is admitted by the trusted kernel gate with an empty Kernel::axiom_footprint, together with every other declaration of ADR-1631's generic Bernoulli layer. The test asserts Environment::contains FIRST, because an absent name has an empty footprint too, and it pins its own name-list length, so a declaration silently dropped from the layer fails it.

Checker command

cargo test --release -p axeyum-lean-kernel --lib rat_prelude::binomial_s::binomial_s_tests::binomial_s_declarations_are_axiom_free -- --exact 2>&1 | grep -c '^test result: ok. 1 passed'

Evidence notes

grep -c, not grep -q: -q would SIGPIPE the producer under pipefail, and -c exits 1 printing 0 when the line is absent, so a suite that compiled to zero tests and exited 0 is caught rather than counted as a pass. --release is mandatory: the rational prelude SIGABRTs on the default debug thread stack.

distinct-from-neg-mul

Kind: kernel-term
Status: checked

Supports: The test infers both theorems' types and requires that the kernel does NOT call them definitionally equal, with a positive control (mul_neg's type is definitionally itself) so a def_eq that had stopped deciding would be visible. Without that assertion the claim 'the spine was missing one of them' would rest on reading two doc comments.

Checker command

cargo test --release -p axeyum-lean-kernel --lib rat_prelude::binomial_s::binomial_s_tests::mul_neg_is_not_neg_mul -- --exact 2>&1 | grep -c '^test result: ok. 1 passed'

Evidence notes

Provenance

{
  "date": "2026-09-05",
  "established_by": "lane binomial-hoeffding (roadmap W3-12, ADR-1631)"
}