Equality of integers is decidable

Identifier: F:int-equality-is-decidable
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For all integers a and b, either a = b or a is not equal to b.

Formal statement

theorem Int.eq_em : ((x0 : Int) -> ((x1 : Int) -> Or (Eq.{1} Int x0 x1) (Not (Eq.{1} Int x0 x1))))

Dependencies

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

3 direct dependencies 8 direct dependents

Evidence

kernel-Int.eq_em

Kind: kernel-term
Status: checked

Supports: For all integers a and b, either a = b or a is not equal to b.

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.eq_em

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- decidability here costs no classical assumption

Checker command

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

Evidence notes

The empty footprint is the whole content of this fact. `Or P (Not P)` for an arbitrary `P` is NOT available on this route -- the logic prelude is intuitionistic and carries zero axioms of any trusted kind, so unrestricted excluded middle would have to be added as one. This instance is decidable instead of assumed, and the two are not interchangeable. `Kernel::axiom_footprint` walks the declaration's transitive dependencies and prints an empty column; `nat_axiom_inventory` independently reports `nat: axiom=0 opaque=0 quotient=0` for the development it rests on.

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 (ADR-0106); this lane constructed ZZ over the proved Nat development and derived it"
}