In an abstract Setoid-flavored group, the inverse of the inverse is the original element (up to equiv)

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

Recorded description

For any AlgS.Group record G and element a of G's carrier, equiv (inv (inv a)) a -- a direct instantiation of AlgS.inv_unique at (a := inv a, b := inv (inv a), c := a), h1 := invL(inv a), h2 := invL a, mirroring Alg.neg_neg's own proof exactly.

Formal statement

theorem AlgS.invInv : ((x0 : AlgS.Group) -> ((x1 : AlgS.Group.carrier x0) -> AlgS.Group.equiv x0 (AlgS.Group.inv x0 (AlgS.Group.inv x0 x1)) x1))

Dependencies

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

1 direct dependencies 1 direct dependents

Evidence

algs-inv-inv-1

Kind: kernel-term
Status: checked

Supports: AlgS.invInv admits through the trusted kernel gate and, applied at AlgS.Group.ofAlg(Int.addGroup), type-checks both concretely (at Int.zero) and symbolically (a free a). Int has no named neg_neg/invInv kernel theorem (ADR-1584 section 3: int_prelude/gcd.rs's neg_neg is a private, never-declared Rust helper), so this is a well-typedness measurement, like AlgS.neg_neg's own Int control.

Checker command

out=$(RUST_MIN_STACK=1073741824 cargo test -p axeyum-lean-kernel --lib --release -- inv_inv_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

algs-inv-inv-2

Kind: kernel-term
Status: checked

Supports: AlgS.invInv, applied at CReal.addGroupS (AlgS.CommGroup.toGroupS(AlgS.CommRing.toCommGroupS(CReal.commRingS)), a NAMED projection chain, not the earlier test-only ring_s_additive_group_value builder), type-checks closed over a free a : CReal -- reaching a carrier Alg.neg_neg (Eq-flavored) could never reach directly.

Checker command

out=$(RUST_MIN_STACK=1073741824 cargo test -p axeyum-lean-kernel --lib --release -- generic_inv_unique_and_inv_inv_instantiated_at_creal_add_group_s_type_check --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_inv), lane structures-ordered-setoid, ADR-1592.",
  "source": "crates/axeyum-lean-kernel/src/nat_prelude/structures_setoid.rs (declare_inv_inv, declared as AlgS.invInv); crates/axeyum-lean-kernel/src/rat_prelude/algebra_ext.rs (build_neg_neg, now deriving Alg.neg_neg from AlgS.invInv via AlgS.Group.ofAlg); crates/axeyum-lean-kernel/src/creal/algebra_instance.rs (CReal.addGroupS)."
}