/-
SPDX-FileCopyrightText: 2026 Advameg, Inc.
SPDX-License-Identifier: Apache-2.0
-/

import Mathlib.Data.Complex.Basic
import Mathlib.Tactic

/-!
# Napoleon Theorem Seed

This file prepares a proof-facing algebraic complex-plane statement for
Napoleon's theorem. The minimum target uses an abstract sixth-root rotation
parameter; the stretch target instantiates it with the usual complex
exponential rotation and adds public geometric diagrams.
-/

namespace AtlasKnownTheorems.NapoleonTheorem

/-- Algebraic condition for a primitive 60-degree rotation parameter. -/
def IsSixtyDegreeRotationParameter (ω : ℂ) : Prop :=
  ω ^ 2 - ω + 1 = 0

/-- The third vertex of the oriented equilateral triangle on side `a b`. -/
def orientedEquilateralApex (ω a b : ℂ) : ℂ :=
  a + ω * (b - a)

/-- Centroid of three complex-plane points. -/
noncomputable def centroid (a b c : ℂ) : ℂ :=
  (a + b + c) / 3

/-- An oriented equilateral relation encoded by a rotation multiplier. -/
def IsEquilateralBy (ω x y z : ℂ) : Prop :=
  z - x = ω * (y - x)

/--
Minimum Napoleon target: if the same 60-degree algebraic rotation is used to
erect equilateral triangles on all three sides, then their centroids again form
an equilateral triangle.
-/
noncomputable def NapoleonTheoremStatement : Prop :=
  ∀ ω a b c : ℂ,
    IsSixtyDegreeRotationParameter ω →
      let ab := orientedEquilateralApex ω a b
      let bc := orientedEquilateralApex ω b c
      let ca := orientedEquilateralApex ω c a
      let cab := centroid a b ab
      let cbc := centroid b c bc
      let cca := centroid c a ca
      IsEquilateralBy (1 - ω) cab cbc cca

theorem centroid_self (z : ℂ) :
    centroid z z z = z := by
  simp [centroid]
  ring

theorem orientedEquilateralApex_self (ω z : ℂ) :
    orientedEquilateralApex ω z z = z := by
  simp [orientedEquilateralApex]

/-- The algebraic centroid relation at the core of Napoleon's theorem. -/
theorem napoleon_centroid_relation (ω a b c : ℂ)
    (hω : IsSixtyDegreeRotationParameter ω) :
    IsEquilateralBy (1 - ω)
      (centroid a b (orientedEquilateralApex ω a b))
      (centroid b c (orientedEquilateralApex ω b c))
      (centroid c a (orientedEquilateralApex ω c a)) := by
  rw [IsSixtyDegreeRotationParameter] at hω
  simp [IsEquilateralBy, centroid, orientedEquilateralApex]
  ring_nf
  have hω_sq : ω ^ 2 = ω - 1 := by
    calc
      ω ^ 2 = (ω ^ 2 - ω + 1) + (ω - 1) := by ring
      _ = 0 + (ω - 1) := by rw [hω]
      _ = ω - 1 := by ring
  rw [hω_sq]
  ring

/-- Checked wrapper for the minimum Napoleon theorem target. -/
theorem napoleonTheorem : NapoleonTheoremStatement := by
  intro ω a b c hω
  exact napoleon_centroid_relation ω a b c hω

/-- Checked statement wrapper for the minimum theorem. -/
theorem napoleonTheorem_statement :
    NapoleonTheoremStatement ↔ NapoleonTheoremStatement := by
  rfl

end AtlasKnownTheorems.NapoleonTheorem