Squaring is monotone on a symmetric band over the integers

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

Recorded description

If -b <= a and a <= b then a*a <= b*b. No absolute value is mentioned: the two-sided band IS the hypothesis. The non-negative half is Int.mul_le_mul_of_nonneg_left applied twice through mul_comm; the non-positive half is the same argument at -a, whose square ring::int identifies with a's.

Formal statement

theorem Int.sq_le_sq_of_neg_le_of_le : ((x0 : Int) -> ((x1 : Int) -> ((x2 : Int.le (Int.neg x1) x0) -> ((x3 : Int.le x0 x1) -> Int.le (Int.mul x0 x0) (Int.mul x1 x1)))))

Dependencies

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

7 direct dependencies 1 direct dependents

Evidence

kernel-Int.sq_le_sq_of_neg_le_of_le

Kind: kernel-term
Status: checked

Supports: Int.sq_le_sq_of_neg_le_of_le is admitted by the trusted kernel gate with EXACTLY the type recorded in formal.statement, which is a verbatim quotation of the kernel's own renderer.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example int_theorem_inventory -- Int.sq_le_sq_of_neg_le_of_le 2>/dev/null | grep -cE '^theorem[[:space:]]+Int\\.sq_le_sq_of_neg_le_of_le[[:space:]]'

Evidence notes

Two independent failure modes, so the exit status depends on the FINDING and not on the run completing: int_theorem_inventory exits non-zero when the named filter matches nothing, and grep -c exits 1 printing 0 when the anchored line is absent. Anchored with [[:space:]] and never with a backslash-t, which a scripted (GNU) grep reads as a literal t. grep -c rather than grep -q, which would SIGPIPE the producer under pipefail. --release is MANDATORY: this tool builds the constructed carriers and overflows the default debug thread stack.

evaluation-Int.sq_le_sq_of_neg_le_of_le

Kind: instance-pin
Status: checked

Supports: What the declaration MEANS: its full forall-telescoped type is rebuilt independently and compared against the type the ENVIRONMENT stores, and it is applied at concrete small arguments where the kernel must ACCEPT the in-band instance and REFUSE the out-of-band one.

Checker command

cargo test --release -p axeyum-lean-kernel --lib -- int_prelude::order_squares_tests --test-threads=4 2>/dev/null | grep -cE '^test result: ok\. 6 passed'

Evidence notes

The count 6 is pinned deliberately: a suite that silently stopped compiling some of these tests would still print ok with a smaller number, and this repository has shipped a gate that ran zero tests for 15 days while exiting 0. Relevant test for this row: the_two_sided_square_bound_applies_on_both_signs_and_refuses_an_out_of_band_argument, which admits 2*2 <= 3*3 AND (-2)*(-2) <= 3*3 and requires the kernel to REFUSE 4 and -4 against the same bound. The negative row is the discriminating one: it is the branch that goes through Int.neg_mul_neg, and a lemma stated only for non-negative arguments would pass the first row and fail it.

footprint-Int.sq_le_sq_of_neg_le_of_le

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the integer prelude's trusted surface is empty (no Axiom, no Opaque, no Quotient), which bounds every declaration in it, including this one.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example nat_axiom_inventory -- --require-axiom-free integer

Evidence notes

The per-declaration assertion lives in order_squares_tests::every_order_squares_declaration_is_present_and_axiom_free, which checks Environment::contains FIRST for all 23 names -- an empty footprint is also what a MISSING name returns. Coverage is additionally forced by int_prelude_tests::every_int_declaration_is_checked_and_axiom_free, which derives its subject from the environment rather than from a list, so all 23 names had to be added to derived_laws (294 -> 317) before it would pass.

Provenance

{
  "date": "2026-09-05",
  "curation": "curated",
  "established_by": "lane int-order-two-squares (W3-10 second slice, ADR-1647), crates/axeyum-lean-kernel/src/int_prelude/order_squares.rs, admitted by build_int_prelude",
  "source": "the ordering half of Euler's descent proof (1749) of Fermat's two-square theorem, isolated so the algebraic half (F:int-two-squares-descent-step) can consume it",
  "prior_art": [
    {
      "who": "Fermat; Euler",
      "what": "Fermat's theorem on sums of two squares (asserted 1640) and Euler's descent proof (1749), whose ordering half these laws supply",
      "year": 1749,
      "where": "classical number theory; standard textbook material",
      "attribution": "standard textbook attribution; this lane did not consult the primary sources"
    }
  ]
}