A strict integer inequality survives addition of a non-strict one

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

Recorded description

For all integers a, b, c and d, if a <= b and c < d then a + c < b + d.

Formal statement

theorem Int.add_lt_add_of_le_of_lt : ((x0 : Int) -> ((x1 : Int) -> ((x2 : Int) -> ((x3 : Int) -> ((x4 : Int.le x0 x1) -> ((x5 : Int.lt x2 x3) -> Int.lt (Int.add x0 x2) (Int.add x1 x3)))))))

Dependencies

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

6 direct dependencies 5 direct dependents

Evidence

kernel-Int.add_lt_add_of_le_of_lt

Kind: kernel-term
Status: checked

Supports: For all integers a, b, c and d, if a <= b and c < d then a + c < b + d.

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

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