CubicMultiplicity.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Full one-value or three-and-three dichotomy for cubed entries.

theorem OAI.MUB6.cube_values_dichotomy line 15

Source documentation

The cubed coordinates either have one common value, or have exactly two values occurring three times each; each three-coordinate group sums to zero.

theorem cube_values_dichotomy (v : (Fin 6) → ℂ)
    (hv : ∀ i, Complex.normSq (v i) = 1)
    (h1 : ∑ i, v i = 0) (h2 : ∑ i, v i ^ 2 = 0) :
    (∀ i, v i ^ 3 = v 0 ^ 3) ∨
      ∃ b : ℂ, v 0 ^ 3 ≠ b ∧
        (∀ i, v i ^ 3 = v 0 ^ 3 ∨ v i ^ 3 = b) ∧
        (cubeClass v (v 0 ^ 3)).card = 3 ∧ (cubeClass v b).card = 3 ∧
        (∑ i ∈ cubeClass v (v 0 ^ 3), v i) = 0 ∧
        (∑ i ∈ cubeClass v b, v i) = 0 := by
…

Mentions: OAI.MUB6.cubeClass