Exercise PLAN-112

The flip is a commuting involution over any field. Characteristic different from2 gives complementary algebraic eigenspace projectors; orthogonal projections require the specified real/complex tensor-product metric, not merely involutivity. Characteristic2 and incompatible metrics expose the old scope gap.

1. The algebraic flip is a well-defined involution over any field on the algebraic tensor product; only actually present nonzero eigenvectors define eigenvalues, with characteristic and zero/one-dimensional boundaries explicit.
2. Simple-tensor action proves the flip commutes with phi(g) tensor phi(g), without finite dimension or a unitary representation assumption.
3. When 2 is invertible the half-sums are complementary algebraic idempotents; the compatible tensor-product metric makes them self-adjoint/orthogonal, while characteristic2 and an incompatible positive metric refute unqualified claims.
4. Their images are exactly the plus/minus flip kernels when char!=2, with zero, one-dimensional and higher-dimensional occurrences and the finite-dimensional bases distinguished.
5. Commutation makes both images invariant and the decomposition G-equivariant; the metric specialization adds orthogonality without changing the representation or assuming its unitarity.

The flip is a well-defined K-linear map by the tensor-product universal property: (x,y)->y tensor x is bilinear. Simple tensors span the algebraic tensor product, whether or not V is finite-dimensional. Thus F^2(x tensor y)=x tensor y proves F^2=I_W. Write T_g=phi(g) tensor phi(g). Both F T_g and T_g F send x tensor y to phi(g)y tensor phi(g)x, so they agree on all W. Neither assertion uses a metric, a finite basis, finite G, unitarity or division by two.

Suppose char(K)!=2, so 2 is invertible. Then P_+^2=(I+2F+F^2)/4=P_+ and P_-^2=(I-2F+F^2)/4=P_-. Also P_++P_-=I and P_+P_-=P_-P_+=(I-F^2)/4=0. F P_+=P_+ and F P_-=-P_- show the corresponding images are contained in ker(F-I) and ker(F+I). Conversely, if Fz=z then P_+z=z; if Fz=-z then P_-z=z. Hence those images are exactly the stated eigenspaces. Every z decomposes as P_+z+P_-z, and the intersection is zero because Fz=z=-z implies 2z=0. This proves a direct sum with unique components. The names Sym^2(V) and Lambda^2(V) mean these subspaces throughout this question, as in the source example. No exterior-quotient identification is silently used in characteristic2. Since each P is a polynomial in F, it commutes with T_g; T_g(Pz)=P(T_gz) lies in the image. Using g^(-1) gives equality of image with its transform, so both restrictions are representations and the direct-sum map is G-equivariant. These are complementary, mutually annihilating algebraic idempotents; such algebraic 'orthogonality' does not by itself mean self-adjoint orthogonal projection.

In characteristic2 there is no scalar 1/2 and +1=-1. The universal involution/commutation identities still hold, but the displayed half-projectors are not defined and the two proposed flip eigenspaces coincide. Concretely take K=F_2, V=K^2 and G trivial. In the tensor basis b_00,b_01,b_10,b_11, F exchanges b_01 and b_10 and fixes the other two. N=F-I is nonzero, with N b_01=b_01+b_10 and N^2=0. The common plus/minus eigenspace is ker N=span(b_00,b_11,b_01+b_10), of dimension3 in the dimension4 space W. It cannot give the claimed two-eigenspace direct sum or span all W. Thus the old field-unqualified half-projector request is genuinely invalid in this allowed field, not cured by treating 1/2 as a totalized zero. This does not rule out every invariant decomposition for every particular representation; it rules out the asserted universal formula/eigenspace split.

Now take the separately specified real or complex inner-product setting, with the SAME inner product on each factor and its tensor-product metric. On simple tensors, <F(x tensor y),F(u tensor v)>=<y,v><x,u>=<x,u><y,v>, and <F(x tensor y),u tensor v>=<y,u><x,v>=<x tensor y,F(u tensor v)>. Extend by sesquilinearity to finite sums. Hence F is isometric and has adjoint F itself; F^(-1)=F also follows from the involution. Consequently P_+†=P_+ and P_-†=P_-, in addition to idempotency. Moreover <P_+a,P_-b>=<a,P_+P_-b>=0. Thus their images are orthogonal and the same decomposition is an orthogonal one; these are the orthogonal projections onto those images. This proof does not assume the group action preserves the inner product: invariance follows from the preceding commutation, so a nonunitary phi is allowed. No completed Hilbert-space tensor product is silently substituted for the algebraic one.

