A product over an initial segment collapses to 1 mod p when a fixed-point-free involution pairs each factor with its inverse

Identifier: F:prodrange-collapses-under-a-fixed-point-free-involution
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Let p be a positive integer, F : Nat -> Int, and sigma : Nat -> Nat. If sigma is injective on {0..n-1}, maps that set into itself, has NO fixed point there, is an involution there, and pairs factors into inverses (F k * F (sigma k) = 1 mod p for every k < n), then prodRange F n = 1 mod p. PRIMALITY IS NOT REQUIRED AND IS NOT PRESENT. This is a fact about fixed-point-free involutions over any positive modulus; primality enters only downstream, when sigma := Nat.inverseIndex p is supplied and one has to know the pairing exists at all. THE FIXED-POINT-FREE PREMISE IS LOAD-BEARING: without it sigma = id satisfies injectivity, mapsInto and the involution law, and the pairing premise degenerates to F k * F k = 1, from which prodRange F n = 1 does not follow. Equality of indices is Eq on Nat; the conclusion is Int.ModEq. A NOTE ON `AxNat`, because the name is actively misleading: the `Ax` is `axeyum`, not `axiom`. `lean_pp` roots the kernel's COMPUTATIONAL (inductive, constructed) naturals at `AxNat` for one reason only -- so an exported term does not shadow Lean's own `Nat`. It collides badly with `AxReal`, where `Ax` DOES mean axiomatized and the trusted surface is 30. The `nat` prelude measures 0: no Axiom, no Opaque, no Quotient.

Formal statement

theorem Int.prod_range_pairing_collapse : ((x0 : Int) -> ((x1 : Int.lt Int.zero x0) -> ((x2 : AxNat) -> ((x3 : ((x3 : AxNat) -> Int)) -> ((x4 : ((x4 : AxNat) -> AxNat)) -> ((x5 : AxNat.injectiveOn x4 x2) -> ((x6 : AxNat.mapsInto x4 x2) -> ((x7 : ((x7 : AxNat) -> ((x8 : AxNat.lt x7 x2) -> Not (Eq.{1} AxNat (x4 x7) x7)))) -> ((x8 : ((x8 : AxNat) -> ((x9 : AxNat.lt x8 x2) -> Eq.{1} AxNat (x4 (x4 x8)) x8))) -> ((x9 : ((x9 : AxNat) -> ((x10 : AxNat.lt x9 x2) -> Int.ModEq x0 (Int.mul (x3 x9) (x3 (x4 x9))) Int.one))) -> Int.ModEq x0 (Int.prodRange x3 x2) Int.one))))))))))

Dependencies

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

20 direct dependencies 1 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-Int.prod_range_pairing_collapse

Kind: kernel-term
Status: checked

Supports: `Int.prod_range_pairing_collapse` is admitted with exactly the type in formal.statement. THE INDUCTION IS ORDINARY, AND THAT CORRECTS A PLAN THAT HAD SURVIVED NINE DRAFTS: wilson.rs's module doc sketched strong induction via WellFounded.fix, citing gcd.rs's precedent. It is not needed. The step decreases the domain by exactly 2, so proving `And (family n) (family (succ n))` together by plain Nat.rec suffices. The step conjugates sigma by a two-point transposition. Nat.transposition's helpers are typed concretely over NatDev, so a local IntDev-native copy was built rather than editing a file another lane held; the already-generic conjugate_injective / conjugate_maps_into were reused unchanged.

Checker command

test "$(scripts/cargo-serialized.sh test -p axeyum-lean-kernel --lib int_prelude::int_prelude_tests::the_pairing_collapse_keeps_its_fixed_point_free_premise -- --exact 2>&1 | grep -Ec 'test result: ok\. 1 passed; 0 failed')" -ge 1

Evidence notes

A footprint check cannot carry this claim, and here the difference is soundness rather than strength: the SAME theorem with the fixed-point-free premise deleted is FALSE at sigma = id, and it would have an identically empty footprint. Mutation-verified 2026-08-24: deleting that premise from the pinned string makes cargo report `578 passed; 1 failed`, naming this test and no other; restored, 579/579 green. The command is anchored on the exact `1 passed; 0 failed` count so an unmatched filter -- which prints `running 0 tests ... ok` and exits 0 -- cannot read as success.

footprint-int-pairing-collapse

Kind: kernel-term
Status: checked

Supports: axiom_footprint: [] for prod_range_pairing_collapse and everything beneath it. The `integer` prelude's trusted surface is 0. The name was added to the derived-laws sweep in the SAME edit that declared it, moving its pinned size annotation 108 -> 109.

Checker command

test "$(scripts/cargo-serialized.sh test -p axeyum-lean-kernel --lib int_prelude::int_prelude_tests::derived_laws_have_no_axiom_footprint -- --exact 2>&1 | grep -Ec 'test result: ok\. 1 passed; 0 failed')" -ge 1

Evidence notes

The size annotation on the derived-laws array is what makes presence checkable: axiom_footprint of a name interned but never DECLARED is vacuously empty, so a sweep that merely iterates whatever is in the array cannot detect an omission. Declaration::Axiom alone would also not suffice in this kernel -- Opaque has no proof body and Quotient admits Quot.sound -- which is why axiom_footprint, covering all three, is what is read.

Provenance

{
  "date": "2026-08-24",
  "established_by": "lane agent-capability-assurance (2026-08-24). Seven lanes narrowed to this statement: Int.prodRange_permute removes ONE index per step at the SAME domain size, so unwound it reconstructs the product from itself -- which is why ((p-1)!)^2 = 1 mod p came free and the SIGN did not. This lemma removes a matched PAIR and carries the information. Statement pin and its mutation control added by the coordinating lane.",
  "source": "classical",
  "prior_art": [
    {
      "who": "standard",
      "what": "the pairing argument underlying Wilson's theorem",
      "year": 1771,
      "where": "conventionally attributed to Lagrange's first proof of Wilson's theorem",
      "attribution": "standard attribution; this lane did not consult the primary source. The lemma isolated here is the combinatorial core, stated for an arbitrary fixed-point-free involution rather than for the inverse map of a prime residue system."
    }
  ]
}