finite matrix groups over F_p and over Q: orders, isomorphism types, and a decided finiteness question

Identifier: F:cas-matrix-groups-orders-and-isomorphisms
Proof route: cas-certificate
External status: proved
Axiom footprint: cas.exact-modular-and-rational-matrix-arithmetic, cas.schreier-sims-permutation-group-order: the group order is delegated to axeyum_cas::permgroup, whose own correctness is CAS-internal and is not re-derived by the matrix-group certificate, minkowski-lemma-for-odd-primes-as-implemented: the p >= 3 torsion-freeness argument is stated and used by this module; -I breaks it at p = 2, which the module handles by excluding p = 2 rather than by proving the exclusion sound elsewhere, cas.verifier-shares-the-crate-with-the-producer: the certificate checker re-derives every step from the recorded (head, inputs, order) and trusts no recorded number, but it lives in the same crate as the search that produced the certificate, so under ADR-0601 SS1 this is `cas-internal` evidence and NOT reconstruction through the one trust anchor (Kernel::add_declaration). That is why this fact is `computed` and not `proved`.

Recorded description

Over a prime field F_p, a matrix group given by generators acts faithfully on the nonzero vectors of F_p^n (so the permutation group's order IS the matrix group's order) or projectively on the points of P^(n-1)(F_p) (whose kernel is exactly the scalars, so SL generators yield PSL without constructing a quotient). Computed and independently re-verified: |GL(2,F_3)| = 48, |SL(2,F_3)| = 24, |GL(2,F_5)| = 480, |SL(2,F_5)| = 120, |GL(3,F_2)| = 168, |PSL(2,F_5)| = 60, |PSL(2,F_7)| = 168; and as isomorphism types PSL(2,F_5) = A_5 and PSL(2,F_7) = GL(3,F_2), while SL(2,F_3) is NOT isomorphic to the dihedral group of order 24 (a negative control between two groups of the same order). Over Q, finiteness of a matrix group is DECIDED, with a certificate for either verdict: by Minkowski's lemma the reduction mod an odd prime of good reduction is injective on torsion, so the mod-p order N bounds the rational closure -- closing at exactly N gives the order, and producing an (N+1)-st distinct element is a proof of infiniteness. Two cheaper infiniteness routes need no prime at all: |trace| > n and |det| != 1 each force infinite order.

Formal statement

{"actions":["vector on nonzero vectors of F_p^n (faithful)","projective on points of P^(n-1)(F_p) (kernel = scalars)"],"finite_field_orders":{"GL(2,3)":48,"GL(2,5)":480,"GL(3,2)":168,"PSL(2,5)":60,"PSL(2,7)":168,"SL(2,3)":24,"SL(2,5)":120},"format":"axeyum-cas-matrix-group-certificate","infinite_routes":["MinkowskiOverflow","TraceExceedsDimension","DeterminantNotUnit"],"isomorphisms":["PSL(2,5) = A5","PSL(2,7) = GL(3,2)"],"minkowski_bound":[1,2,24,48,5760,11520,2903040],"non_isomorphism":"SL(2,3) != D12 (both of order 24)","rational_route":"Minkowski reduction mod an odd prime of good reduction","version":1}

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

cas-matgroup-finite-field-orders-and-isomorphisms

Kind: witness-replay
Status: checked

Supports: the seven computed orders, the two isomorphisms, and the one non-isomorphism, each re-derived by a certificate verifier that re-enumerates the action from (p, n, action) alone

Checker command

cargo test -p axeyum-cas --lib matgroup::tests

Evidence notes

26 tests. The negative control matters: two groups of order 24 that are not isomorphic is the case an order-only check cannot distinguish.

cas-matgroup-rational-finiteness-decision

Kind: witness-replay
Status: checked

Supports: that finiteness over Q is decided with a certificate for BOTH verdicts, and that the infiniteness verdicts are proofs rather than timeouts

Checker command

cargo test -p axeyum-cas --lib matgroup_q::tests

Evidence notes

35 tests. Halting below the mod-p order N is reported as MinkowskiContradiction -- a declared bug -- never as a smaller order. That is the design choice that keeps a wrong answer from being expressible.

Provenance

{
  "date": "2026-09-06",
  "established_by": "lane ledger-coverage (ADR-1674): registered from the existing axeyum-cas implementation and its own certificate verifiers; no new mathematics was produced by this lane",
  "source": "crates/axeyum-cas/src/matgroup.rs (1,469 lines) and matgroup_q.rs (1,692 lines), over permgroup.rs",
  "prior_art": [
    {
      "who": "H. Minkowski; C. Sims",
      "what": "Minkowski's lemma bounding the order of a finite subgroup of GL(n,Q); the Schreier-Sims algorithm for permutation-group order",
      "where": "Minkowski (1887); Sims, in Computational Problems in Abstract Algebra (1970)",
      "attribution": "standard textbook attribution; this lane did not consult the primary sources"
    },
    {
      "who": "classical",
      "what": "the exceptional isomorphisms PSL(2,5) = A_5 and PSL(2,7) = GL(3,2)",
      "where": "standard; see e.g. Dummit and Foote, Abstract Algebra",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}