A null direct summand in a tensor power of a singular semigroup module

David He and Daniel Tubbenhauer, Tensor powers of representations of (diagram) monoids, arXiv:2508.04054v1, Conjecture 4.2, page 17:

Let V be a kS-module on which no element acts invertibly, then there is some m ≥ 1 such that Z is a summand of V^{⊗m}, and consequently a(n)=(dim V)ⁿ.

The field is algebraically closed, the semigroup is nonempty and finite with no two-sided identity, and the representation is finite dimensional and nonunital. The one-dimensional null representation has zero action. The source defines $a(n)$ as an asymptotic equivalent of the indecomposable-summand count $b(n)$, with multiplicity. Thus the final clause means $b(n)/(\dim V)^n\to1$, rather than exact equality at finite exponents. Preregistration: #22531.

Statement echo

| Source clause | Lean counterpart | | --- | --- | | Algebraically closed field of arbitrary characteristic | claim: field and algebraic-closure instances, with no characteristic restriction | | Nonempty finite semigroup without identity | claim: semigroup, finiteness and nonemptiness instances, and the negated two-sided-identity existence hypothesis | | Finite-dimensional nonunital module | claim: finite-dimensional vector space and a multiplicative map into endomorphisms | | Every element acts noninvertibly | claim: nonunit hypothesis for every action | | Some positive tensor power contains the null representation as an actual direct summand | HasNullSummand and the first conjunct of claim; complementary subspace is invariant | | Indecomposable summands counted with multiplicity | IsIndecomposableSummand, IsSummandCount, internal direct sum indexed by Fin b | | The asymptotic equivalent is the tensor dimension | Count-sequence existence and the ratio limit for every such sequence, the second and third conjuncts of claim |

Nonemptiness and singularity exclude the zero space; there is no additional nonzero-space hypothesis. The public definitions retain the literal preregistered expressions. The tensor action uses the upstream PiTensorProduct.map construction.

The frozen settling declaration is D5/S3/HomologicalAlgebra/TensorNullSummand.result. It proves the entire claim, including count-sequence existence and the limit for every internal indecomposable decomposition. The source's stated asymptotic consequence is therefore included in the settlement.

The exact maximal-null-multiplicity identity suggested by the source outline is not separately formalized. The general infinite-semigroup extension, universal formal sharpness of the Jordan-family formula, and the separate invertible-action monoid group-summand conjecture remain open in this delivery.

For an operator family on $W$, write $K=\bigcap_s\ker a_s$ and $I=\sum_s\operatorname{im}a_s$. The private split_common_null constructs a complement $L$ of $K\cap I$ in $K$ and an ambient complement $U$ of $L$ containing $I$. Thus every action vanishes on $L$ and preserves $U$. The compiled dimension identity is $\dim L+\dim(K\cap I)=\dim K$.

The common-image and common-kernel dimension bounds yield a null line whenever $2\sum_s\operatorname{rank}a_s<\dim W$. Tensor ranks are bounded by individual-rank powers. Singularity makes these ranks strictly smaller than $d=\dim V$, so geometric decay gives a sufficient positive exponent. Strong induction on dimension constructs indecomposable decompositions. The private count bounds hold for every such decomposition and yield the universal ratio limit by squeezing.

A representation satisfying every hypothesis of claim and violating its positive-power existence or universal ratio limit would contradict the kernel-checked settling declaration. The finite experiments test the splitting construction independently; their finite scope does not establish the universal conclusion.

The public theorem D5.S3.HomologicalAlgebra.TensorNullSummand.result is the kernel evidence. Its axiom closure is contained in ${\mathrm{propext},\mathrm{Classical.choice},\mathrm{Quot.sound}}$. Its Scribe displays the full proposition.

The escape audit is unfinished: #25442. The dependent-family registration lacks a faithful full-telescope realization, equivalence bridge, variation and whole-family observational-sensitivity evidence. No validated registration is claimed.

Independent finite experiment

Experiment source and data, immutable commit 93806b3096b542f57f6884b2c30f723a225ccb43, script check.py, SHA-256 50e965a51db43be71be3771da00239828e289983585bc4cba17f24d22db5b0b6. The verified immutable script was run as python3 /Users/auric/.sshx/b6846da44a97a17369f2364c/attempt-1/verified-check.py, exit 0, final result ALL_CHECKS_OK.

It checks all 1023 nonempty families of singular $2\times2$ matrices over $\mathbf F_2$ in 3069 tensor cases at $n=1,2,3$; 92 families are semigroups and 79 have no identity. The $n=1$ cases also agree with exhaustive null-image-idempotent enumeration. At $n=5$ the full singular-matrix family has lower bound 14 and computed null multiplicity 28. There are 25 Jordan-chain cases, $2\le d\le6$, $1\le n\le5$. Source Example 4.3 gives $b(0),\ldots,b(5)=(1,1,29,209,1289,7769)$ and 28 null summands at $n=2$; the checker verifies $b(n)=6^n-7$ for $2\le n\le12$. These are computed readings in exactly those ranges.

What the settlement shows

1. Proved, kernel-checked: result proves the exact binding claim, including the nonvacuous universal asymptotic count assertion.
2. Proved, kernel-checked: the consumed exists_null_tensor_power, tensor_counts_tendsto and exists_summand_count work over any field. Their signatures require neither algebraic closure nor absence of a semigroup identity.
3. Proved, kernel-checked: summand_count_lower gives $\dim W\le b+2\sum_s\operatorname{rank}a_s$ for every internal indecomposable decomposition with $b$ factors.
4. Computed: the immutable experiment above verifies 1023 nonempty singular $\mathbf F_2$ matrix families in 3069 tensor cases and 25 Jordan-chain cases, with the stated command, exit code and SHA-256.
5. Open: universal formal sharpness of the Jordan-family formula and a general infinite-semigroup extension are not supplied. The finite Jordan computations do not establish either extension.
6. Open: the separate monoid group-summand conjecture for invertible actions is not settled by this argument.
7. Proved in prose from the compiled bounds: for any $m\ge1$ with $2|S|(d-1)^m<d^m$, tensor_rank_sum_bound bounds twice the tensor-rank sum by $2|S|(d-1)^m$, while tensor_power_finrank identifies the ambient dimension with $d^m$. Thus the hypothesis of null_summand_of_rank_bound holds at that $m$, giving a null line. The kernel-checked exists_power_separation supplies such an exponent and exists_null_tensor_power applies it. The upper bound tensor_power_range_le suffices without a separate rank-equality theorem.
8. Open: the exact maximal-null-multiplicity identity is not separately formalized; the compiled complement identity and rank/count bounds suffice for the unchanged target.

The source's “consequently” clause is proved as a ratio limit in result. No additional result about invertible monoid actions follows from this theorem.

Literature status

The bounded source and literature screen recorded in #22531 found no settlement of Conjecture 4.2. Its inspected source is arXiv:2508.04054v1. The restricted right-idempotent-generation results of arXiv:2512.05510v3 do not establish the full singular-semigroup assertion. This is a bounded literature finding; completeness is ASSUMED-UNVERIFIED.

Global publication, citation-index and full-text search completeness is ASSUMED-UNVERIFIED. The experiment's finite ranges do not prove uniform Jordan-family sharpness or an infinite-semigroup extension. Escape registration is unfinished under #25442.