The strict decrease of the two-squares descent measure

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

Recorded description

If m > 0 and both c and e lie in the symmetric band -m <= x + x <= m, then c*c + e*e < m*m. Only m > 0 is needed; 1 < m is NOT required, because the strictness comes from the halving and not from a gap between m and 1. The multiplied-through form 2*(c*c + e*e) <= m*m is Int.two_mul_sq_add_sq_le_sq, recorded in the same module.

Formal statement

theorem Int.sq_add_sq_lt_sq_of_bounds : ((x0 : Int) -> ((x1 : Int) -> ((x2 : Int) -> ((x3 : Int.lt Int.zero x0) -> ((x4 : Int.le (Int.neg x0) (Int.add x1 x1)) -> ((x5 : Int.le (Int.add x1 x1) x0) -> ((x6 : Int.le (Int.neg x0) (Int.add x2 x2)) -> ((x7 : Int.le (Int.add x2 x2) x0) -> Int.lt (Int.add (Int.mul x1 x1) (Int.mul x2 x2)) (Int.mul x0 x0)))))))))

Dependencies

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

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

Evidence

kernel-Int.sq_add_sq_lt_sq_of_bounds

Kind: kernel-term
Status: checked

Supports: Int.sq_add_sq_lt_sq_of_bounds 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_add_sq_lt_sq_of_bounds 2>/dev/null | grep -cE '^theorem[[:space:]]+Int\\.sq_add_sq_lt_sq_of_bounds[[: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_add_sq_lt_sq_of_bounds

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

Relevant test: the_strict_decrease_applies_inside_the_band_and_is_refused_outside_it. At m = 5 it admits 2*2 + 1*1 < 5*5 and REFUSES c = 3 -- whose conclusion 9 + 1 < 25 is still TRUE, so the refusal pins that the BOUND is load-bearing in the statement rather than that the arithmetic happens to work out. MUTATION-MEASURED: replacing m*m by m in the conclusion is REJECTED BY THE KERNEL, killing 119 of the 122 int_prelude tests (3 survive because they do not build the Int prelude).

footprint-Int.sq_add_sq_lt_sq_of_bounds

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"
    }
  ]
}