An ordinary nilpotency index outside the proposed binary spectrum

Abstract

An ordinary nilpotency index outside the proposed binary spectrum.

Definition 1.1 (productSpace).

$$\forall K\in \mathrm{Type},[\mathrm{Field}\left(K\right)]\forall V\in \mathrm{Type},[\mathrm{AddCommGroup}\left(V\right)][\mathrm{Module}\left(K,V\right)]\forall mu\in \mathrm{LinearMap}\left(K,V,\mathrm{LinearMap}\left(K,V,V\right)\right),\forall U\in \mathrm{Submodule}\left(K,V\right),\forall W\in \mathrm{Submodule}\left(K,V\right),\mathrm{productSpace}\left(mu,U,W\right)=\mathrm{span}\left(K,\{z:V\mid \exists x\in V,\mathrm{mem}\left(x,U\right)\wedge \left(\exists y\in V,\mathrm{mem}\left(y,W\right)\wedge mu\left(x,y\right)=z\right)\}\right)$$

Formalization. D5/S3/QuadraticForms/EvolutionAlgebras/NilpotencySpectrumRefutation.productSpace (✓ std3).

Source. Repository-derived.

Acknowledgement. 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 of two subspaces is the linear span of all products of their elements. Multiplication is bilinear; associativity is not assumed.

Definition 1.2 (ordinaryPower).

