-- Squares in the Dedekind real numbers
-- 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.Real.Squares
import Inverse
import Algebra.OrderedField.Core

-- The product of two nonnegative reals is nonnegative.  This is the
-- non-strict companion to the ordered-field positive-product law.
theorem realMulValue.nonnegative (A B : Real)
  requires nonnegativeA : 0 ≤ A
  requires nonnegativeB : 0 ≤ B
  shows 0 ≤ A * B
proof
  have subsetA := realLe.subset with realZero.real, nonnegativeA
  have subsetB := realLe.subset with realZero.real, nonnegativeB
  have valueCut := realMulValue.cut at A, B with *
  have reduction := realMulCut.of_nonnegative with subsetA, subsetB
  apply realLe.of_subset with realZero.real
  rw [valueCut, reduction]
  exact realPosMulCut.nonnegative

instance reals.ordered_ring
  shows OrderedRing(ℝ, realAdd, realZero, realNeg, realMul, realOne, realLe)
proof
  constructor
  . exact reals.comm_ring
  . constructor
    . exact reals.ordered_additive_group
    . constructor
        intros x hx y hy xy yx
        have subsetXY := realLe.subset with xy
        have subsetYX := realLe.subset with yx
        exact Subset.antisymmetric with subsetXY, subsetYX
      . intros x hx y hy nonnegativeX nonnegativeY
        exact realMulValue.nonnegative with nonnegativeX, nonnegativeY

-- The algebraic rearrangement behind multiplicative monotonicity.
theorem realMulValue.add_mul_sub (A B C : Real)
  shows A * C + C * (B - A) = B * C
proof
  have differenceReal := realSubValue.real at B, A with *
  have acReal := realMulValue.real at A, C with *
  have differenceProductReal := realMulValue.real at B - A, C with
    differenceReal, assumption
  have productSwap := realMulValue.commutative at C, B - A with
    assumption, differenceReal
  have distributed := realMulValue.distributive_right at B - A, A, C with
    differenceReal, *{2}
  have cancellation := realSubValue.add_right_cancel at B, A with
    *{2}
  rw cancellation at distributed
  have sumSwap := realAddValue.commutative with acReal, differenceProductReal
  calc
    A * C + C * (B - A) = A * C + (B - A) * C := by cc
    _ = (B - A) * C + A * C := sumSwap
    _ = B * C := by cc

-- Multiplication by a nonnegative real preserves non-strict order.  The proof
-- is the usual difference argument: B = A + (B - A), and C(B - A) is
-- nonnegative.
theorem realLe.mul_right_of_nonnegative (A B C : Real)
  requires ab : A ≤ B
  requires nonnegativeC : 0 ≤ C
  shows A * C ≤ B * C
proof
  have negAReal := realNegValue.real at A
  have differenceReal := realSubValue.real at B, A with *
  have translated := realLe.add_right at A, B, -A with
    *{2}, negAReal, ab
  have inverse := realAddValue.neg_right at A
  rw inverse at translated
  have differenceNonnegative : 0 ≤ B - A
    unfold realSubValue
    exact translated
  have productNonnegative := realMulValue.nonnegative at C, B - A with
    assumption, differenceReal, nonnegativeC, differenceNonnegative
  have productReal := realMulValue.real at C, B - A with
    assumption, differenceReal
  have acReal := realMulValue.real at A, C with *
  have step := realLe.add_left with realZero.real, productReal, acReal, productNonnegative
  have zero := realAddValue.zero_right with acReal
  rw zero at step
  have expansion := realMulValue.add_mul_sub at A, B, C with
    *{3}
  rwa expansion at step

theorem realLe.mul_left_of_nonnegative (A B C : Real)
  requires ab : A ≤ B
  requires nonnegativeC : 0 ≤ C
  shows C * A ≤ C * B
proof
  have result := realLe.mul_right_of_nonnegative with ab, nonnegativeC
  have left := realMulValue.commutative at A, C with *
  have right := realMulValue.commutative at B, C with *
  rwa [left, right] at result

-- The strict companion used in epsilon estimates.
theorem realLess.mul_right_of_positive (A B C : Real)
  requires ab : A < B
  requires positiveC : 0 < C
  shows A * C < B * C
