Attaining permutation algebras

Abstract

Coefficient-one permutation evolution algebras realize the complete root kernel and permutation centralizer.

Definition 1.1 (The coordinate permutation).

$$\forall n\in \mathbb{N},\forall sigma\in \mathrm{Perm}\left(\mathrm{Fin}\left(n\right)\right),\forall x\in \mathrm{Coord}\left(n\right),\forall j\in \mathrm{Fin}\left(n\right),\mathrm{coordinate}\left(\mathrm{apply}\left(\mathrm{permutationLinear}\left(sigma\right),x\right),j\right)=\mathrm{coordinate}\left(x,\mathrm{inverseApply}\left(sigma,j\right)\right)$$

Formalization. D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionPermutationFamily.permutationLinear (✓ std3).

Source. Repository-derived.

Commentary.

The linear equivalence P_sigma sends coordinate vector e_i to e_(sigma(i)); its j-th output coordinate is x_(sigma inverse(j)).

Definition 1.2 (The bilinear evolution law).

$$\forall n\in \mathbb{N},\forall sigma\in \mathrm{Perm}\left(\mathrm{Fin}\left(n\right)\right),\forall x\in \mathrm{Coord}\left(n\right),\forall y\in \mathrm{Coord}\left(n\right),\mathrm{ApplyProduct}\left(\mathrm{permutationProduct}\left(sigma\right),x,y\right)=\mathrm{apply}\left(\mathrm{permutationLinear}\left(sigma\right),x\cdot y\right)$$

Formalization. D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionPermutationFamily.permutationProduct (✓ std3).

Citation. Ivan Kaygorodov; Cándido Martín González; Antonio Viruel (2026). Evolution algebras: a survey of results and a list of open problems. DOI: 10.48550/arXiv.2610.22248. URL: https://arxiv.org/abs/2610.22248v1.

Commentary.

The product is P_sigma applied to coordinatewise multiplication. The original coordinateProduct construction supplies bilinearity. Its basis squares are e_i squared=e_(sigma(i)) and distinct basis vectors multiply to zero. The structure map is invertible, so all pair products span the whole space.

Theorem 1.3 (The image of each coordinate basis vector).

