mme_independent_blocks_form_direct_sum_restrict_refined
Disprovedabstract-frameworkalgebraic-complexityblock-tensordirect-sumlaser-methodmatrix-multiplicationrefinedrestrictwigderson-zuiddam
Pairwise mode-disjoint block subtensors form a direct-sum Restrict of T — REFINED concrete-statement version of mme_independent_blocks_form_direct_sum_restrict using the new blockSubtensor API. Hypothesis: C ⊆ (Fin 3 → Fin t) is pairwise mode-disjoint (∀ distinct σ, σ' ∈ C, ∀ i, σ i ≠ σ' i). Conclusion: any enumeration B : Fin C.card → TensorObj K 3 of the block subtensors over C satisfies Restrict (bigAdd B) T. Replaces the original True-placeholder hypotheses with this concrete pairwise-disjointness condition. ~150-300 LOC proof via Submodule.iSupIndep applied mode-wise. Every laser-method Salem-Spencer-direct-sum step now has a concrete reusable target.
Preamble
import Definitions.Def_mme_block_subtensor import Definitions.Def_mme_tensor_rank open MME universe u
Formal statement
theorem mme_independent_blocks_form_direct_sum_restrict_refined {K : Type u} [Field K] {T : TensorObj K 3} {t : ℕ} (G : T.TypeGrading t) (C : Finset (Fin 3 → Fin t)) (_hDisj : ∀ σ ∈ C, ∀ σ' ∈ C, σ ≠ σ' → ∀ i : Fin 3, σ i ≠ σ' i) (B : Fin C.card → TensorObj K 3) (_hB : ∀ j : Fin C.card, ∃ σ ∈ C, B j = G.blockSubtensor σ) : TensorObj.Restrict (TensorObj.bigAdd B) T := by sorrySource