How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Finite Abelian Characters for Combinatorics — Examples
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Binary Operations, Monoids, Groups and Subgroups
- Chain Conditions, Semisimple Modules and the Wedderburn–Artin Theorem
- Characters and the Orthogonality Relations
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Composition Series, the Jordan–Hölder Theorem and Solvable Groups
- Congruences, the Integers Modulo n and the Chinese Remainder Theorem
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Determinants of Matrices over a Commutative Ring
- Diagonalisation and the Minimal Polynomial
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Eigenvalues, Eigenvectors and the Characteristic Polynomial
- Filters and Ultrafilters
- Finite Abelian Characters for Combinatorics
- Finite Averaging and Character-Theory Prerequisites
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Free Modules, Exact Sequences, Projective and Injective Modules
- Fundamental Trigonometric Identities
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Maschke's Theorem, Complete Reducibility and the Structure of k[G]
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Metric Spaces
- Modules, Submodules, Quotient Modules and the Isomorphism Theorems
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Properties of the Integral and the Working FTC
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Simple Field Extensions and the Construction of the Complex Numbers
- Sine, Cosine, and the Definition of Pi
- Suprema and Infima
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- Tensor Products of Modules
- The Complex Exponential and Euler's Formula
- The Derivative and the Mean Value Theorems
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Exponential Function
- The Group Algebra and Representations of Finite Groups
- The Riemann Integral: Definition and Integrability
- The ZFC Axioms and the Basic Set Constructions
- Topology of ℝ
- Triangularisation, Generalised Eigenspaces and Jordan Canonical Form
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
The companion page defines additive characters of a finite abelian group, identifies them with the characters of one-dimensional complex representations, and proves their row orthogonality in the normalized form. This example carries that interface out in coordinates for the cyclic group of order five.
With , the five additive characters of are for . The verification checks that the formula is independent of the chosen representative of a class, that each is multiplicative, that the five functions are pairwise distinct, and that every additive character of the group is determined by its value at and is therefore one of them. The character table is then written out row by row, and the orthogonality relation is both quoted from the companion page and checked directly: the off-diagonal entry for against the trivial character is the vanishing sum of the five fifth roots of unity, and the diagonal entries are all .
The example is a leaf: it requires only its companion page and no later page cites it.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
The five characters of Z/5Z and their orthogonality
Example
Put (The complex exponential by its power series). For and a class with representative (The congruence class and the quotient set ), put The five functions are exactly the additive characters (Additive characters of a finite abelian group) of , their character table has entries , and the entries satisfy
Facts & Assumptions
Given: The group and .
An additive character is a group homomorphism , so and (Additive characters of a finite abelian group).
Additive characters of a finite abelian group are exactly its irreducible complex characters: each is the trace character of a one-dimensional irreducible representation, every irreducible representation arises this way up to equivalence, all values have modulus one, and distinct additive characters give inequivalent representations (Additive characters are exactly one-dimensional complex representation characters).
Row orthogonality: for a finite abelian group and additive characters of , equals when and otherwise (Row orthogonality for additive characters of a finite abelian group).
In classes satisfy exactly when (The congruence class and the quotient set ); the map is a bijection from onto , so (For , every class in has one representative with , so ; while is in bijection with ); addition is given by , independently of representatives (Addition and multiplication on by and ), and makes an abelian group with identity (For every natural , is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold).
The complex exponential satisfies for all (, and the complex exponential extends the real exponential), and its kernel and fibres are given by and exactly when (, and exactly when ).
The -th roots of unity in are precisely the values with , for (The -th roots of a complex number and the distinct roots of unity for every ), and for every real (, , and ).
For every the sum of all -th roots of unity is (For , the sum of all -th roots of unity is zero).
Complex conjugation is an involutive real-field automorphism; it fixes , and for every one has with , while (Conjugation is an involutive real-field automorphism, , and modulus is definite, multiplicative, and subadditive).
Verification
Compute : iterating the addition law [L5] gives , because ; and , since otherwise would give , which is false. So is a fifth root of unity different from , and by [L6] the fifth roots of unity are exactly the five distinct values , .
Well-definedness. Suppose in , so by [L4]; write with . Then the integer power laws together with give , so the prescription does not depend on the chosen representative and defines a function for each .
The five are distinct and exhaustive. If , evaluating at gives , that is , and [L5] gives , so ; as this forces . Conversely let be any additive character and put ; five applications of multiplicativity in [L1], together with in [L4], give , so is a fifth root of unity and by step 1.1 there is a unique with . For one has , whence ; therefore , and every additive character of occurs among the five.
Each is an additive character. By [L4], , so ; every value is one of the fifth roots of unity listed in step 1.1 and hence nonzero. So is a group homomorphism, that is, an additive character of , by [L1].
The table and its orthogonality. By [L2] the five additive characters are exactly the irreducible complex characters of , so the array of values is the character table of the group: its rows, for , are , , , and . By [L4] the group has order and its five elements are , so row orthogonality [L3] applied to and gives exactly . As a direct check of an off-diagonal entry, for and the summands are , and by [L7], since step 1.1 lists as the five fifth roots of unity; on the diagonal by [L6] and [L8], so each diagonal average is .
Steps 2.1 and 3.1 show that each is a well-defined additive character, step 2.2 that they are pairwise distinct and are all of them, and step 3.2 computes the table and verifies its orthogonality; this proves every claim of the example.