In an abstract Setoid-flavored group, a left inverse equals a right inverse (up to equiv)

Identifier: F:algs-inv-unique
Proof route: kernel-lean
External status: unknown
Axiom footprint: Empty

Recorded description

For any AlgS.Group record G (an abstract carrier, a caller-supplied equivalence relation equiv with a congruence field for op, and the two-sided identity/inverse laws stated over equiv rather than Eq) and elements a b c of G's carrier, if equiv (op b a) e and equiv (op a c) e then equiv b c -- the setoid twin of Alg.groupInvUnique, proved by the identical chain b = b*e = b*(a*c) = (b*a)*c = e*c = c, with equivTrans/equivSymm/opCongr in place of Eq.trans/symm_of/congr_arg.

Formal statement

theorem AlgS.inv_unique : ((x0 : AlgS.Group) -> ((x1 : AlgS.Group.carrier x0) -> ((x2 : AlgS.Group.carrier x0) -> ((x3 : AlgS.Group.carrier x0) -> ((x4 : AlgS.Group.equiv x0 (AlgS.Group.op x0 x2 x1) (AlgS.Group.e x0)) -> ((x5 : AlgS.Group.equiv x0 (AlgS.Group.op x0 x1 x3) (AlgS.Group.e x0)) -> AlgS.Group.equiv x0 x2 x3))))))

Dependencies

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

1 direct dependencies 2 direct dependents

Evidence

algs-inv-unique-1

Kind: kernel-term
Status: checked

Supports: AlgS.inv_unique admits through the trusted kernel gate with an empty axiom footprint, and instantiated at AlgS.Group.ofAlg(Int.addGroup) closed over (a,b,c) type-checks (well-typedness only, no named Int counterpart to def_eq against). This is the AlgS.Group-level generic theorem ADR-1590 (amending ADR-1588) named as missing -- there was no AlgS record-level generic theorem at all before this fact, which is why Alg.neg_neg (stated over Alg.Group) could not previously derive from the setoid spine.

Checker command

out=$(RUST_MIN_STACK=1073741824 cargo test -p axeyum-lean-kernel --lib --release -- inv_unique_instantiated_at_int_through_ofalg_concrete_and_symbolic --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 nat_prelude::structures_setoid (declare_inv_unique/build_group_inv_unique_s), lane structures-ordered-setoid, ADR-1592 -- closes the AlgS.Group-level generic-theorem gap ADR-1590 named explicitly.",
  "source": "crates/axeyum-lean-kernel/src/nat_prelude/structures_setoid.rs (build_group_inv_unique_s, declare_inv_unique, declared as AlgS.inv_unique); test nat_prelude::structures_setoid::structures_setoid_tests::inv_unique_instantiated_at_int_through_ofalg_concrete_and_symbolic."
}