Every residue class modulo a positive integer has a representative in the symmetric band

Identifier: F:int-exists-centered-representative
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For any a and any m > 0 there is a c with c congruent to a modulo m and -m <= c + c <= m. The witness is a % m when (a % m) + (a % m) <= m, and (a % m) - m otherwise. This is the BOUNDED CHOICE OF REPRESENTATIVE that Fermat's descent needs and that the two-squares lane recorded as missing.

Formal statement

theorem Int.exists_centered_representative : ((x0 : Int) -> ((x1 : Int) -> ((x2 : Int.lt Int.zero x1) -> Exists.{1} Int (fun (x3 : Int) => And (Int.ModEq x1 x3 x0) (And (Int.le (Int.neg x1) (Int.add x3 x3)) (Int.le (Int.add x3 x3) x1))))))

Dependencies

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

15 direct dependencies 2 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-Int.exists_centered_representative

Kind: kernel-term
Status: checked

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

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_centered_representative_keeps_the_small_residue_and_shifts_the_large_one. At m = 5 it pins BOTH branches -- 7 % 5 = 2 is kept, 8 % 5 = 3 must shift to -2, and c = 3 is REFUSED. Nothing else distinguishes the two branches: a construction that returned the bare remainder in both would pass the first row and fail the third. A fourth row requires 7 to be NOT congruent to -2 modulo 5, so the congruence conjunct is not vacuous either.

footprint-Int.exists_centered_representative

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