The descent's next multiplier exists

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

Recorded description

Let m*p = a*a + b*b, and let c and e be congruent to a and b modulo m. Then c*c + e*e is again a multiple of m: there is a q with m*q = c*c + e*e. This is the step that turns a bounded choice of representatives into the NEXT multiplier of Euler's descent. Positivity of m is deliberately NOT a hypothesis -- every congruence used is unconditional in the modulus -- and the conclusion is spelled m*q = c*c + e*e rather than Int.dvd's own c*c + e*e = m*q so that it matches Int.descentMultiplierBounds and Int.descentStep verbatim.

Formal statement

theorem Int.exists_next_multiplier : ((x0 : Int) -> ((x1 : Int) -> ((x2 : Int) -> ((x3 : Int) -> ((x4 : Int) -> ((x5 : Int) -> ((x6 : Eq.{1} Int (Int.mul x0 x1) (Int.add (Int.mul x2 x2) (Int.mul x3 x3))) -> ((x7 : Int.ModEq x0 x4 x2) -> ((x8 : Int.ModEq x0 x5 x3) -> Exists.{1} Int (fun (x9 : Int) => Eq.{1} Int (Int.mul x0 x9) (Int.add (Int.mul x4 x4) (Int.mul x5 x5))))))))))))

Dependencies

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

3 direct dependencies 2 direct dependents

Evidence

kernel-Int.exists_next_multiplier

Kind: kernel-term
Status: checked

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

pin-fermat-two-squares

Kind: instance-pin
Status: checked

Supports: What the declarations MEAN: each of the twelve has its full forall-telescoped type rebuilt independently in the test file and compared with Kernel::def_eq against the type the ENVIRONMENT stores, at free variables. checked == 12 is asserted, so a deleted row fails rather than passing quietly. Int.fermatTwoSquares is additionally APPLIED at p = 5, 13 and 17 with a real Nat.Even witness, and two wrong applications must be REFUSED.

Checker command

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

Evidence notes

The count 5 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. MUTATION-MEASURED, all three rows RUN and restored byte-for-byte: dropping the Nat.lt n p hypothesis from the PIN's own expected type for Int.exists_sum_of_two_squares_of_multiple -- leaving the declaration alone, so the prelude still builds -- kills EXACTLY ONE test (4 passed, 1 failed), fermat_two_squares_declarations_state_the_intended_types. The two mutants that touch the PROOF instead (the IH fed n rather than natAbs q; the n = 1 branch refuted from n < p rather than 1 < n) both make the prelude un-buildable and kill 125 of 128 int_prelude:: tests each -- total, but identical for two mutants at opposite ends of the proof, so it says nothing about which guard caught either, and neither error message names the defect (both are a bare TypeMismatch over two ExprIds).

footprint-fermat-two-squares

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 fermat_two_squares_tests::every_declaration_is_a_checked_axiom_free_theorem, which checks Environment::contains FIRST for all 12 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 12 names had to be added to derived_laws (319 -> 331, recounted with recount-pinned-inventory.py rather than incremented) before it would pass.

Provenance

{
  "date": "2026-09-06",
  "curation": "curated",
  "established_by": "lane fermat-two-squares (W3-10 third slice, ADR-1650), crates/axeyum-lean-kernel/src/int_prelude/fermat_two_squares.rs, admitted by build_int_prelude",
  "source": "a step of Euler's descent proof (1749) of Fermat's theorem on sums 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"
    }
  ]
}