44-coordinate point frame and triangle tightness

import Mathlib

set_option autoImplicit false

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

namespace Conway99Formal.CubicOperators

open Finset

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





























































end Conway99Formal.CubicOperators

namespace Conway99Formal.CubicOperators.Graph

open Finset

abbrev Coord := Fin 44

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

/-- A triangle of the given graph, with its original vertex labels. -/
abbrev Triangle := {T : Finset V // T ∈ G.cliqueFinset 3}

/-- A column of the real point frame of this graph. -/
def pointColumn (Pi : Matrix Coord V ℝ) (u : V) : Coord → ℝ :=
  fun i => Pi i u



/-- The four source equations that make `Pi` the actual `(-4)` point frame. -/
structure IsPointFrame (Pi : Matrix Coord V ℝ) : Prop where
  gram : Pi.transpose * Pi =
    27 • (1 : Matrix V V ℝ) - 9 • G.adjMatrix ℝ + Matrix.of 1
  tight : Pi * Pi.transpose = 63 • (1 : Matrix Coord Coord ℝ)
  zero_sum : Pi.mulVec (fun _ => (1 : ℝ)) = 0
  adjacency : Pi * G.adjMatrix ℝ = -(4 • Pi)



/-- The triangle vector formed from the same frame and graph. -/
noncomputable def triangleVector (Pi : Matrix Coord V ℝ) (T : Triangle G) : Coord → ℝ :=
  fun i => (∑ u ∈ T.1, Pi i u) / 3





/-- Point-triangle incidence in the original graph. -/
def incidence (u : V) (T : Triangle G) : ℝ :=
  if u ∈ T.1 then 1 else 0

/-- Real vertex-triangle incidence matrix of the same graph. -/
def realIncidenceMatrix : Matrix V (Triangle G) ℝ :=
  fun u T => if u ∈ T.1 then 1 else 0

















































/-- The source's `V Vᵀ=21I` in the fixed frame coordinates. -/
def HasTriangleTightness (Pi : Matrix Coord V ℝ) : Prop :=
  ∀ i j : Coord, (∑ T : Triangle G,
    triangleVector G Pi T i * triangleVector G Pi T j) =
      21 * (if i = j then (1 : ℝ) else 0)












end Conway99Formal.CubicOperators.Graph