proof
  have negAReal := realNegValue.real at A
  have differenceReal := realSubValue.real at B, A with *
  have translated := realLess.add_right at A, B, -A with
    *{2}, negAReal, ab
  have inverse := realAddValue.neg_right at A
  rw inverse at translated
  have differencePositive : 0 < B - A
    unfold realSubValue
    exact translated
  have productPositive := realMulValue.positive at C, B - A with
    assumption, differenceReal, positiveC, differencePositive
  have productReal := realMulValue.real at C, B - A with
    assumption, differenceReal
  have acReal := realMulValue.real at A, C with *
  have step := realLess.add_left with realZero.real, productReal, acReal, productPositive
  have zero := realAddValue.zero_right with acReal
  rw zero at step
  have expansion := realMulValue.add_mul_sub at A, B, C with
    *{3}
  rwa expansion at step

theorem realLess.mul_left_of_positive (A B C : Real)
  requires ab : A < B
  requires positiveC : 0 < C
  shows C * A < C * B
proof
  have result := realLess.mul_right_of_positive with ab, positiveC
  have left := realMulValue.commutative at A, C with *
  have right := realMulValue.commutative at B, C with *
  rwa [left, right] at result

theorem realInvValue.positive (A : Real)
  requires positive : 0 < A
  shows 0 < realInvValue(A)
proof
  have generic := IsOrderedField.positive_inverse with reals.ordered_field, positive
  unfold realInvValue
  exact generic

-- Reciprocation reverses strict order on the positive reals.
theorem realInvValue.antitone_positive (A B : Real)
  requires positiveA : 0 < A
  requires less : A < B
  shows realInvValue(B) < realInvValue(A)
proof
  have positiveB := realLess.transitive with realZero.real, positiveA, less
  have inverseAPositive := realInvValue.positive with positiveA
  have inverseBPositive := realInvValue.positive with positiveB
  have nonzeroA : A ≠ 0
    intro equal
    rw equal at positiveA
    have irreflexive := realLess.irreflexive_on
    exact irreflexive with realZero, positiveA
  have nonzeroB : B ≠ 0
    intro equal
    rw equal at positiveB
    have irreflexive := realLess.irreflexive_on
    exact irreflexive with realZero, positiveB
  have first := realLess.mul_right_of_positive at
    A, B, realInvValue(A) with
      *{2}, realInvValue.real at A with assumption,
      less, inverseAPositive
  have inverseA := realInvValue.mul_right with nonzeroA
  rw inverseA at first
  have inverseAReal := realInvValue.real at A
  have inverseBReal := realInvValue.real at B
  have bInverseAReal := realMulValue.real at B, realInvValue(A) with
    assumption, inverseAReal
  have second := realLess.mul_left_of_positive with
    realOne.real, bInverseAReal, inverseBReal, first, inverseBPositive
  have inverseB := realInvValue.mul_left with nonzeroB
  have associative := realMulValue.associative at
    realInvValue(B), B, realInvValue(A) with
      inverseBReal, assumption, inverseAReal
  have oneLeft := realMulValue.one_left with inverseAReal
  have oneRight := realMulValue.one_right with inverseBReal
  rwa [oneRight, ← associative, inverseB, oneLeft] at second

-- Every square is nonnegative.  For a nonpositive A, apply the preceding
-- result to -A and use (-A)(-A) = A².
theorem realMulValue.square_nonnegative (A : Real)
  shows 0 ≤ A * A
proof
  have sign := Real.sign_cases at A
  cases sign with nonpositive | nonnegative
  . have negAReal := realNegValue.real at A
    have negANonnegative := realNegValue.nonnegative_of_nonpositive with nonpositive
    have negALe := realLe.of_subset with realZero.real, negANonnegative
    have square := realMulValue.nonnegative with negALe, negALe
    have negSquare := realMulValue.neg_both at A, A with *
    rwa negSquare at square
  . have nonnegativeLe := realLe.of_subset at realZero, A with
      realZero.real, assumption, nonnegative
    exact realMulValue.nonnegative with nonnegativeLe, nonnegativeLe

theorem Real.positive_of_nonnegative_of_ne_zero (A : Real)
  requires nonnegative : 0 ≤ A
  requires nonzero : A ≠ 0
  shows 0 < A
proof
  have subset := realLe.subset with realZero.real, nonnegative
  have zeroNeA : realZero ≠ A
    intro zeroA
    apply nonzero
    cc
  apply realLess.characterization.backward
  unfold RealLess
  refine ⟨realZero.real, assumption, _⟩
  constructor
  . exact subset
  . exact zeroNeA

