The integer borrow has exactly two outcomes, and each is witnessed by a natural

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

Recorded description

For any property P of integers and any naturals m and n: if P holds of ofNat i whenever n + i = m, and P holds of negSucc i whenever m + (i+1) = n, then P holds of the normalized difference of m and n.

Formal statement

theorem Int.subNatNat_elim : ((x0 : ((x0 : Int) -> Prop)) -> ((x1 : AxNat) -> ((x2 : AxNat) -> ((x3 : ((x3 : AxNat) -> ((x4 : Eq.{1} AxNat (AxNat.add x2 x3) x1) -> x0 (Int.ofNat x3)))) -> ((x4 : ((x4 : AxNat) -> ((x5 : Eq.{1} AxNat (AxNat.add x1 (AxNat.succ x4)) x2) -> x0 (Int.negSucc x4)))) -> x0 (Int.subNatNat x1 x2))))))

Dependencies

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

6 direct dependencies 11 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-Int.subNatNat_elim

Kind: kernel-term
Status: checked

Supports: For any property P of integers and any naturals m and n: if P holds of ofNat i whenever n + i = m, and P holds of negSucc i whenever m + (i+1) = n, then P holds of 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_elim

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_elim 2>/dev/null | grep -Ec '^theorem[[:space:]]+Int\.subNatNat_elim[[: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"
}