CubicHadamard.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.MUB6.hadamard_row_ratio_moments line 12
theorem OAI.MUB6.cubed_row_ratio_pattern line 26
theorem OAI.MUB6.twoValuePattern_constant line 33
theorem OAI.MUB6.cubed_row_pattern line 38

theorem OAI.MUB6.dephased_hadamard_cubes_block line 48

Source documentation

Before excluding it with the three-by-three block obstruction, the only possible failure of cube roots after dephasing has one constant block.

theorem dephased_hadamard_cubes_block {H : CMatrix} (hH : IsHadamard H)
    (hH2 : IsHadamard (fun i j => H i j ^ 2))
    (h0row : ∀ j, H 0 j = 1) (h0col : ∀ i, H i 0 = 1)
    (i j : Coord) (hij : H i j ^ 3 ≠ 1) :
    ∃ (R S : Finset Coord) (x : ℂ),
      R.card = 3 ∧ S.card = 3 ∧ (0 : Coord) ∉ R ∧ (0 : Coord) ∉ S ∧
      x ≠ 0 ∧ x ≠ 1 ∧
      ∀ r c, H r c ^ 3 = if r ∈ R ∧ c ∈ S then x else 1 := by
…

Mentions: OAI.MUB6.CMatrix, OAI.MUB6.IsHadamard, OAI.MUB6.Coord