Both cross terms of the conjugate Brahmagupta grouping vanish modulo the multiplier

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

Recorded description

Let m > 0, let c = a and e = b modulo m, and let a^2 + b^2 = 0 modulo m. Then BOTH a*c + b*e and a*e - b*c are 0 modulo m. This is the congruence half of Fermat's descent, and the reason the descent uses the conjugate grouping (ac+bd)^2 + (ad-bc)^2 rather than the textbook one: it is exactly the divisibility that licenses dividing the product through by m.

Formal statement

theorem Int.modEq_descent_cross_terms : ((x0 : Int) -> ((x1 : Int) -> ((x2 : Int) -> ((x3 : Int) -> ((x4 : Int) -> ((x5 : Int.lt Int.zero x0) -> ((x6 : Int.ModEq x0 x3 x1) -> ((x7 : Int.ModEq x0 x4 x2) -> ((x8 : Int.ModEq x0 (Int.add (Int.mul x1 x1) (Int.mul x2 x2)) Int.zero) -> And (Int.ModEq x0 (Int.add (Int.mul x1 x3) (Int.mul x2 x4)) Int.zero) (Int.ModEq x0 (Int.sub (Int.mul x1 x4) (Int.mul x2 x3)) Int.zero))))))))))

Dependencies

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

5 direct dependencies 3 direct dependents

Evidence

kernel-Int.modEq_descent_cross_terms

Kind: kernel-term
Status: checked

Supports: Int.modEq_descent_cross_terms is admitted by the trusted kernel gate with the type recorded in formal.statement.

Checker command

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

Evidence notes

Two independent failure modes, so the exit status depends on the finding rather than 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. The anchor AFTER the name is load-bearing here, because Int.brahmaguptaFibonacci' is a different declaration whose rendered name has Int.brahmaguptaFibonacci as a prefix.

evaluation-Int.modEq_descent_cross_terms

Kind: instance-pin
Status: checked

Supports: What the declaration MEANS, settled at concrete small arguments and at free variables. The kernel gate cannot do this, and for the Definition Int.IsSumOfTwoSquares nothing else can.

Checker command

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

Evidence notes

The count 16 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 tests for this row: the_cross_terms_are_divisible_by_the_multiplier, the_cross_term_conjuncts_are_ordered_as_stated. MUTATION-MEASURED: transposing both the conjunction and its And.intro in Int.modEq_descent_cross_terms SURVIVED the whole suite (0 kills of 15), because at the worked instance (m,a,b,c,e) = (2,5,1,1,1) both conjuncts reduce to Eq Int 0 0 and the two orderings are definitionally equal there; the_cross_term_conjuncts_are_ordered_as_stated was added in response and kills that mutant with EXACTLY ONE failing test (15 passed, 1 failed).

footprint-Int.modEq_descent_cross_terms

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the integer prelude's trusted surface is empty, which bounds Int.modEq_descent_cross_terms.

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 two_squares_tests::every_two_squares_declaration_is_present_and_axiom_free, which checks Environment::contains FIRST for all 20 names. An empty footprint is also what a missing name returns, so without the containment check the footprint assertion would pass for a declaration that does not exist. The name list there is written out in full rather than derived from the module, which is a known weakness: it measures this lane's memory of what it declared, not the module's actual output.

Provenance

{
  "date": "2026-09-05",
  "curation": "curated",
  "established_by": "the two-squares lane (W3-10, ADR-1633), crates/axeyum-lean-kernel/src/int_prelude/two_squares.rs, admitted by build_int_prelude",
  "source": "the congruence step of Euler's descent proof (1749) of Fermat's two-square theorem, isolated here as a standalone reusable lemma",
  "prior_art": [
    {
      "who": "Brahmagupta; Fibonacci; Fermat; Euler",
      "what": "the composition identity for sums of two squares (Brahmagupta 628, restated by Fibonacci 1225), 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"
    }
  ]
}