The entry point of Fermat's two-squares descent

Identifier: F:int-two-squares-descent-entry
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Let p > 0 with 1 + 1 <= p, and let x satisfy x*x = -1 (mod p). Then there are k and c with k*p = c*c + 1*1 and 0 < k < p. That is: a multiple of p is a sum of two squares, and the multiplier is ALREADY strictly between 0 and p -- which is the invariant the descent's induction needs, and the reason the representative has to be centered before the divisibility is read off. Primality is deliberately NOT a hypothesis: everything here needs only 0 < p and 1 + 1 <= p, and the caller derives the second from p = 2m+1 with m even and p prime, which is Nat work that does not belong in an Int order module.

Formal statement

theorem Int.exists_small_multiple_of_sq_add_one : ((x0 : Int) -> ((x1 : Int) -> ((x2 : Int.lt Int.zero x0) -> ((x3 : Int.le (Int.add Int.one Int.one) x0) -> ((x4 : Int.ModEq x0 (Int.mul x1 x1) (Int.neg Int.one)) -> Exists.{1} Int (fun (x5 : Int) => Exists.{1} Int (fun (x6 : Int) => And (Eq.{1} Int (Int.mul x5 x0) (Int.add (Int.mul x6 x6) (Int.mul Int.one Int.one))) (And (Int.lt Int.zero x5) (Int.lt x5 x0)))))))))

Dependencies

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

22 direct dependencies 1 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-Int.exists_small_multiple_of_sq_add_one

Kind: kernel-term
Status: checked

Supports: Int.exists_small_multiple_of_sq_add_one 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.exists_small_multiple_of_sq_add_one 2>/dev/null | grep -cE '^theorem[[:space:]]+Int\\.exists_small_multiple_of_sq_add_one[[: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. --release is MANDATORY: this tool builds the constructed carriers and overflows the default debug thread stack.

evaluation-Int.exists_small_multiple_of_sq_add_one

Kind: instance-pin
Status: checked

Supports: What the declaration MEANS: its full forall-telescoped type -- including the nested existential's body -- is rebuilt independently and compared against the type the ENVIRONMENT stores, and it is APPLIED at p = 5 with the hypotheses discharged by reduction, where a non-root of -1 must be REFUSED.

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\. 7 passed'

Evidence notes

The count 7 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: the_descent_entry_point_applies_at_a_square_root_of_minus_one_and_is_refused_off_it. At p = 5 it admits x = 2 (2*2 = 4 = -1 mod 5) and REFUSES x = 1 -- and the refusal row is the discriminating one, because the CONCLUSION at x = 1 is still true (1*5 = 2*2 + 1*1 witnesses it), so a lemma that ignored its congruence hypothesis would pass both rows. The statement pin additionally rebuilds the nested Exists body, which no application test can see.

footprint-Int.exists_small_multiple_of_sq_add_one

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 25 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, whose subject is derived from kernel.environment(), so all 25 names had to be added to derived_laws (294 -> 319) 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 entry step of Euler's descent proof (1749) of Fermat's two-square theorem: from -1 being a quadratic residue mod p, some multiple of p below p^2 is a sum of two squares",
  "prior_art": [
    {
      "who": "Fermat; Euler",
      "what": "Fermat's theorem on sums of two squares (asserted 1640) and Euler's descent proof (1749)",
      "year": 1749,
      "where": "classical number theory; standard textbook material",
      "attribution": "standard textbook attribution; this lane did not consult the primary sources"
    }
  ]
}