Covariance sum from frame correlations

import Mathlib

namespace Conway99Formal.CubicMetric
end Conway99Formal.CubicMetric

set_option autoImplicit false

open Conway99Formal.CubicMetric

theorem Conway99Formal.CubicMetric.rank_one_covariance {U T I : Type*} [Fintype U] [Fintype T]
    [Fintype I] [DecidableEq I] (tau : T → I → ℝ) (h : U → T → ℝ)
    (F : U → Matrix I I ℝ)
    (hF : ∀ u i j, F u i j = -(∑ t, h u t * tau t i * tau t j) / 3)
    (hpair : ∀ t s,
      (∑ u, h u t * h u s) = 63 * (∑ k, tau t k * tau s k)) :
    (∑ u, F u * F u) =
      (7 : ℝ) • Matrix.of (fun i j =>
        ∑ t, ∑ s, (∑ k, tau t k * tau s k) ^ 2 * tau t i * tau s j) := by sorry