feat(opening): fold four tensor axes to two

[windsornguyen]

Explain what this changes, why it is needed, and anything reviewers should
verify. Link an issue when one exists.

What does this change?

Instantiates the affine binder on a 2 x 2 x 2 x 2 binary tensor and proves a semantic four-axis-to-two-axis exact fold. The child type has two axes; this PR does not claim a particular compiled memory representation.

How was it tested?

• lake build --wfail passes on stacked tip 16b7318
• lake lint passes on stacked tip 16b7318
• No sorry or new axioms, or this PR does not change Lean proofs
• git diff --check passes
• The four-axis affine instantiation compiles