-- Squared complex modulus and its Euclidean geometry, without square roots (ZF).
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Complex.Norm
import Field
import Geometry.Plane

theorem complex.point (z : Set)
  requires member : z ∈ complexCarrier
  shows Euclidean.Point(z)
proof
  obtain ⟨a, aReal, b, bReal, coordinates⟩ := complexCarrier.cases at z with *
  rw coordinates
  exact Euclidean.pair.point with *

theorem complex.of_point (z : Euclidean.Point)
  shows z ∈ complexCarrier
proof
  have coordinates := Euclidean.coordinates at z with *
  rw coordinates
  exact complexCarrier.pair with *

def complexNormSquared (z : Euclidean.Point) : Real := Euclidean.normSquared(z)

theorem complexNormSquared.real (z : Set)
  requires member : z ∈ complexCarrier
  shows Real(complexNormSquared(z))
proof
  have point := complex.point with *
  unfold complexNormSquared
  exact Euclidean.normSquared.real with *

theorem complexNormSquared.pair (a b : Real)
  shows complexNormSquared((a, b)) = a * a + b * b
proof
  have horizontal := Euclidean.x.pair at a, b with *
  have vertical := Euclidean.y.pair at a, b with *
  simp [complexNormSquared, Euclidean.normSquared, Euclidean.dot]

theorem complexNormSquared.nonnegative (z : Set)
  requires member : z ∈ complexCarrier
  shows 0 ≤ complexNormSquared(z)
proof
  have point := complex.point with *
  unfold complexNormSquared
  exact Euclidean.normSquared.nonnegative with *

theorem complexNormSquared.zero_iff (z : Set)
  requires member : z ∈ complexCarrier
  shows complexNormSquared(z) = 0 ↔ z = complexZero
proof
  obtain ⟨a, aReal, b, bReal, coordinates⟩ := complexCarrier.cases at z with *
  have norm := complexNormSquared.pair at a, b with *
  have vanishing := complex.norm_zero_iff at a, b with *
  rw [coordinates, norm]
  constructor
  . intro zeroNorm
    have parts := vanishing.forward with zeroNorm
    unfold complexZero
    cc
  . intro zeroPoint
    unfold complexZero at zeroPoint
    have parts := orderedPair.injective with zeroPoint
    rw [parts.left, parts.right]
    ring

theorem complexNormSquared.positive (z : Set)
  requires member : z ∈ complexCarrier
  requires nonzero : z ≠ complexZero
  shows 0 < complexNormSquared(z)
proof
  have nonnegative := complexNormSquared.nonnegative with *
  have nonvanishing : complexNormSquared(z) ≠ 0
    intro zeroNorm
    have zeroPoint := complexNormSquared.zero_iff.forward with *
    exact nonzero with zeroPoint
  exact Real.positive_of_nonnegative_of_ne_zero with *

section Arithmetic
notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)
notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)

theorem complexNormSquared.zero
  shows complexNormSquared(ℂ[0]) = R[0]
proof
  unfold complexZero
  rw complexNormSquared.pair
  ring

theorem complexNormSquared.one
  shows complexNormSquared(ℂ[1]) = R[1]
proof
  unfold complexOne
  rw complexNormSquared.pair
  ring

theorem complexNormSquared.mul (z w : Set)
  requires first : z ∈ ℂ
  requires second : w ∈ ℂ
  shows complexNormSquared(ℂ[z * w]) = R[complexNormSquared(z) * complexNormSquared(w)]
proof
  obtain ⟨a, aReal, b, bReal, zPair⟩ := complexCarrier.cases at z with *
  obtain ⟨c, cReal, d, dReal, wPair⟩ := complexCarrier.cases at w with *
  rw [zPair, wPair, complexMul.pair, complexNormSquared.pair, complexNormSquared.pair, complexNormSquared.pair]
  ring

theorem complexNormSquared.neg (z : Set)
  requires member : z ∈ ℂ
  shows complexNormSquared(ℂ[-z]) = complexNormSquared(z)
proof
  obtain ⟨a, aReal, b, bReal, coordinates⟩ := complexCarrier.cases at z with *
  rw [coordinates, complexNeg.pair, complexNormSquared.pair, complexNormSquared.pair]
  ring

theorem complexNormSquared.parallelogram (z w : Set)
  requires first : z ∈ ℂ
  requires second : w ∈ ℂ
  shows R[complexNormSquared(ℂ[z + w]) + complexNormSquared(ℂ[z - w])] = R[2 * (complexNormSquared(z) + complexNormSquared(w))]
proof
  obtain ⟨a, aReal, b, bReal, zPair⟩ := complexCarrier.cases at z with *
  obtain ⟨c, cReal, d, dReal, wPair⟩ := complexCarrier.cases at w with *
  rw [zPair, wPair]
  simp [complexAdd.pair, complexNeg.pair, complexNormSquared.pair]
  ring

theorem complexNormSquared.add_bound (z w : Set)
  requires first : z ∈ ℂ
  requires second : w ∈ ℂ
  shows complexNormSquared(ℂ[z + w]) ≤ R[2 * (complexNormSquared(z) + complexNormSquared(w))]
proof
  have field := complexes.is_field
  have ring := IsField.comm_ring with field
  have ordinary := IsCommRing.ring with ring
  have negated := IsRing.neg_closed with ordinary, second
  have difference := IsRing.add_closed with ordinary, first, negated
  have sum := IsRing.add_closed with ordinary, first, second
  have nonnegative := complexNormSquared.nonnegative with difference
  have identity := complexNormSquared.parallelogram with first, second
  have bound := realLe.add_left at realZero, complexNormSquared(ℂ[z - w]), complexNormSquared(ℂ[z + w]) with *
  rwa [realAddValue.zero_right, identity] at bound

theorem complexNormSquared.perturbation (z w : Set)
  requires first : z ∈ ℂ
  requires second : w ∈ ℂ
  shows complexNormSquared(ℂ[z + w]) = R[complexNormSquared(z) + 2 * Euclidean.dot(z, w) + complexNormSquared(w)]
proof
  obtain ⟨a, aReal, b, bReal, zPair⟩ := complexCarrier.cases at z with *
  obtain ⟨c, cReal, d, dReal, wPair⟩ := complexCarrier.cases at w with *
  rw [zPair, wPair]
  simp [complexAdd.pair, complexNormSquared.pair, Euclidean.dot, Euclidean.x.pair, Euclidean.y.pair]
  ring

theorem complexNormSquared.strict_descent (z w : Set)
  requires first : z ∈ ℂ
  requires second : w ∈ ℂ
  requires descent : R[2 * Euclidean.dot(z, w) + complexNormSquared(w)] < R[0]
  shows complexNormSquared(ℂ[z + w]) < complexNormSquared(z)
proof
  have pointZ := complex.point at z with *
  have pointW := complex.point at w with *
  have decreasing := realLess.add_left at R[2 * Euclidean.dot(z, w) + complexNormSquared(w)], realZero, complexNormSquared(z) with *
  have identity := complexNormSquared.perturbation at z, w with *
  have regroup : complexNormSquared(ℂ[z + w]) = R[complexNormSquared(z) + (2 * Euclidean.dot(z, w) + complexNormSquared(w))]
    rw identity
    ring
  rwa [← regroup, realAddValue.zero_right] at decreasing

end Arithmetic