Basis transport and the full algebra group

Abstract

All multiplication automorphisms of an arbitrary finite-dimensional perfect complex evolution algebra obey joint cycle, quotient and block control.

A and B are complex vector spaces with bilinear multiplication mu. Neither associativity nor a multiplicative unit is required. productSpan(mu) is the span of every mu(x,y); perfection means productSpan(mu)=Top. The automorphism group is the single Aut definition of EvolutionAutomorphismControl: all complex LinearEquivs preserving every pair product.

Definition 1.1 (Transporting the multiplication).

$$\forall A\in Typeu,\forall B\in Typeu,\mathrm{ComplexVectorSpace}\left(A\right)\Rightarrow \left(\mathrm{ComplexVectorSpace}\left(B\right)\Rightarrow \left(\forall e\in \mathrm{LinearEquiv}\left(A,B\right),\forall mu\in \mathrm{BilinearProduct}\left(A\right),\forall x\in B,\forall y\in B,\mathrm{ApplyProduct}\left(\mathrm{transportProduct}\left(e,mu\right),x,y\right)=e\left(\mathrm{ApplyProduct}\left(mu,\mathrm{inverse}\left(e,x\right),\mathrm{inverse}\left(e,y\right)\right)\right)\right)\right)$$

Formalization. D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionBasisTransport.transportProduct (✓ std3).

Source. Repository-derived.

Commentary.

For x,y in B, the transported multiplication is e(mu(e inverse(x),e inverse(y))). Bilinearity follows from composition of linear maps.

Theorem 1.2 (Exact product-span correspondence).

