CubicBlock.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The three-by-three block obstruction in cubic classification, proved by Newton's determinant identity instead of a dimension argument.

theorem OAI.MUB6.trace_newton_three line 19
theorem OAI.MUB6.no_three_by_three_scaled_projection line 28
Source documentation
A three-dimensional projection cannot have rank three halves. This formulation needs only polynomial identities over the complex numbers.
```
theorem no_three_by_three_scaled_projection (C : Matrix (Fin 3) (Fin 3) ℂ)
    (hC : C * C = (6 : ℂ) • C) (ht : C.trace = 9) : False := by
…
```

theorem OAI.MUB6.no_cubic_three_by_three_block line 43

Source documentation

The two classes of three restricted rows cannot be mutually orthogonal when their combined columns are orthogonal and every entry has modulus one.

theorem no_cubic_three_by_three_block
    (A B : Matrix (Fin 3) (Fin 3) ℂ)
    (hunit : ∀ i j, Complex.normSq (A i j) = 1)
    (hcross : A * B.conjTranspose = 0)
    (hcol : A.conjTranspose * A + B.conjTranspose * B = (6 : ℂ) • 1) : False := by
…