The normalized integer difference is invariant under a common shift

Identifier: F:int-sub-nat-nat-shift
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For all naturals m, n and k, the normalized difference of m+k and n+k is the normalized difference of m and n.

Formal statement

theorem Int.subNatNat_add_add : ((x0 : AxNat) -> ((x1 : AxNat) -> ((x2 : AxNat) -> Eq.{1} Int (Int.subNatNat (AxNat.add x0 x2) (AxNat.add x1 x2)) (Int.subNatNat x0 x1))))

Dependencies

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

2 direct dependencies 3 direct dependents

Evidence

kernel-Int.subNatNat_add_add

Kind: kernel-term
Status: checked

Supports: For all naturals m, n and k, the normalized difference of m+k and n+k is the normalized difference of m and n.

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-15: 12 tests pass (a nonzero count -- the filter is not inert). A real Lean 4.30.0 kernel also read the module this prelude exports to: `scripts/check-lean-gate.sh` reports 12 suites, 49 tests, 112 real-Lean checks (floor 105).

footprint-Int.subNatNat_add_add

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 -- subNatNat_add_add 2>/dev/null | grep -Ec '^theorem[[:space:]]+Int\.subNatNat_add_add[[: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; `int_theorem_inventory` prints it as the third tab-separated column, and the regex requires that column to be EMPTY -- the type must begin immediately after the name. The negative control is in the same output: `Int.euclidean_decomposition`, the one law still asserted, prints its own name in that column and fails the same regex (measured 2026-08-15). So the check discriminates rather than merely running. (2) `nat_axiom_inventory` reports `nat: axiom=0 opaque=0 quotient=0` for the development ZZ is constructed over. Counting `Declaration::Axiom` alone would not suffice: `Opaque` has no proof body and `Quotient` admits `Quot.sound` -- exactly the declaration a quotient-of-NxN construction would have added -- and the enumeration covers all three kinds and reports zero for each.

Provenance

{
  "date": "2026-08-15",
  "established_by": "axeyum-lean-kernel build_int_prelude, lane int-remainder",
  "source": "one of the six propositions build_int_prelude still ASSERTED after lane int-keystone constructed ZZ; this lane proved the `Int.subNatNat` borrow lemmas and derived it"
}