Sums of two squares are closed under multiplication (over the constructed integers)

Identifier: F:int-sum-of-two-squares-multiplicative
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

If m and n are each a sum of two integer squares then so is their product. This is the Brahmagupta-Fibonacci identity read as a closure property of the predicate Int.IsSumOfTwoSquares n := exists a b, n = a*a + b*b, which this lane declared as a named Definition so that the whole two-squares family quantifies over one term instead of four spellings of the same double existential.

Formal statement

theorem Int.isSumOfTwoSquares_mul : ((x0 : Int) -> ((x1 : Int) -> ((x2 : Int.IsSumOfTwoSquares x0) -> ((x3 : Int.IsSumOfTwoSquares x1) -> Int.IsSumOfTwoSquares (Int.mul x0 x1)))))

Dependencies

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

1 direct dependencies 2 direct dependents

Evidence

kernel-Int.isSumOfTwoSquares_mul

Kind: kernel-term
Status: checked

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

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_composition_law_applies_to_two_concrete_witnesses, the_three_primes_are_witnessed_sums_of_two_squares, wrong_pairs_are_refused_by_the_kernel, is_sum_of_two_squares_unfolds_to_the_intended_double_existential, the_witness_slots_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.isSumOfTwoSquares_mul

Kind: exhaustive-enumeration
Status: checked

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

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 closure property classically read off Brahmagupta's identity; the predicate Int.IsSumOfTwoSquares is this repository's own Definition, not an import",
  "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"
    }
  ]
}