mme_tensorAsymptoticRank_kronPow_le

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

Asymptotic rank is multiplicative under Kronecker powers.

For any order-$d$ tensor object $X$ and natural number $N$,

(In fact equality holds, by reindexing the underlying iInf; the $\leq$ direction is what's needed for τ-style ω-bound derivations.)

Proof sketch. Unfold $\widetilde R$ as $\inf_n \mathrm{tensorRankObj}(X^{\otimes(n+1)})^{1/(n+1)}$. For $X^{\otimes N}$, the infimum is over $\mathrm{tensorRankObj}((X^{\otimes N})^{\otimes(n+1)})^{1/(n+1)} = \mathrm{tensorRankObj}(X^{\otimes N(n+1)})^{1/(n+1)} = \bigl(\mathrm{tensorRankObj}(X^{\otimes N(n+1)})^{1/(N(n+1))}\bigr)^N$. Taking the infimum over $n$ is at most taking the infimum over the subsequence $\{N(n+1)\}$ of $\mathrm{tensorRankObj}(X^{\otimes m})^{1/m}$, which is bounded above by the full infimum over $m$ (= $\widetilde R(X)$). The $\,\cdot^N$ outside gives the result.

Reusability — abstract Layer-2 leaf under mme_omega_le_of_subrank_capacity. Together with mme_holder_subexp_capacity_omega_bound, this discharges the asymptotic-rank scaling step of the abstract bridge from subrank capacity to ω bound. Reusable for any tensor with an asymptotic-rank upper bound; the canonical CW use case bounds $\widetilde R(T_6) \leq 8$ via mme_degenerates_asymptoticRank_le ∘ mme_CW_border_rank_le, then this leaf gives $\widetilde R(T_6^{\otimes N}) \leq 8^N$.

Why this node was retired

The posted statement is

theorem mme_tensorAsymptoticRank_kronPow_le {K : Type u} [Field K] {d : ℕ} (X : TensorObj K d) (N : ℕ) : tensorAsymptoticRank (X.kronPow N) ≤ tensorAsymptoticRank X ^ N := by sorry

The rank definition at tensor order zero takes a natural infimum of an empty representation set, yielding zero for scalar −1.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

Require tensor order d≥2 in the current rank-law statement, or redesign tensorRankObj so order-zero scalar tensors have mathematically intended rank and prove the needed Kronecker-rank laws. Do not simply change the inequality or use the empty-infimum value. The proposed d≥2 repair has not been checked here.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.