Regular Ledger Collision

Abstract

A regular and a trivial graded rational representation have equal formal-log histories on one conjugacy class.

Theorem 1.1 (Determinant of a cyclic permutation).

$$\begin{array}{r}\forall r\in \mathbb{N},0<r\Rightarrow \\ \det \left(I-X{P}_r\right)=1-X^r\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Dilation/ActualRegularLedgerCollision.single_cycle_det (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every positive cycle length r, the determinant of the identity minus X times the matrix of the cyclic rotation of Fin r is 1-X^r over the rational polynomial ring. The proof replaces the final row by a weighted sum of all rows. The resulting matrix is upper triangular, with final diagonal entry 1-X^r; the same calculation includes a one-element cycle.

Theorem 1.2 (Collision of actual graded representations).

$$\begin{array}{r}G\in \mathrm{FiniteGroup}\left(\right),g\in G,\\ r=\mathrm{ord}\left(g\right),1<r,N=\mathrm{card}\left(G\right),c=\frac{N}{r},0<c\\ A_{1,1}=\mathrm{regular}\left(G\right),B_{r,r}=\mathrm{trivial}\left(c\right)\\ \mathrm{support}\left(A\right)=\mathrm{singleton}\left(\mathrm{pair}\left(1,1\right)\right),\mathrm{support}\left(B\right)=\mathrm{singleton}\left(\mathrm{pair}\left(r,r\right)\right)\\ H_A=\mathrm{traceSeries}\left(A\right),H_B=\mathrm{traceSeries}\left(B\right)\\ \exists D,\\ \forall h\in \mathrm{Conj}\left(g\right),\\ \mathrm{detRegular}\left(h,X\right)={1-X^r}^c,\mathrm{detTrivial}\left(h,X^r\right)={1-X^r}^c\\ D=\mathrm{substitute}\left({1-X^r}^c,pq\right),\mathrm{negativeLog}\left(D\right)=\mathrm{Phi}\left(H_A,h\right),\mathrm{negativeLog}\left(D\right)=\mathrm{Phi}\left(H_B,h\right)\\ \mathrm{Phi}\left(H_A,h\right)=\mathrm{Phi}\left(H_B,h\right),\mathrm{coeff}\left(H_A,r,r\right)=0\ne c=\mathrm{coeff}\left(H_B,r,r\right)\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Dilation/ActualRegularLedgerCollision.actual_ledger_collision (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let G be a finite group and let g have order r greater than one. Write N for the cardinality of G and c=N/r, which is positive. The rational G-representation A has the left regular module Q[G] in bidegree (1,1) and the zero module in every other bidegree. B has c copies of the trivial rational representation in bidegree (r,r) and the zero module elsewhere. At every bidegree, the coefficients of H_A and H_B equal the characters of these ledger entries; the PUnit zero modules have trace zero.

For every h conjugate to g, left multiplication on G has c cycles of length r. Reindexing by right cosets of the subgroup generated by h gives the determinant (1-X^r)^c on Q[G]. The trivial action on Q^c gives the same determinant when weighted by X^r. Substitution X=pq defines a bivariate denominator with constant coefficient one from either actual determinant.

Its negative formal logarithm is the entire class-indexed logarithmic history of both trace series at h, including zero and off-diagonal coefficients. The raw coefficient in bidegree (r,r) is zero for A and c for B. The assertion concerns only conjugates of g; it gives no equality at every group element or every power and makes no claim about a Monster root space or a vertex algebra.

References

• Truth anchor: D5/S3/Analytic/Dilation/ActualRegularLedgerCollision.actual_ledger_collision
• Truth anchor: D5/S3/Analytic/Dilation/ActualRegularLedgerCollision.single_cycle_det
• Dependency: D5/S3/Analytic/Dilation/EquivariantSeriesObserver
• Dependency: D5/S3/Analytic/Dilation/MonsterPrimitiveMobiusRecovery