Incident sum of incidence square

import Definitions.Def_CubicOperators
import Mathlib

namespace Conway99Formal.CubicOperators.Graph
end Conway99Formal.CubicOperators.Graph

set_option autoImplicit false

/-! Algebraic contraction lemmas for the graph-owned triangle cubic. The
incidence identities in the hypotheses are the explicit graph bridge. -/

open Conway99Formal.CubicOperators

open Finset

variable {T I : Type*} [Fintype T] [Fintype I]






























































open Conway99Formal.CubicOperators.Graph

open Finset



variable {V : Type*} [Fintype V] [DecidableEq V]
variable (G : SimpleGraph V) [DecidableRel G.Adj]

theorem Conway99Formal.CubicOperators.Graph.incident_sum_of_incidence_square (Pi : Matrix Coord V ℝ)
    (hf : IsPointFrame G Pi)
    (hinc : realIncidenceMatrix G * (realIncidenceMatrix G).transpose =
      7 • (1 : Matrix V V ℝ) + G.adjMatrix ℝ)
    (u : V) (i : Coord) :
    (∑ T : Triangle G, incidence G u T * triangleVector G Pi T i) =
      pointColumn Pi u i := by sorry