MonochromaticObstruction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.GrahamSpherical.derivationEnergy line 12
Source documentation
The actual finite squared Euclidean energy of the entrywise derivation.
```
def derivationEnergy {n : ℕ} (D : Derivation ℤ ℝ ℝ) (y : Point n) : ℝ :=
…
```
Mentions: OAI.GrahamSpherical.Point
def OAI.GrahamSpherical.energyColor line 16
Source documentation
Native integer floor and Euclidean remainder, reindexed into Fin 50.
```
def energyColor {n : ℕ} (e : Point n → ℝ) (y : Point n) : Fin 50 :=
…
```
Mentions: OAI.GrahamSpherical.Point
theorem OAI.GrahamSpherical.energyColor_eq_implies_residue_eq line 22
theorem OAI.GrahamSpherical.energyColor_avoids_of_invariant line 34
Source documentation
Every copy here is an actual isometry of the literal witness subtype. The energy identity is an explicit intermediate premise, discharged separately.
```
theorem energyColor_avoids_of_invariant {n : ℕ} (e : Point n → ℝ)
    (hinvariant : ∀ (f : witness → Point n), Isometry f →
      ∑ i : Label, (weight i : ℝ) * e (f ⟨vertex i, ⟨i, rfl⟩⟩) = 8) :
    AvoidsCopy witness (energyColor e) := by
…
```
Mentions: OAI.GrahamSpherical.Point, OAI.GrahamSpherical.witness, OAI.GrahamSpherical.Label, OAI.GrahamSpherical.weight, OAI.GrahamSpherical.vertex, OAI.GrahamSpherical.AvoidsCopy, OAI.GrahamSpherical.energyColor