mme_block_tensor_is_matMul

⚠️ Retired — incorrect formalization

The Lean statement below asserts nothing: its conclusion is the proposition True, which is closed by trivial in any context. Its proof status therefore records no mathematical content and says nothing about mme_block_tensor_is_matMul. Do not import it or use it as a dependency.

Each non-zero block of a laser-aligned tensor power is a matrix-multiplication tensor. Layer-4 abstract placeholder (True-conclusion). Layer-3 refinement names explicit (a,b,c) and provides Restrict witness. WZ Lemma 6.7 / CW 1990 Lemma 5.1. Decomposes into: combinatorial bijection (type-balanced triple ↔ MM entries) + Restrict witness (basis choice on grading classes).

Why this node was retired

The posted statement is

theorem mme_block_tensor_is_matMul {K : Type u} [Field K] {T : TensorObj K 3} {t : ℕ} (_G : T.TypeGrading t) (_S : Finset (Fin t × Fin t × Fin t)) (_hSym : LaserSymmetric _S) (_hsupport : TensorObj.LaserAlignedSupport _G _S) (_N : ℕ) (_σ : Fin 3 → Fin (t ^ _N)) : True := by sorry

and its goal is True. Since True holds unconditionally, the hypotheses are never used and no relationship among them is asserted — the statement can be closed without doing any part of the work its name refers to. Concretely, this node is a title attached to an empty proposition: it occupies the name of a real result while proving none of it, and anything that imports it gains nothing.

What a faithful statement would require

The conclusion must be the mathematical assertion that the name refers to, expressed in terms of the objects and hypotheses in the signature, in place of True.

No corrected replacement node exists yet.