The CRT residue-pairing self-map is injective on a block of coprime dimensions

Identifier: F:nat-crt-self-map-injective-on
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For naturals mp, np, write m = mp+1 and n = np+1. If gcd(m, n) = 1 then the map g(x) = n*(x mod m) + (x mod n) is injective on [0, n*m). The statement is sharp: measured over every pair with 1 <= m,n <= 9, g is injective at every coprime pair and at NONE of the 26 non-coprime pairs, the smallest collision being m = n = 2 where g(0) = g(2) = 0. Both moduli are written as successors so their positivity is syntactic rather than hypothetical.

Formal statement

theorem Nat.crtSelfMap_injectiveOn : ((x0 : AxNat) -> ((x1 : AxNat) -> ((x2 : Eq.{1} AxNat (AxNat.gcd (AxNat.succ x0) (AxNat.succ x1)) (AxNat.succ AxNat.zero)) -> AxNat.injectiveOn (fun (x3 : AxNat) => AxNat.add (AxNat.mul (AxNat.succ x1) (AxNat.mod x3 (AxNat.succ x0))) (AxNat.mod x3 (AxNat.succ x1))) (AxNat.mul (AxNat.succ x1) (AxNat.succ x0)))))

Dependencies

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

8 direct dependencies 1 direct dependents

Evidence

kernel-Nat.crtSelfMap_injectiveOn

Kind: kernel-term
Status: checked

Supports: The coprimality-hypothesised injectivity of the residue-pairing self-map on [0, n*m), with the whole rendered type pinned.

Checker command

test "$(cargo run -q -p axeyum-lean-kernel --example nat_theorem_inventory -- crtSelfMap_injectiveOn 2>/dev/null | tr '\t' ' ' | grep -Fc 'Nat.crtSelfMap_injectiveOn 3 ((x0 : AxNat) -> ((x1 : AxNat) -> ((x2 : Eq.{1} AxNat (AxNat.gcd (AxNat.succ x0) (AxNat.succ x1)) (AxNat.succ AxNat.zero)) -> AxNat.injectiveOn (fun (x3 : AxNat) => AxNat.add (AxNat.mul (AxNat.succ x1) (AxNat.mod x3 (AxNat.succ x0))) (AxNat.mod x3 (AxNat.succ x1))) (AxNat.mul (AxNat.succ x1) (AxNat.succ x0)))))')" -ge 1

Evidence notes

The grep pins the WHOLE rendered type rather than the name, and here that is load-bearing rather than tidy. The kernel refuses a false theorem, but it cannot notice a statement that is weaker than intended, and this one has two ways to be weak that both still type-check: the map could be written with the two moduli swapped (`mod x (succ x1)` in the quotient slot), which is a DIFFERENT map, and the bound could be written `mul (succ x0) (succ x1)`, which is the same number by commutativity but a different term and not what `countRange_product` factors. Both are pinned by quoting the lambda and the bound verbatim. `nat_theorem_inventory` additionally exits non-zero for a name that does not exist, and `grep -Fc` consumes the whole pipe (so it cannot SIGPIPE the producer the way `grep -q` would) with the count tested by `test -ge 1`. NOTE, measured 2026-08-30: `nat_theorem_inventory` consumes only ONE name argument -- given two names in either order it reports on the LAST one only -- so this command deliberately passes exactly one.

sharpness-Nat.crtSelfMap_injectiveOn

Kind: exhaustive-enumeration
Status: checked

Supports: The coprimality hypothesis is necessary, not merely convenient: the map is injective at NO non-coprime pair with 1 <= m,n <= 9.

Checker command

python3 scripts/tests/check-totient-mul-coprime-numerics.py

Evidence notes

Twenty checks over the exact map this theorem is about, each paired with a negative control the script asserts must GENUINELY fail; any failure exits 1 naming the check. The two rows that bear on this fact are `InjectiveOn: g is injective on [0,n*m) at EVERY coprime pair` and its control `g is injective at NO non-coprime pair (0 of 26)`, plus a witness assertion that the m = n = 2 collision is real (g 0 = g 2 = 0 with 0 != 2). The Rust side checks the same collision through the kernel, by EVALUATION rather than type-checking, in `the_crt_self_map_permutes_a_coprime_block_and_collides_on_a_non_coprime_one` -- necessary because the map is a bare lambda and no `Declaration::Definition` gate constrains what it computes.

footprint-Nat.crtSelfMap_injectiveOn

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the Nat prelude's trusted surface is empty, which bounds this theorem.

Checker command

cargo run -q -p axeyum-lean-kernel --example nat_axiom_inventory -- --require-axiom-free nat

Evidence notes

`--require-axiom-free` exits non-zero when the named prelude's trusted surface (Axiom + Opaque + Quotient, not `Axiom` alone -- `Opaque` has no proof body and `Quotient` admits `Quot.sound`) is non-empty, and errors rather than passing silently for a prelude the run never built. A declaration cannot depend on a trusted declaration the environment does not contain, so an empty nat surface bounds every declaration in it.

Provenance

{
  "date": "2026-08-30",
  "established_by": "axeyum-lean-kernel nat_prelude::totient_mul (totient-mul-finish lane)",
  "source": "the remaining piece named by docs/plan/status/344-countrange-bijection.md; statement authored here",
  "prior_art": [
    {
      "who": "Sun Tzu / Qin Jiushao",
      "what": "the Chinese Remainder Theorem's uniqueness half, of which this is the bijectivity reading",
      "year": 1247,
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}