The metric qualification is essential. Set V=C^2 and use the same ordered tensor basis above, but on W choose the positive-definite Gram matrix H=diag(1,1,2,1), not the tensor square of one chosen metric on V. F still squares to I, yet ||F b_01||_H^2=2 while ||b_01||_H^2=1, so it is not unitary in this metric. More directly <F b_01,b_10>_H=2 whereas <b_01,F b_10>_H=1, so F is not self-adjoint. The algebraic plus vector s=b_01+b_10 and minus vector a=b_01-b_10 satisfy <s,a>_H=1-2=-1, not zero. Thus the algebraic idempotents are not orthogonal projections in this legitimate but incompatible metric. A permutation's real symmetric matrix is not a basis-independent proof of Hermiticity unless that basis is orthonormal for the actual metric.

For char(K)!=2 and V=0, W=0; I_W,F,P_+,P_- are all the unique zero map, both images are zero and there are no eigenvalues (eigenvectors must be nonzero). For dim(V)=1, F=I_W, P_+=I_W and P_-=0, so only +1 occurs. For dim(V)>=2, choose independent x,y: the nonzero vectors x tensor x and x tensor y-y tensor x give eigenvalues +1 and -1 respectively, even in infinite dimension. If d is finite, the symmetric basis x_i tensor x_i and x_i tensor x_j+x_j tensor x_i for i<j, and antisymmetric basis x_i tensor x_j-x_j tensor x_i for i<j, yield dimensions d(d+1)/2 and d(d-1)/2. This is an optional finite-dimensional specialization, not an assumption in the universal algebraic proof. In characteristic2 the original formulas remain undefined even in low dimensions; for a one-dimensional V the flip is identity and the two named eigenspaces coincide. Thus the correction explicitly separates a universally meaningful flip, a characteristic-dependent algebraic split and a metric-dependent orthogonal split; it does not claim the original unspecific request was already a fully typed theorem.

1. Proves well-definedness, F^2=I and commutation on spanning simple tensors with no finite-dimensional, metric or unitarity premise; does not assert that both eigenvalues always occur. (1 weight)
2. Proves all half-projector algebraic identities for char!=2 and explicitly refutes the unqualified characteristic2 formula/split using a concrete F_2^2 witness. (1 weight)
3. Identifies both image/kernel eigenspaces in both directions and proves the direct-sum representation/invariance; correctly handles V=0, dimension1 and dimension>=2. (1 weight)
4. Derives F†=F/isometry and metric orthogonal projection from the specified real/complex tensor-product inner product, not from involutivity alone; verifies an explicit incompatible Gram-metric counterexample and keeps algebraic versus metric assertions distinct. (1 weight)

No aligned Lean view has been admitted for this native core in this textbook checkpoint. This is not a claim that the underlying mathematics lacks a formal proof. Contributions must preserve this exact target contract and split.

Read the Lean track and existing diagnostic warmups

• website/research/sources.json

  leditzky-2025-repth-qit

  Source SHA-256: 9f85f45f20ed5a46931ad0dec3b94ee09748bc56e39fae29b0aefe910440b0ae · MIT metadata only
• Primary source

Contract: 39d1ada95b06b194068795408738de8b848948875e62f1ae6293547cb055c41f

Item digest: 99726c8e5c24347e62ed199cbd98623cc0ad20376610f14a23e34c2cbcc4ca78

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

Authored support steps: 5. This is not measured graph distance or model difficulty.

{ "question_version": 2, "predecessor_key": "qcb-core-plan-112-sym-antisym-projectors-swap-operator", "predecessor_item_digest": "e8c8246646fbf81f51999b8e11cc182f484f8874e8336b896a04bced8d9ab219", "predecessor_contract_hash": "9fe8d82f4864ac76e0234ade21d7e2bfe84b1e31e622941593236230470e4720", "current_contract_hash": "39d1ada95b06b194068795408738de8b848948875e62f1ae6293547cb055c41f", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/plan-112-swap-algebra-metric-question-successor.json", "repair_record_digest": "ff862e93c47b9b828ac723a9f65cbb10087527e0d575bcf443d641af9602bbd8", "review_record": "reports/textbook-v1/repairs/plan-112-swap-algebra-metric-question-successor-review.json", "review_digest": "36eb797bb3b89897230d24196120d073fb4a8cd7c3b8e2210ac3fbdf50469dae", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }