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

import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Data.Fin.Basic
import Mathlib.Tactic

/-!
# Heron's Formula Seed

This file prepares a proof-facing statement for Heron's formula in coordinates.
The minimum theorem is the geometric formula for the square of twice the signed
area of a triangle in the plane. A small algebraic factorization lemma is
included as route support; it is not the full theorem.
-/

namespace AtlasKnownTheorems.HeronFormula

/-- A concrete point in the real coordinate plane. -/
abbrev Point : Type :=
  Fin 2 → ℝ

/-- Squared Euclidean distance, kept algebraic for route lemmas. -/
def sqDist (p q : Point) : ℝ :=
  (p 0 - q 0) ^ 2 + (p 1 - q 1) ^ 2

/-- Euclidean side length. -/
noncomputable def side (p q : Point) : ℝ :=
  Real.sqrt (sqDist p q)

/-- Twice the signed coordinate area of triangle `p q r`. -/
def twiceSignedArea (p q r : Point) : ℝ :=
  (q 0 - p 0) * (r 1 - p 1) - (q 1 - p 1) * (r 0 - p 0)

/-- Heron's radicand from side lengths. -/
noncomputable def heronRadicand (a b c : ℝ) : ℝ :=
  let s := (a + b + c) / 2
  s * (s - a) * (s - b) * (s - c)

/--
Minimum geometric Heron target in coordinate form. Since
`twiceSignedArea p q r = 2 * orientedArea p q r`, the right side is multiplied
by `4`.
-/
noncomputable def HeronFormulaStatement : Prop :=
  ∀ p q r : Point,
    (twiceSignedArea p q r) ^ 2 =
      4 * heronRadicand (side q r) (side r p) (side p q)

theorem sqDist_nonneg (p q : Point) :
    0 ≤ sqDist p q := by
  dsimp [sqDist]
  nlinarith [sq_nonneg (p 0 - q 0), sq_nonneg (p 1 - q 1)]

/--
Algebraic side-length factorization behind Heron's formula. This is useful
route support, but it does not prove that side lengths came from coordinates.
-/
theorem heron_factor_identity (a b c : ℝ) :
    16 * heronRadicand a b c =
      (a + b + c) * (-a + b + c) * (a - b + c) * (a + b - c) := by
  dsimp [heronRadicand]
  ring

/-- The Heron factor product can be rewritten using only side-length squares. -/
theorem heron_factor_product_sq (a b c : ℝ) :
    (a + b + c) * (-a + b + c) * (a - b + c) * (a + b - c) =
      4 * a ^ 2 * b ^ 2 - (a ^ 2 + b ^ 2 - c ^ 2) ^ 2 := by
  ring

/-- Coordinate determinant identity for the squared side lengths. -/
theorem coordinate_sqdist_identity (p q r : Point) :
    4 * sqDist q r * sqDist r p - (sqDist q r + sqDist r p - sqDist p q) ^ 2 =
      4 * (twiceSignedArea p q r) ^ 2 := by
  dsimp [sqDist, twiceSignedArea]
  ring

/-- The Heron factor product for coordinate side lengths equals four times
the square of twice signed area. -/
theorem coordinate_heron_factor_identity (p q r : Point) :
    (side q r + side r p + side p q) *
        (-side q r + side r p + side p q) *
        (side q r - side r p + side p q) *
        (side q r + side r p - side p q) =
      4 * (twiceSignedArea p q r) ^ 2 := by
  rw [heron_factor_product_sq]
  rw [side, side, side]
  rw [Real.sq_sqrt (sqDist_nonneg q r)]
  rw [Real.sq_sqrt (sqDist_nonneg r p)]
  rw [Real.sq_sqrt (sqDist_nonneg p q)]
  exact coordinate_sqdist_identity p q r

/-- Minimum coordinate Heron theorem. -/
theorem heronFormula :
    HeronFormulaStatement := by
  intro p q r
  have hfactor := heron_factor_identity (side q r) (side r p) (side p q)
  have hcoord := coordinate_heron_factor_identity p q r
  nlinarith

end AtlasKnownTheorems.HeronFormula