OAI.HadamardSix.rowRatio_cubeFiber_sum_zero
OpenThe theorem states that, for a 6×6 complex matrix H, which is called a complex Hadamard matrix when every entry has modulus 1 and HH = 6I (with H the conjugate transpose), the following holds. Suppose H is complex Hadamard and the entrywise square matrix, whose (i,j) entry is H_{ij}², is also complex Hadamard. Let i and j be distinct row indices in Fin 6, and define the row ratio r_k = H_{ik}·conj(H_{jk}) for each column k. Suppose a and b are distinct complex numbers such that for every column k, r_k³ equals a or r_k³ equals b. Then the sum of H_{ik}·conj(H_{jk}) over the set of columns k with r_k³ = a is zero. This is stated as an admitted theorem with no proof supplied.
Preamble
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a -- Source: lean/ComparatorChallenges/HadamardCubeFiber.lean; bytes 714..1057 -- Kind: theorem; original declaration names and bodies preserved. -- Source groups are independent. Target: Lean 4.33.1; see compilation.json. import Mathlib import Definitions.Def_HadamardCubeFiber namespace OAI open scoped BigOperators Matrix namespace HadamardSix
Formal statement
lemma rowRatio_cubeFiber_sum_zero {H : Matrix6} (hH : IsComplexHadamard H)
(hs : IsComplexHadamard (entrywiseSquare H)) {i j : Index} (hij : i ≠ j)
(a b : ℂ) (hne : a ≠ b)
(hab : ∀ k, rowRatio H i j k ^ 3 = a ∨ rowRatio H i j k ^ 3 = b) :
∑ k ∈ cubeFiber (rowRatio H i j) a, H i k * star (H j k) = 0 := by
sorry
end HadamardSix
end OAI
Source
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.