slug: aliabadi-2025-matchability-subspace-product
bibkey: aliabadi2025matchabilityii
doi: 10.7151/dmgaa.1461
url: https://www.dmgaa.uz.zgora.pl/publish/pdf.php?doi=1461
triage: theorem
motivation_gids:
  - D5/S3/Factorization/Galois/AliabadiSubspaceProductRefutation.result

Aliabadi’s uncapped subspace-product conjecture is false

Problem

Mohsen Aliabadi, Conditions for matchability in groups and field extensions II, Discussiones Mathematicae General Algebra and Applications 45 (2025), 135–157, section 5.1, Conjecture 38, printed page 154 / PDF page 20, states:

Let $K\subset L$ be a field extension and $A,B\subset L$ be a $K$-subspace of $L$ of finite positive dimensions. Assume further that for every $a,b\in L$ and every nontrivial proper finite intermediate subfield $K\subset M⊊L$, we have

$${\dim }_K(aM\cap A)+{\dim }_K(bM\cap B)\le [M:K]+1.$$

Then for all $K$-subspaces $S\subset A$ and $T\subset B$, the following holds

$${\dim }_K⟨ST⟩\ge {\dim }_{K}S+{\dim }_{K}T-1.$$

The same statement is Conjecture 5.1 in arXiv:2309.14664v1, PDF page 14, and v2/v3, PDF page 15. Section 2.2 defines the brackets as the $K$-linear span of the actual product set in $L$. The source note records the primary versions, DOI and locators. The sole target is the whole original universal assertion. Preregistration: #23409.

Statement correspondence

The matching definitions in the introduction use equal dimensions and $1\notin B$ when defining matchability. Conjecture 38 states neither matchability nor these conditions as an added premise. The witness nonetheless has $A=B$ and $S=T$, with $1$ absent from all four spaces. It also has $S<A<L$ and $T<B<L$. No assumption that a subspace contain $1$, that the ambient extension be infinite, or that the dimension sum be small is inserted. No ambient cap replaces the source conclusion.

Motivation

Section 5.1 seeks a linear counterpart of the group product-set estimate used for sufficient matchability conditions. The conjecture would force expansion of every pair of contained subspaces from bounds on translated intermediate-field intersections. Its universal conclusion must also respect finite ambient dimension. A field of prime degree separates that obstruction from all the proper intermediate-field tests in the premise.

Gap

The premise omits the ambient intermediate field $M=L$. In prime degree there is also no nontrivial proper intermediate field. Thus the premise places no restriction on $A$ and $B$ in this case, while the proposed conclusion can demand dimension larger than $[L:K]$. The obstruction persists for strict subspaces and for spaces avoiding $1$; it is not caused by choosing an endpoint or a zero-dimensional space.

Route

Set $K=\mathbb{Q}$, $f=X^7-2$, $L=\mathbb{Q}[X]/(f)$ and let $\alpha$ be the class of $X$. Eisenstein at the prime ideal $(2)$ first proves the integer polynomial irreducible; its monicity gives primitiveness, and Gauss’s lemma transfers irreducibility to $\mathbb{Q}[X]$. AdjoinRoot then supplies the field and its canonical algebra structure. Its power basis gives

$$[L:\mathbb{Q}]=7,{\alpha }^7=2,1,\alpha ,{\alpha }^2,\dots ,{\alpha }^6\text{ a basis}.$$

Define

$$A=B={\mathrm{span}}_{\mathbb{Q}}\{\alpha ,\dots ,{\alpha }^6\},S=T={\mathrm{span}}_{\mathbb{Q}}\{\alpha ,\dots ,{\alpha }^5\}.$$

The selected powers are distinct basis entries. Their spans have dimensions six and five; the omitted constant entry proves $1$ is absent. The inclusion of the five powers among the six, together with their strict dimension inequality, proves $S<A$ and $T<B$. Dimension six is less than seven, so $A$ and $B$ are proper ambient subspaces.

IntermediateField.isSimpleOrder_of_finrank_prime proves that every intermediate field is bottom or top. This discharges the full universal premise for every scalar pair and every finite nontrivial proper $M$. For the identical actual product span appearing in claim, the ambient finrank bound gives

$${\dim }_{\mathbb{Q}}⟨ST⟩\le 7<9=5+5-1.$$

Applying the universal assertion to these fields and subspaces yields a contradiction. Exact equality $⟨ST⟩=L$ is unnecessary and is not asserted as proved. The endpoint negates the whole original claim, not only a proposition about the selected parameter values.

Falsifier

An omitted source condition excluding this finite extension or these subspaces, a different meaning of the printed intermediate-field range, or a failure of irreducibility, the actual quotient field, the power-basis dimensions, or the actual product-span bridge would invalidate the route. All four primary versions have the same quantified uncapped conclusion; the source conditions above are matched by the formal claim and witness. The optional exact product-span equality is outside the required argument.

Evidence

The formal endpoint is D5/S3/Factorization/Galois/AliabadiSubspaceProductRefutation.result, with literal type Not claim; claim has literal type Prop. The Scribe binds the dossier to this one endpoint with a Refuted OpenProblemResolutionClaim. The public definitions describe the field, translated-intersection premise, universal claim, power spans and realized certificate. The private countermodel_verified proves that certificate; result uses its premise, dimensions, containments and product upper bound.

The exact reused suppliers in pinned Mathlib include the Eisenstein and Gauss irreducibility theorems, AdjoinRoot.powerBasis', the prime-degree intermediate-field theorem, finrank_span_eq_card, and Submodule.finrank_le. No external Lean dependency is selected. The axiom closure is contained in Classical.choice, Quot.sound and propext; there is no sorry or new axiom. The source-authored inventory has six public definitions, two public abbreviations, nine private implementation theorems, two private definitions, two private instances, and one public theorem. Compiler-generated companions are not additional authored public results.

The proof organization is bind-only. Its admission basis is the external named open-problem-resolution under #23409, and its utility is certified-instance with refutes pointing to the literal whole claim. The designated result is exempt from four-slot escape registration; there is no other authored public theorem requiring a Reg mirror. No new general method or escape witness is claimed.

Triage

Tier 1: a short refutation of the complete original published conjecture. The 2023 preprint and 2025 journal statement provide the named target; the bounded source/literature screen in #23409 found no prior settlement in its searched scope. This is not an exhaustive literature or priority certificate. Aliabadi–Zerbib’s matroid Question 2.7 is a different problem.

What the settlement shows

The failure mechanism is finite ambient saturation combined with omission of $L$ from the field tests. Any linear matchability argument relying on the universal estimate must replace or restrict that estimate. The source presents the estimate as a proposed future extension of a group result; the refutation does not negate that group theorem, the separate Chowla conjecture, or the paper’s independently proved matching theorems. The surviving certified facts are the explicit field and subspaces and their full premise together with the incompatible lower and upper bounds. No repair or uniform family theorem is inferred from this one certificate.

ASSUMED-UNVERIFIED

Completeness of the bounded external literature and Lean-ecosystem searches, worldwide priority, and absence of uninspected settlements remain ASSUMED-UNVERIFIED. The historical supplier-search ordering is recorded in the completed source handoff, rather than independently timestamp-certified by the mathematical proof. It includes repository declarations, including private originals, then pinned Mathlib, then a bounded external screen; exact generic suppliers are directly reused. The formal result makes no claim about exhaustive theorem discovery or method novelty. The stronger exact product-span equality and the alternative repaired conjectures listed above are not proved by this endpoint.