-- A nonzero square is strictly positive.  This is the order-theoretic heart
-- of the familiar fact that the reals have no nontrivial nilpotents.
theorem realMulValue.square_positive (A : Real)
  requires nonzero : A ≠ 0
  shows 0 < A * A
proof
  have sign := Real.sign_cases at A
  cases sign with nonpositive | nonnegative
  . have negAReal := realNegValue.real at A
    have negANonnegative := realNegValue.nonnegative_of_nonpositive with nonpositive
    have negALe := realLe.of_subset with realZero.real, negANonnegative
    have negANonzero : -A ≠ 0
      intro negAZero
      apply nonzero
      have involutive := realNegValue.involutive at A
      calc
        A = -(-A) := by cc
        _ = -realZero := by cc
        _ = realZero := realNegValue.zero
    have positiveNegA := Real.positive_of_nonnegative_of_ne_zero with negALe, negANonzero
    have positiveSquare := realMulValue.positive with positiveNegA, positiveNegA
    have negSquare := realMulValue.neg_both at A, A with *
    rwa negSquare at positiveSquare
  . have nonnegativeLe := realLe.of_subset at realZero, A with
      realZero.real, assumption, nonnegative
    have positiveA := Real.positive_of_nonnegative_of_ne_zero with nonnegativeLe, nonzero
    exact realMulValue.positive with positiveA, positiveA

theorem realMulValue.square_eq_zero_iff (A : Real)
  shows A * A = 0 ↔ A = 0
proof
  constructor
  . intro squareZero
    by_contra nonzero
    have positive := realMulValue.square_positive with nonzero
    rw squareZero at positive
    have irreflexive := realLess.irreflexive_on
    exact irreflexive with realZero, positive
  . intro zeroA
    rw zeroA
    exact realMulValue.zero_left with realZero.real

theorem realAddValue.sum_squares_nonnegative (A B : Real)
  shows 0 ≤ A * A + B * B
proof
  have squareALe := realMulValue.square_nonnegative at A
  have squareBLe := realMulValue.square_nonnegative at B
  have squareASubset := realLe.subset with realZero.real, squareALe
  have squareBSubset := realLe.subset with realZero.real, squareBLe
  apply realLe.of_subset with realZero.real
  exact realAddValue.nonnegative with squareASubset, squareBSubset

-- A sum of two nonnegative reals can vanish only term by term.
theorem realAddValue.nonnegative_eq_zero (A B : Real)
  requires nonnegativeA : 0 ≤ A
  requires nonnegativeB : 0 ≤ B
  requires zeroSum : A + B = 0
  shows A = 0
proof
  have upper := realLe.add_left at realZero, B, A with
    realZero.real, *{2}, nonnegativeB
  have identity := realAddValue.zero_right at A
  rw [identity, zeroSum] at upper
  have down := realLe.subset at A, realZero with realZero.real, upper
  have up := realLe.subset with realZero.real, nonnegativeA
  exact Subset.antisymmetric with down, up

theorem realLe.of_nonnegative_difference (A B : Real)
  requires nonnegative : 0 ≤ B - A
  shows A ≤ B
proof
  have shifted := realLe.add_right at realZero, B - A, A with *
  have left : (0:R) + A = A
  . ring
  have right : (B - A) + A = B
  . ring
  rwa [left, right] at shifted

theorem realLe.mul_right_cancel_positive (A B C : Real)
  requires positive : 0 < C
  requires multiplied : A * C ≤ B * C
  shows A ≤ B
proof
  by_contra contrary
  have reversed := realLess.of_not_le with *
  have strict := realLess.mul_right_of_positive at B, A, C with *
  have ac := realMulValue.real at A, C with *
  have cycle := realLe.transitive_less with *
  have irreflexive := realLess.irreflexive_on
  have member : A * C ∈ ℝ
  . settle with Real
  exact irreflexive with A * C, cycle

-- A quotient by a positive real is below C once the numerator is below C
-- times the denominator.
theorem realDiv.lt_of_lt_mul (A B C : Real)
  requires positive : 0 < B
  requires below : A < C * B
  shows A / B < C
proof
  have nonzero : B ≠ 0
    intro zero
    linarith
  have nonnegative : (0:R) ≤ B by linarith
  have quotientReal := realDiv.real at A, B with *
  have product := realDiv.mul_right at A, B with nonzero
  by_contra
  have above := realLe.of_not_less at C, A / B with this
  have scaled :=
    realLe.mul_right_of_nonnegative at C, A / B, B with above, nonnegative
  rw product at scaled
  linarith