-- =============================================================================
-- GOLDBACH LEAN PROJECT - VERSION CONSOLIDÉE FINALE
-- Denise Vella-Chemla
-- =============================================================================

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic.Omega

-- =============================================================================
-- PARTIE 1 : GRAPHE PONDÉRÉ
-- =============================================================================

namespace GoldbachGraph

variable (n : ℕ)

structure SommetGraphe where
  p : ℕ
  q : ℕ
  dans_triangle : q ≥ p ∧ q ≤ n ∧ p ≤ n

def excentricite (s : SommetGraphe n) : ℕ :=
  Nat.max (2 * n - s.p - s.q) (s.p + s.q)

def EstCentreGraphe (s : SommetGraphe n) : Prop :=
  excentricite n s = n

theorem ligne_centre_implique_excentricite_n (s : SommetGraphe n) (h_ligne : s.p + s.q = n) :
  EstCentreGraphe n s := by
  dsimp [EstCentreGraphe, excentricite]
  rw [h_ligne]
  exact Nat.max_self n

theorem excentricite_n_implique_ligne_centre (s : SommetGraphe n) (h_centre : EstCentreGraphe n s) :
  s.p + s.q = n := by
  dsimp [EstCentreGraphe, excentricite] at h_centre
  
  have h_upper : s.p + s.q ≤ n := by
    calc
      s.p + s.q ≤ (2 * n - s.p - s.q).max (s.p + s.q) := Nat.le_max_right _ _
      _ = n := h_centre
  
  have h_lower : n ≤ s.p + s.q := by
    by_contra h
    have h_lt : s.p + s.q < n := by
      apply lt_of_not_ge
      exact h
    have : n < (2 * n - s.p - s.q).max (s.p + s.q) := by
      have h_sub_gt : n < 2 * n - s.p - s.q := by omega
      have h_le_max : 2 * n - s.p - s.q ≤ (2 * n - s.p - s.q).max (s.p + s.q) := Nat.le_max_left _ _
      apply lt_of_lt_of_le h_sub_gt h_le_max
    rw [h_centre] at this
    exact lt_irrefl n this
  
  exact Nat.le_antisymm h_upper h_lower

end GoldbachGraph

-- =============================================================================
-- PARTIE 2 : INVOLUTION ET SYMÉTRIE
-- =============================================================================

namespace GoldbachSymmetry

def involution (n : ℕ) (p : ℕ) : ℕ := n - p

theorem involution_involutive (n p : ℕ) (hp : p ≤ n) :
  involution n (involution n p) = p := by
  rw [involution, involution]
  rw [Nat.sub_sub_self hp]

theorem symmetry_about_half (n p q : ℕ) (h_sum : p + q = n) (h_order : p ≤ n / 2) :
  n / 2 - p = q - n / 2 := by
  have h_q_def : q = n - p := by omega
  rw [h_q_def]
  omega

-- Exemples de test
example : involution 10 3 = 7 := by simp [involution]; rfl
example : involution 10 7 = 3 := by simp [involution]; rfl

end GoldbachSymmetry

-- =============================================================================
-- PARTIE 3 : TESTS CONCRETS
-- =============================================================================

#eval GoldbachSymmetry.involution 10 3  -- 7
#eval GoldbachSymmetry.involution 10 7  -- 3