mme_independent_blocks_form_direct_sum_restrict

⚠️ Retired — incorrect formalization

The Lean statement below does not express the problem its name refers to, so its Disproved status carries no information about that problem. Do not import it or use it as a dependency.

Intended content: if the blocks $B_1, \dots, B_k$ are independent and each restricts to $T$, then their direct sum restricts to $T$.

Why this node was retired

The posted statement is

theorem … (B : Fin k → TensorObj K d) (_hindep : True) (_hsub : True) :
    TensorObj.Restrict (TensorObj.bigAdd B) T

Both hypotheses are placeholders. _hindep : True was to express independence of the blocks and _hsub : True was to express that each block restricts to $T$; as written they assume nothing. What remains is the claim that for every family $B$ and every target $T$ the direct sum TensorObj.bigAdd B restricts to $T$, which is false in general — hence the Disproved status, which says nothing about the intended lemma.

Note also that $T$ is an implicit argument that appears only in the conclusion, so nothing connects the blocks to the target.

What a faithful statement would require

Independence of the family and the per-block restriction property must be stated as real propositions about B and T in place of the two Trues.

No corrected replacement node exists yet.