Hastriangletightness 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.hasTriangleTightness_of_incidence_square (Pi : Matrix Coord V ℝ)
    (hf : IsPointFrame G Pi)
    (hinc : realIncidenceMatrix G * (realIncidenceMatrix G).transpose =
      7 • (1 : Matrix V V ℝ) + G.adjMatrix ℝ) :
    HasTriangleTightness G Pi := by sorry