$$\forall K\in \mathrm{Type},[\mathrm{Field}\left(K\right)]\forall V\in \mathrm{Type},[\mathrm{AddCommGroup}\left(V\right)][\mathrm{Module}\left(K,V\right)]\forall mu\in \mathrm{LinearMap}\left(K,V,\mathrm{LinearMap}\left(K,V,V\right)\right),\mathrm{ordinaryPower}\left(mu,0\right)=\mathrm{bot}\wedge \left(\mathrm{ordinaryPower}\left(mu,1\right)=\mathrm{top}\wedge \left(\forall n\in \mathbb{N},\mathrm{ordinaryPower}\left(mu,n+2\right)=\mathrm{iSup}\left(\mathrm{fun}(i:\mathrm{Fin}\left(n+1\right))\mapsto \mathrm{productSpace}\left(mu,\mathrm{ordinaryPower}\left(mu,\mathrm{val}\left(i\right)+1\right),\mathrm{ordinaryPower}\left(mu,n+1-\mathrm{val}\left(i\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S3/QuadraticForms/EvolutionAlgebras/NilpotencySpectrumRefutation.ordinaryPower (✓ 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 degree n+2 the supremum runs over i from 0 through n. Thus it contains every split into the positive degrees i+1 and n+1-i. This is the ordinary lower series in section 1.1, including every parenthesization. The zeroth power is unused for positive k.

Definition 1.3 (indexExists).

$$\forall K\in \mathrm{Type},[\mathrm{Field}\left(K\right)]\forall n\in \mathbb{N},\forall k\in \mathbb{N},\mathrm{indexExists}\left(K,n,k\right)=\left(\exists V\in \mathrm{Type},\exists [\mathrm{AddCommGroup}\left(V\right)],\exists [\mathrm{Module}\left(K,V\right)],\exists [\mathrm{FiniteDimensional}\left(K,V\right)],\exists mu\in \mathrm{LinearMap}\left(K,V,\mathrm{LinearMap}\left(K,V,V\right)\right),\mathrm{finrank}\left(K,V\right)=n\wedge \left(\mathrm{IsEvolutionAlgebra}\left(mu\right)\wedge \left(\mathrm{ordinaryPower}\left(mu,k+1\right)=\mathrm{bot}\wedge \mathrm{ordinaryPower}\left(mu,k\right)\ne \mathrm{bot}\right)\right)\right)$$

Formalization. D5/S3/QuadraticForms/EvolutionAlgebras/NilpotencySpectrumRefutation.indexExists (✓ 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 existential quantifiers range over the vector space, its additive group and scalar module structures, its finite-dimensionality, and the bilinear product. The natural-basis predicate is the existing evolution-algebra definition: commutativity and a basis with zero mixed products. Zero squares are permitted.

Definition 1.4 (predicted).

$$\forall n\in \mathbb{Z},\forall k\in \mathbb{Z},\mathrm{predicted}\left(n,k\right)=\left(\left(\exists a\in \mathbb{N},k=2^a\wedge \mathrm{Int}\left(a\right)\le n-1\right)\vee \left(2\le \mathrm{count}\left(\mathrm{digits}\left(2,\mathrm{toNat}\left(k\right)\right),1\right)\wedge \mathrm{Int}\left(\log \left(2,\mathrm{toNat}\left(k\right)\right)\right)+\mathrm{Int}\left(\mathrm{count}\left(\mathrm{digits}\left(2,\mathrm{toNat}\left(k\right)\right),1\right)\right)\le n-1\right)\right)$$

Formalization. D5/S3/QuadraticForms/EvolutionAlgebras/NilpotencySpectrumRefutation.predicted (✓ 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 first branch is a power of two. In the second branch the number of digits equal to one in the base-two expansion is at least two. The function log here means the integer floor of the base-two logarithm. The dimension bound is the integer n minus one. Int denotes the cast from natural numbers to integers; toNat converts the nonnegative integer argument to its natural-number representative.

Definition 1.5 (claim).

$$\mathrm{claim}=\left(\forall K\in \mathrm{Type},[\mathrm{Field}\left(K\right)][\mathrm{Infinite}\left(K\right)]\forall n\in \mathbb{Z},\forall k\in \mathbb{Z},0\le n\Rightarrow \left(1\le k\Rightarrow \left(\mathrm{indexExists}\left(K,\mathrm{toNat}\left(n\right),\mathrm{toNat}\left(k\right)\right)\iff \mathrm{predicted}\left(n,k\right)\right)\right)\right)$$

Formalization. D5/S3/QuadraticForms/EvolutionAlgebras/NilpotencySpectrumRefutation.claim (✓ 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.

Conjecture 9 of Kaygorodov, Martin Gonzalez and Viruel, arXiv:2610.22248v1, section 2.3, asserts this equivalence for every infinite field and every nonnegative integer dimension n, at each positive integer k. The nilpotency index in its wording is k+1.

Definition 1.6 (product).

$$\forall x\in (\mathrm{Fin}\left(15\right)\to \mathbb{Q}),\forall y\in (\mathrm{Fin}\left(15\right)\to \mathbb{Q}),\mathrm{product}\left(x,y\right)=\mathrm{vector}\left(0,x\left(0\right)\cdot y\left(0\right),x\left(0\right)\cdot y\left(0\right),x\left(2\right)\cdot y\left(2\right)-x\left(1\right)\cdot y\left(1\right),x\left(0\right)\cdot y\left(0\right)+x\left(2\right)\cdot y\left(2\right)-x\left(1\right)\cdot y\left(1\right),x\left(4\right)\cdot y\left(4\right)-x\left(3\right)\cdot y\left(3\right),x\left(5\right)\cdot y\left(5\right),x\left(4\right)\cdot y\left(4\right)-x\left(3\right)\cdot y\left(3\right)+x\left(5\right)\cdot y\left(5\right),x\left(7\right)\cdot y\left(7\right)-x\left(6\right)\cdot y\left(6\right),x\left(8\right)\cdot y\left(8\right),x\left(9\right)\cdot y\left(9\right),x\left(10\right)\cdot y\left(10\right),x\left(11\right)\cdot y\left(11\right),x\left(7\right)\cdot y\left(7\right)-x\left(6\right)\cdot y\left(6\right)+x\left(11\right)\cdot y\left(11\right),x\left(13\right)\cdot y\left(13\right)-x\left(12\right)\cdot y\left(12\right)\right)$$

Formalization. D5/S3/QuadraticForms/EvolutionAlgebras/NilpotencySpectrumRefutation.product (✓ std3).

Source. Repository-derived.

Acknowledgement. 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.

In one-based coordinates the natural square rows r are: e2+e3+e5; -e4-e5; e4+e5; -e6-e8; e6+e8; e7+e8; -e9-e14; e9+e14; e10; e11; e12; e13+e14; -e15; e15; 0. The displayed vector uses zero-based coordinate subscripts; the square-row description uses one-based subscripts. The standard coordinate vectors form a natural basis. All mixed products vanish.

Theorem 1.7 (result).

$$\neg \mathrm{claim}$$

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

Resolves. Problems/kaygorodov-martin-gonzalez-viruel-2026-nilpotency-spectrum-conjecture-9 (refuted) by D5/S3/QuadraticForms/EvolutionAlgebras/NilpotencySpectrumRefutation.result.

Source. Repository-derived.

Acknowledgement. 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.

Over the infinite field Q this fifteen-dimensional algebra has A^256=0 and A^255 nonzero. The triangular spanning vectors, in order, are e1; e2+e3+e5; e3; e4+e5; e5; e6+e8; e7+e8+e9+e14; e8; e9+e14; e10+e15; e11; e12; e13+e14; e14; e15. Their weights are 1,2,1,3,1,5,10,1,15,30,60,120,240,1,255. Every nonzero product of two such vectors is another vector whose weight is at least the sum of the input weights. Bilinearity therefore gives F_r F_s contained in F_(r+s) for every positive r,s, where F_m spans vectors of weight at least m. Strong induction over all splits gives A^m contained in F_m; F_256 is zero. Starting from e1, and using e3 as the separate degree-one leaf at the second step, the input degree pairs are (1,1), (2,1), (3,2), (5,5), (10,5), (15,15), (30,30), (60,60), (120,120), (240,15). Their outputs are respectively the second, fourth, sixth, seventh, ninth, tenth, eleventh, twelfth, thirteenth and fifteenth spanning vectors. The final product has 255 leaves and equals e15. Hence the ordinary index is exactly 256. At k=255 there are eight one digits and floor(log2(k))=7; their sum 15 exceeds n-1=14, and k is not a power of two. Existence is true and both arithmetic alternatives are false.

References

• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/NilpotencySpectrumRefutation.claim
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/NilpotencySpectrumRefutation.indexExists
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/NilpotencySpectrumRefutation.ordinaryPower
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/NilpotencySpectrumRefutation.predicted
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/NilpotencySpectrumRefutation.product
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/NilpotencySpectrumRefutation.productSpace
• Truth anchor: D5/S3/QuadraticForms/EvolutionAlgebras/NilpotencySpectrumRefutation.result
• Dependency: D5/S3/QuadraticForms/EvolutionAlgebras/DerivationAnnihilatorObstruction