Every integer has an additive inverse

Identifier: F:int-add-neg
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For every integer a, a + (-a) = 0.

Formal statement

theorem Int.add_neg : ((x0 : Int) -> Eq.{1} Int (Int.add x0 (Int.neg x0)) Int.zero)

Dependencies

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

1 direct dependencies 46 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-Int.add_neg

Kind: kernel-term
Status: checked

Supports: For every integer a, a + (-a) = 0.

Checker command

cargo test -p axeyum-lean-kernel --lib int_prelude

Evidence notes

`build_int_prelude` admits this theorem through the trusted `Kernel::add_declaration` gate, which re-checks the proof term against the stated type, so a green run of the command is a machine-checked proof. Measured 2026-08-14: 12 tests pass (a nonzero count -- the filter is not inert).

footprint-Int.add_neg

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- this theorem's trusted closure is empty

Checker command

test "$(cargo run -q -p axeyum-lean-kernel --example int_theorem_inventory -- add_neg 2>/dev/null | grep -Ec '^theorem[[:space:]]+Int\.add_neg[[:space:]]')" -ge 1

Evidence notes

Two independent bounds, because either alone would be weaker than it looks. (1) `Kernel::axiom_footprint` walks THIS declaration's transitive dependencies and prints an empty footprint column -- this is the kernel's `#print axioms`, and it is the check that matters, since an integer law IS still asserted (`Int.euclidean_decomposition`; it was 6 until lane int-remainder proved the `subNatNat` borrow, and the check mattered more then) and Int.add_neg could have reached for one and still type-checked. (2) `nat_axiom_inventory` reports `nat: axiom=0 opaque=0 quotient=0` for the development ZZ is constructed over, so the foundation admits no trusted declaration at all. Counting `Declaration::Axiom` alone would not have sufficed: `Opaque` has no proof body and `Quotient` admits `Quot.sound`, which is exactly the declaration the quotient-of-NxN construction would have added -- the enumeration covers all three kinds and reports zero for each.

compute-Int.add_neg

Kind: exhaustive-enumeration
Status: checked

Supports: `Int.add` and `Int.neg` are the intended operations, not merely operations satisfying this law

Checker command

cargo test -p axeyum-lean-kernel --lib the_operations_compute_their_normal_forms

Evidence notes

A wrong `Int.add` would satisfy a wrong-but-provable `add_neg`, so the theorem alone does not pin the operation down. This test evaluates 16 additions and multiplications and 5 negations by kernel reduction against their normal forms, covering every sign combination including the borrow cases where `Int.subNatNat` has to decide which constructor the answer lands in (3 + (-3) = 0 and 1 + (-3) = -2 are both present).

Provenance

{
  "date": "2026-08-14",
  "established_by": "axeyum-lean-kernel build_int_prelude, lane int-keystone",
  "source": "one of the 34 propositions build_int_prelude previously ASSERTED; this lane constructed ZZ over the proved Nat development and derived it"
}