$$\forall n\in \mathbb{N},\forall sigma\in \mathrm{Perm}\left(\mathrm{Fin}\left(n\right)\right),\forall i\in \mathrm{Fin}\left(n\right),\mathrm{permutationLinear}\left(sigma\right)\left(\mathrm{Pi}.\mathrm{basisFun}\left(Complex,\mathrm{Fin}\left(n\right)\right)\left(i\right)\right)=\mathrm{Pi}.\mathrm{basisFun}\left(Complex,\mathrm{Fin}\left(n\right)\right)\left(sigma\left(i\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionPermutationFamily.permutationLinear_basis (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every n, permutation sigma and index i, permutationLinear sigma sends Pi.basisFun at i to Pi.basisFun at sigma(i). This identity identifies the support permutation of explicit automorphisms.

Theorem 1.4 (Products of distinct basis vectors vanish).

$$\forall n\in \mathbb{N},\forall sigma\in \mathrm{Perm}\left(\mathrm{Fin}\left(n\right)\right),\forall i\in \mathrm{Fin}\left(n\right),\forall j\in \mathrm{Fin}\left(n\right),i\ne j\Rightarrow \mathrm{permutationProduct}\left(sigma\right)\left(\mathrm{Pi}.\mathrm{basisFun}\left(Complex,\mathrm{Fin}\left(n\right)\right)\left(i\right),\mathrm{Pi}.\mathrm{basisFun}\left(Complex,\mathrm{Fin}\left(n\right)\right)\left(j\right)\right)=0$$

Proof. Machine-checked in Lean as D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionPermutationFamily.permutation_mixed (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every n, permutation sigma and distinct i,j in Fin n, permutationProduct sigma applied to the two coordinate basis vectors is zero. This supplies the natural basis for the cyclic algebras.

Theorem 1.5 (The exact support relation).

$$\forall n\in \mathbb{N},\forall sigma\in \mathrm{Perm}\left(\mathrm{Fin}\left(n\right)\right),\forall i\in \mathrm{Fin}\left(n\right),\forall j\in \mathrm{Fin}\left(n\right),\mathrm{supportRelation}\left(\mathrm{permutationProduct}\left(sigma\right),\mathrm{Pi}.\mathrm{basisFun}\left(Complex,\mathrm{Fin}\left(n\right)\right),i,j\right)\iff j=sigma\left(i\right)$$

Proof. Machine-checked in Lean as D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionPermutationFamily.permutation_support (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every n, permutation sigma and indices i,j, the supportRelation of permutationProduct sigma in Pi.basisFun has an arrow from i to j exactly when j=sigma(i). The cyclic family uses this to establish strong connectivity.

Definition 1.6 (Every commuting permutation lifts).

$$\forall n\in \mathbb{N},\forall sigma\in \mathrm{Perm}\left(\mathrm{Fin}\left(n\right)\right),\forall tau\in \mathrm{centralizer}\left(sigma\right),\mathrm{Member}\left(\mathrm{centralizerLift}\left(sigma,tau\right),\mathrm{Aut}\left(\mathrm{permutationProduct}\left(sigma\right)\right)\right)$$

Formalization. D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionPermutationFamily.centralizerLift (✓ std3).

Citation. Ivan Kaygorodov; Cándido Martín González; Antonio Viruel (2026). Evolution algebras: a survey of results and a list of open problems. DOI: 10.48550/arXiv.2610.22248. URL: https://arxiv.org/abs/2610.22248v1.

Commentary.

For each tau commuting with sigma, P_tau preserves the product on all vector pairs. It is therefore an actual member of the full LinearEquiv automorphism group. Its support permutation is tau itself. These explicit lifts prove equality of the actual projection image and the full centralizer.

Theorem 1.7 (Exact full-group cardinality).

$$\forall n\in \mathbb{N},\forall sigma\in \mathrm{Perm}\left(\mathrm{Fin}\left(n\right)\right),\mathrm{Finite}\left(\mathrm{Aut}\left(\mathrm{permutationProduct}\left(sigma\right)\right)\right)\wedge \mathrm{NatCard}\left(\mathrm{Aut}\left(\mathrm{permutationProduct}\left(sigma\right)\right)\right)=\mathrm{weight}\left(\mathrm{parts}\left(\mathrm{partition}\left(sigma\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionPermutationFamily.permutation_aut_card (✓ std3). ∎

Citation. Ivan Kaygorodov; Cándido Martín González; Antonio Viruel (2026). Evolution algebras: a survey of results and a list of open problems. DOI: 10.48550/arXiv.2610.22248. URL: https://arxiv.org/abs/2610.22248v1.

Commentary.

The entire algebra group is finite. Monomiality identifies its actual permutation image; preservation of basis squares forces that image to commute with sigma, and the lifts prove the converse inclusion. The actual kernel is exactly the unit assignments a_(sigma(i))=a_i squared. Existing independent cycle-root realization counts it, including the singleton root factor one. Kernel cardinality times image cardinality is therefore the full partition weight, with every singleton multiplicity factorial retained. The source states attainment by sums of cyclic algebras; this proof derives the exact cardinality directly without assuming a wreath-product classification.

Theorem 1.8 (All algebraic witness conditions).

$$\forall n\in \mathbb{N},\forall sigma\in \mathrm{Perm}\left(\mathrm{Fin}\left(n\right)\right),\mathrm{commutative}\left(\mathrm{permutationProduct}\left(sigma\right)\right)\wedge \left(\mathrm{hasNaturalBasis}\left(\mathrm{permutationProduct}\left(sigma\right)\right)\wedge \left(\mathrm{perfect}\left(\mathrm{permutationProduct}\left(sigma\right)\right)\wedge \left(\mathrm{Finite}\left(\mathrm{Aut}\left(\mathrm{permutationProduct}\left(sigma\right)\right)\right)\wedge \mathrm{NatCard}\left(\mathrm{Aut}\left(\mathrm{permutationProduct}\left(sigma\right)\right)\right)=\mathrm{weight}\left(\mathrm{parts}\left(\mathrm{partition}\left(sigma\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionPermutationFamily.permutation_family (✓ std3). ∎

Citation. Ivan Kaygorodov; Cándido Martín González; Antonio Viruel (2026). Evolution algebras: a survey of results and a list of open problems. DOI: 10.48550/arXiv.2610.22248. URL: https://arxiv.org/abs/2610.22248v1.

Commentary.

Every permutation gives a commutative, perfect complex evolution algebra on Fin(n) to C. It need not be associative. Naturality and perfection use the original coordinate-product facts. The same actual algebra and same full automorphism group satisfy the exact order formula.

References

• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionPermutationFamily.centralizerLift
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionPermutationFamily.permutationLinear
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionPermutationFamily.permutationLinear_basis
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionPermutationFamily.permutationProduct
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionPermutationFamily.permutation_aut_card
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionPermutationFamily.permutation_family
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionPermutationFamily.permutation_mixed
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionPermutationFamily.permutation_support
• Dependency: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionSharpBound
• Dependency: D5/S3/QuadraticForms/EvolutionAlgebras/HuEvolutionJordanFamily