FormalConjecturesForMathlib.Combinatorics.SimpleGraph.UnitDistancePlaneGraph

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module

public import FormalConjecturesForMathlib.Geometry.Euclidean
public import Mathlib.Analysis.InnerProductSpace.PiL2
public import Mathlib.Combinatorics.SimpleGraph.Basic

@[expose] public sectionnamespace SimpleGraphvariable {α : Type*} [Fintype α] [DecidableEq α]open Finset List

A unit distance graph in ℝ²: A graph where the vertices V are a collection of points in ℝ² and there is an edge between two points if and only if the distance between them is 1.

def UnitDistancePlaneGraph (V : Set (EuclideanSpace ℝ (Fin 2))) : SimpleGraph V where
  Adj x y := dist x y = 1
  symm.symm x y := byα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αV:Set (EuclideanSpace ℝ (Fin 2))x:↑Vy:↑V⊢ dist x y = 1 → dist y x = 1 simp [dist_comm]All goals completed! 🐙

An integer distance graph in ℝ²: the same construction with 1 replaced by an arbitrary positive integer, so two distinct points are adjacent exactly when the distance between them is a positive whole number.


def IntegerDistancePlaneGraph (V : Set (EuclideanSpace ℝ (Fin 2))) : SimpleGraph V where
  Adj x y := ∃ n : ℕ, 0 < n ∧ dist x y = n
  symm.symm x y := byα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αV:Set (EuclideanSpace ℝ (Fin 2))x:↑Vy:↑V⊢ (∃ n, 0 < n ∧ dist x y = ↑n) → ∃ n, 0 < n ∧ dist y x = ↑n simp [dist_comm]All goals completed! 🐙
  loopless.irrefl x := byα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αV:Set (EuclideanSpace ℝ (Fin 2))x:↑V⊢ ¬∃ n, 0 < n ∧ dist x x = ↑n
    rintro ⟨n, hn, h⟩α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αV:Set (EuclideanSpace ℝ (Fin 2))x:↑Vn:ℕhn:0 < nh:dist x x = ↑n⊢ False
    rw [dist_self,α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αV:Set (EuclideanSpace ℝ (Fin 2))x:↑Vn:ℕhn:0 < nh:0 = ↑n⊢ Falseα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αV:Set (EuclideanSpace ℝ (Fin 2))x:↑Vn:ℕhn:0 < nh:n = 0⊢ False eq_comm,α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αV:Set (EuclideanSpace ℝ (Fin 2))x:↑Vn:ℕhn:0 < nh:↑n = 0⊢ Falseα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αV:Set (EuclideanSpace ℝ (Fin 2))x:↑Vn:ℕhn:0 < nh:n = 0⊢ False Nat.cast_eq_zeroα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αV:Set (EuclideanSpace ℝ (Fin 2))x:↑Vn:ℕhn:0 < nh:n = 0⊢ Falseα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αV:Set (EuclideanSpace ℝ (Fin 2))x:↑Vn:ℕhn:0 < nh:n = 0⊢ False] at hα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αV:Set (EuclideanSpace ℝ (Fin 2))x:↑Vn:ℕhn:0 < nh:n = 0⊢ False
    liaAll goals completed! 🐙

open scoped EuclideanGeometry

G can be embedded in ℝ^n with every edge a unit line segment if there is an injective map from the vertices of G to ℝ^n sending any two adjacent vertices to points at distance 1.

def UnitDistanceEmbeddable {V : Type*} (G : SimpleGraph V) (n : ℕ) : Prop :=
  ∃ f : V → ℝ^n, Function.Injective f ∧ ∀ u v : V, G.Adj u v → dist (f u) (f v) = 1

G has dimension n: the least m for which G embeds in ℝ^m with every edge a unit line segment.

def HasDimension {V : Type*} (G : SimpleGraph V) (n : ℕ) : Prop :=
  IsLeast {m | UnitDistanceEmbeddable G m} n

end SimpleGraph