$$\forall A\in Typeu,\forall B\in Typeu,\mathrm{ComplexVectorSpace}\left(A\right)\Rightarrow \left(\mathrm{ComplexVectorSpace}\left(B\right)\Rightarrow \left(\forall e\in \mathrm{LinearEquiv}\left(A,B\right),\forall mu\in \mathrm{BilinearProduct}\left(A\right),\mathrm{map}\left(e,\mathrm{productSpan}\left(mu\right)\right)=\mathrm{productSpan}\left(\mathrm{transportProduct}\left(e,mu\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The image under e of the span of all pair products is exactly the span of all transported pair products. Surjectivity of e supplies the reverse inclusion. Since e has zero kernel and full range, perfection is equivalent on the two spaces.

Definition 1.3 (Conjugacy of the entire automorphism group).

$$\forall A\in Typeu,\forall B\in Typeu,\mathrm{ComplexVectorSpace}\left(A\right)\Rightarrow \left(\mathrm{ComplexVectorSpace}\left(B\right)\Rightarrow \left(\forall e\in \mathrm{LinearEquiv}\left(A,B\right),\forall mu\in \mathrm{BilinearProduct}\left(A\right),\mathrm{GroupEquiv}\left(\mathrm{Aut}\left(mu\right),\mathrm{Aut}\left(\mathrm{transportProduct}\left(e,mu\right)\right)\right)\right)\right)$$

Formalization. D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionBasisTransport.automorphismConjugacy (✓ std3).

Source. Repository-derived.

Commentary.

The map sends f to e composed with f composed with e inverse. Its inverse conjugates by e inverse. Both maps preserve multiplication because the transported product is defined on all pairs. They are inverse group homomorphisms; no monomiality, support lift, finiteness or conjugacy premise is inserted.

Theorem 1.4 (The natural-basis correspondence).

$$\forall A\in Typeu,\mathrm{ComplexVectorSpace}\left(A\right)\Rightarrow \left(\forall n\in NaturalNumbers,\forall mu\in \mathrm{BilinearProduct}\left(A\right),\forall b\in \mathrm{Basis}\left(\mathrm{Fin}\left(n\right),Complex,A\right),\left(\mathrm{NaturalBasisAt}\left(mu,b\right)\Rightarrow \mathrm{CoordinateBasisNatural}\left(mu,b\right)\right)\wedge \left(\mathrm{CoordinateBasisNatural}\left(mu,b\right)\Rightarrow \mathrm{NaturalBasisAt}\left(mu,b\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The equivalence b.equivFun sends b(i) to the i-th coordinate vector. Products of distinct basis vectors therefore vanish exactly when products of the corresponding coordinate basis vectors vanish.

Definition 1.5 (The finite-index bridge).

$$\forall A\in Typeu,\mathrm{FiniteDimensionalComplexVectorSpace}\left(A\right)\Rightarrow \left(\forall I\in Typeu,\mathrm{Fintype}\left(I\right)\Rightarrow \left(\forall n\in \mathrm{NaturalNumbers}\left(\right),\mathrm{finrank}\left(A\right)=n\Rightarrow \left(\forall b\in \mathrm{Basis}\left(I,Complex,A\right),\mathrm{Basis}\left(\mathrm{Fin}\left(n\right),Complex,A\right)\right)\right)\right)$$

Formalization. D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionBasisTransport.dimensionBasis (✓ std3).

Source. Repository-derived.

Commentary.

For any finite index type I and any basis b indexed by I, finrank equals card(I). Given finrank(A)=n, Fintype.equivFinOfCardEq and Basis.reindex produce the n-indexed basis. Its naturality follows by injectivity of the index equivalence. Thus the original natural basis is arbitrary, and the n-dimensional source quantifier is retained.

Theorem 1.6 (Reindexing preserves zero mixed products).

$$\forall A\in \mathrm{Type},[\mathrm{AddCommGroup}\left(A\right)][\mathrm{Module}\left(Complex,A\right)][\mathrm{FiniteDimensional}\left(Complex,A\right)]\forall I\in \mathrm{Type},[\mathrm{Fintype}\left(I\right)]\forall n\in Nat,\forall hn\in \mathrm{Module}.\mathrm{finrank}\left(Complex,A\right)=n,\forall mu\in \mathrm{LinearMap}\left(Complex,A,\mathrm{LinearMap}\left(Complex,A,A\right)\right),\forall b\in \mathrm{Module}.\mathrm{Basis}\left(I,Complex,A\right),\left(\forall i\in I,\forall j\in I,i\ne j\Rightarrow mu\left(b\left(i\right),b\left(j\right)\right)=0\right)\Rightarrow \left(\forall i\in \mathrm{Fin}\left(n\right),\forall j\in \mathrm{Fin}\left(n\right),i\ne j\Rightarrow mu\left(\mathrm{dimensionBasis}\left(hn,b\right)\left(i\right),\mathrm{dimensionBasis}\left(hn,b\right)\left(j\right)\right)=0\right)$$

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

Source. Repository-derived.

Commentary.

Let A be a finite-dimensional complex vector space, I a finite index type, hn an equality finrank(A)=n, mu a bilinear product and b an I-indexed basis. If mu(b(i),b(j))=0 for distinct I-indices, the same is true of dimensionBasis hn b for distinct Fin n indices. Injectivity of the reindexing equivalence preserves distinctness. The arbitrary-module automorphism bound uses this to apply the coordinate theorem.

Theorem 1.7 (Joint control on the actual algebra group).

$$\forall A\in Typeu,\mathrm{FiniteDimensionalComplexVectorSpace}\left(A\right)\Rightarrow \left(\forall I\in Typeu,\mathrm{Fintype}\left(I\right)\Rightarrow \left(\forall n\in \mathrm{NaturalNumbers}\left(\right),\mathrm{finrank}\left(A\right)=n\Rightarrow \left(\forall mu\in \mathrm{BilinearProduct}\left(A\right),\forall b\in \mathrm{Basis}\left(I,Complex,A\right),\mathrm{NaturalBasisAt}\left(mu,b\right)\Rightarrow \left(\mathrm{productSpan}\left(mu\right)=Top\Rightarrow \left(\mathrm{Finite}\left(\mathrm{Aut}\left(mu\right)\right)\wedge \mathrm{card}\left(\mathrm{Aut}\left(mu\right)\right)\le \mathrm{cycleWeight}\left(\mathrm{beta}\left(\mathrm{SupportOfCoordinateProduct}\left(mu,b,n\right)\right)\right)\cdot \mathrm{card}\left(\mathrm{centralizer}\left(\mathrm{beta}\left(\mathrm{SupportOfCoordinateProduct}\left(mu,b,n\right)\right)\right)\right)\cdot \mathrm{BlockFactorialProduct}\left(\mathrm{SupportOfCoordinateProduct}\left(mu,b,n\right)\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

First transport along the reindexed basis and prove coordinate perfection and naturality. The coordinate algebra group is finite, and the group conjugacy transfers that actual finiteness before Nat.card is used. Let R be the support of the transported product, P its least successor-compatible quotient, beta the induced permutation, and B_q the original vertices in quotient class q. The bound is product_c(2^card(c)-1) times card(centralizer_Sym(P)(beta)) times product_q(card(B_q)!). The cycles c partition P, not the n original vertices. Singleton cycles contribute one. Exact diagonal assignment descent and cycle-root realization supply the first factor. The actual kernel of the block action injects into the product of the symmetric groups of B_q; it may be nontrivial. No support-surjectivity or faithful quotient-action hypothesis is used. The neutral n=0 case is included.

This joint control concerns the full source family in Conjecture 3 of Kaygorodov, Martín González and Viruel, arXiv:2610.22248v1. It does not assert the conjecture’s sharp maximum or attainment. The partition maximum, six small dimensions, factorial tail and absorption, coefficient-one cyclic-family attainment, and final upper-bound-plus-attainment assembly remain further mathematical requirements.

References

• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionBasisTransport.automorphismConjugacy
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionBasisTransport.dimensionBasis
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionBasisTransport.dimensionBasis_natural
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionBasisTransport.finite_and_joint_bound
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionBasisTransport.natural_basis_transport_iff
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionBasisTransport.product_span_transport
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionBasisTransport.transportProduct
• Dependency: D5/S3/QuadraticForms/EvolutionAlgebras/EvolutionAutomorphismControl