character tables over exact cyclotomic fields, checked by orthogonality, degrees and Galois consistency

Identifier: F:cas-character-tables-verified-over-cyclotomic-fields
Proof route: cas-certificate
External status: proved
Axiom footprint: cas.exact-cyclotomic-field-arithmetic, cas.conjugacy-class-certificate-from-permgroup: condition (1) is delegated to ConjugacyClassCertificate::verify and is not re-derived here, chartable.orthogonality-and-galois-consistency-do-not-imply-representability: this is the module's own stated limit. A table that passes all six conditions is CONSISTENT WITH being the character table of G; it is not proved to be one, because none of the six conditions exhibits a representation. Do not read an accepted table as `the character table of G has been proved correct`., 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

For a finite group G of exponent e, a candidate character table over Q(zeta_e) is accepted only if all six conditions hold, each re-derived from the certificate alone: (1) the conjugacy classes are the classes of the group described by the carried permutation-group order certificate; (2) the table is square on those classes and every entry lies in Q(zeta_e) for the RECOMPUTED exponent e, not a conductor the certificate may pad; (3) row orthogonality, (1/|G|) sum_k |C_k| chi_i(g_k) conj(chi_j(g_k)) = delta_ij; (4) column orthogonality, sum_i chi_i(g_k) conj(chi_i(g_l)) = delta_kl |G| / |C_k|; (5) every degree chi_i(1) is a positive rational integer dividing |G|, and the trivial character occurs exactly once; and (6) Galois consistency, that for every t coprime to e the substitution zeta -> zeta^t sends chi_i(g) to chi_i(g^t). Arithmetic is exact in the power basis modulo the cyclotomic polynomial; no complex floating-point number occurs anywhere. Verified for S_3, S_4, A_4, A_5 (including its golden-ratio entries) and Q_8; produced AND verified for C_4, the Klein four-group, C_6 and a product of two cyclic groups.

Formal statement

{"arithmetic":"exact in Q(zeta_e), power basis modulo the e-th cyclotomic polynomial; no complex floating point","checked_groups":["S3","S4","A4","A5","Q8"],"conjugation":"the Galois substitution zeta -> zeta^(e-1)","does_not_establish":"that each row is the character of an actual representation","format":"axeyum-cas-character-table-certificate","produced_and_checked_groups":["C4","V4","C6","C_m x C_n"],"verify_conditions":["classes-are-the-groups-classes","square-and-in-the-recomputed-field","row-orthogonality","column-orthogonality","integral-degrees-dividing-order-and-one-trivial-character","galois-consistency"],"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-chartable-verification-and-discrimination

Kind: witness-replay
Status: checked

Supports: that the six conditions are each load-bearing -- every one rejects a table forged on exactly its axis -- and in particular that condition (6) catches a defect the orthogonality relations provably cannot

Checker command

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

Evidence notes

28 tests, 11 of them discrimination controls. The A_5 test asserts exactly four irrational entries, so the golden-ratio arithmetic is checked positively and not merely 'did not crash'.

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/chartable.rs (1,615 lines), over permgroup.rs",
  "prior_art": [
    {
      "who": "F. G. Frobenius; I. Schur; W. Burnside; J. D. Dixon",
      "what": "the orthogonality relations for irreducible characters; the Burnside-Dixon algorithm for computing character tables",
      "where": "Frobenius (1896); Dixon, Numerische Mathematik 11 (1968)",
      "attribution": "standard textbook attribution; this lane did not consult the primary sources"
    }
  ]
}