The termination certificate of the two-squares descent, read off the factorisation

Identifier: F:int-descent-multiplier-bounds
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

If m > 0, m*q = c*c + e*e, and both c and e lie in the symmetric band -m <= x + x <= m, then 0 <= q and q < m. This is the shape Fermat's descent actually consumes: it takes the FACTORISATION rather than the measure, and returns both halves of the termination argument at once.

Formal statement

theorem Int.descentMultiplierBounds : ((x0 : Int) -> ((x1 : Int) -> ((x2 : Int) -> ((x3 : Int) -> ((x4 : Int.lt Int.zero x0) -> ((x5 : Eq.{1} Int (Int.mul x0 x1) (Int.add (Int.mul x2 x2) (Int.mul x3 x3))) -> ((x6 : Int.le (Int.neg x0) (Int.add x2 x2)) -> ((x7 : Int.le (Int.add x2 x2) x0) -> ((x8 : Int.le (Int.neg x0) (Int.add x3 x3)) -> ((x9 : Int.le (Int.add x3 x3) x0) -> And (Int.le Int.zero x1) (Int.lt x1 x0)))))))))))

Dependencies

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

8 direct dependencies 1 direct dependents

Evidence

kernel-Int.descentMultiplierBounds

Kind: kernel-term
Status: checked

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

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_multiplier_bounds_apply_at_a_worked_factorisation_and_refuse_a_wrong_quotient. 5*1 = 2*2 + 1*1 certifies 0 <= 1 AND 1 < 5; the same call with q = 2 is REFUSED, even though 0 <= 2 AND 2 < 5 is perfectly true -- so the refusal row is what says the FACTORISATION hypothesis is actually read. A lemma that ignored its second hypothesis would pass both rows without it.

footprint-Int.descentMultiplierBounds

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