-- Signed multiplicative inverses and the ordered-field structure of the reals -- 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.Inverse import PositiveInverse -- The total inverse graph sends zero to zero. Away from zero its two clauses -- are the familiar positive reciprocal and the negative of the reciprocal of -- the absolute value. Keeping the sign split here lets all subsequent field -- proofs speak only about multiplication and negation. def realInv : Set := { p ∈ (ℝ × ℝ) | ∃ A ∈ ℝ, ( (A = 0 ∧ p = (A ↦ 0)) ∨ (0 < A ∧ p = (A ↦ positiveRealInvCut(A))) ∨ (A < 0 ∧ p = (A ↦ realNegCut(positiveRealInvCut(realNegCut(A)))))) } theorem realInv.negative_argument_positive (A : Real) requires negative : A < 0 shows 0 < -A proof have negativeView := realLess.characterization.forward with negative have reversedView := RealLess.neg_reverse with negativeView have reversed := realLess.characterization.backward with reversedView have negZero := realNegValue.zero rwa negZero at reversed theorem realInv.relates_zero shows relates(realInv, realZero, realZero) proof unfold relates apply realInv.membership.backward have zeroInReals : realZero ∈ ℝ by exact realZero.real constructor . exact product.pair at realZero, realZero, ℝ, ℝ with zeroInReals, zeroInReals . witness realZero constructor . exact zeroInReals . left constructor . rfl . rfl theorem realInv.relates_positive (A : Real) requires positive : 0 < A shows relates(realInv, A, positiveRealInvCut(A)) proof have inverseReal := positiveRealInvCut.real with positive have realA : A ∈ ℝ by simp [Real] have realInverse : positiveRealInvCut(A) ∈ ℝ by exact inverseReal unfold relates apply realInv.membership.backward constructor . exact product.pair at A, positiveRealInvCut(A), ℝ, ℝ with realA, realInverse . witness A constructor . exact realA . right left constructor . exact positive . rfl theorem realInv.relates_negative (A : Real) requires negative : A < 0 shows relates(realInv, A, realNegCut(positiveRealInvCut(realNegCut(A)))) proof have positiveNegA := realInv.negative_argument_positive with negative have inverseReal := positiveRealInvCut.real with positiveNegA have negInverseReal := realNegValue.real with inverseReal have realA : A ∈ ℝ by simp [Real] have realInverse : realNegCut(positiveRealInvCut(realNegCut(A))) ∈ ℝ unfold Real at negInverseReal simpa [realNegValue.cut] using negInverseReal unfold relates apply realInv.membership.backward constructor . exact product.pair at A, realNegCut(positiveRealInvCut(realNegCut(A))), ℝ, ℝ with realA, realInverse . witness A constructor . exact realA . right right constructor . exact negative . rfl theorem realInv.total shows TotalBetween(realInv, ℝ, ℝ) proof intros A realA have zeroCases : A = realZero ∨ A ≠ realZero by_contra neither apply neither right intro equal apply neither left exact equal cases zeroCases with zero | nonzero . witness realZero constructor . exact realZero.real . rw zero exact realInv.relates_zero . have connected := realLess.connected_on have signs := connected with A, realA, realZero, nonzero cases signs with negative | positive . have positiveNegA := realInv.negative_argument_positive with negative have inverseReal := positiveRealInvCut.real with positiveNegA have negInverseReal := realNegValue.real with inverseReal have cutInverseReal : Real( realNegCut(positiveRealInvCut(realNegCut(A)))) simpa [realNegValue.cut] using negInverseReal witness realNegCut(positiveRealInvCut(realNegCut(A))) constructor exact cutInverseReal . exact realInv.relates_negative with negative . have inverseReal := positiveRealInvCut.real with positive witness positiveRealInvCut(A) constructor exact inverseReal . exact realInv.relates_positive with positive theorem realInv.negative_mul_eq_one (A : Real) requires negative : A < 0 shows realMulValue(A, realNegCut(positiveRealInvCut(realNegCut(A)))) = realOne proof have negAReal := realNegValue.real at A have positiveNegA := realInv.negative_argument_positive with negative have inverseReal := positiveRealInvCut.real with positiveNegA have positiveLaw := positiveRealInvCut.mul_eq_one with positiveNegA unfold realMulValue at positiveLaw have negatedProduct := realMulValue.neg_both with negAReal, inverseReal have involutiveA := realNegValue.involutive at A rw involutiveA at negatedProduct have law : A * (-positiveRealInvCut(-A)) = realOne rw negatedProduct unfold call2 exact positiveLaw have negACut := realNegValue.cut at A have inverseNegCut := realNegValue.cut with inverseReal rw negACut at inverseNegCut rw [negACut, inverseNegCut] at law unfold call2 at law unfold realMulValue exact law theorem realLess.not_reverse (A B : Real) requires less : A < B shows ¬(B < A) proof intro reverse have cycle := realLess.transitive with less, reverse have irreflexive := realLess.irreflexive_on exact irreflexive with A, cycle theorem realInv.factors (input output : Set) requires mapped : relates(realInv, input, output) shows ∃ A ∈ ℝ, input = A ∧ ((A = 0 ∧ output = realZero) ∨ (0 < A ∧ output = positiveRealInvCut(A)) ∨ (A < 0 ∧ output = realNegCut(positiveRealInvCut(realNegCut(A))))) proof unfold relates at mapped simp [realInv.membership] at mapped rcases mapped with ⟨bounded, A, realA, cases⟩ witness A constructor . exact realA . cases cases with zero | nonzero . rcases zero with ⟨zeroA, shape⟩ obtain ⟨inputA, outputZero⟩ := orderedPair.injective with shape constructor . exact inputA . left constructor . exact zeroA . exact outputZero . cases nonzero with positive | negative . rcases positive with ⟨positiveA, shape⟩ obtain ⟨inputA, outputInverse⟩ := orderedPair.injective with shape constructor . exact inputA . right left constructor . exact positiveA . exact outputInverse . rcases negative with ⟨negativeA, shape⟩ obtain ⟨inputA, outputInverse⟩ := orderedPair.injective with shape constructor . exact inputA . right right constructor . exact negativeA . exact outputInverse theorem realInv.functional shows Functional(realInv) proof intros input y inputY z inputZ obtain ⟨A, realA, inputA, yCases⟩ := realInv.factors with inputY obtain ⟨B, realB, inputB, zCases⟩ := realInv.factors with inputZ have sameInput : A = B by cc rw ← sameInput at zCases cases yCases with yZero | yNonzero . rcases yZero with ⟨zeroA, yShape⟩ cases zCases with zZero | zNonzero . rcases zZero with ⟨zeroAgain, zShape⟩ cc . cases zNonzero with zPositive | zNegative . rcases zPositive with ⟨positiveA, zShape⟩ rw zeroA at positiveA exfalso have impossible := realLess.not_reverse with realZero.real, realZero.real, positiveA exact impossible with positiveA . rcases zNegative with ⟨negativeA, zShape⟩ rw zeroA at negativeA exfalso have impossible := realLess.not_reverse with realZero.real, realZero.real, negativeA exact impossible with negativeA . cases yNonzero with yPositive | yNegative . rcases yPositive with ⟨positiveA, yShape⟩ cases zCases with zZero | zNonzero . rcases zZero with ⟨zeroA, zShape⟩ rw zeroA at positiveA exfalso have impossible := realLess.not_reverse with realZero.real, realZero.real, positiveA exact impossible with positiveA . cases zNonzero with zPositive | zNegative . rcases zPositive with ⟨positiveAgain, zShape⟩ cc . rcases zNegative with ⟨negativeA, zShape⟩ exfalso have impossible := realLess.not_reverse with realZero.real, positiveA exact impossible with negativeA . rcases yNegative with ⟨negativeA, yShape⟩ cases zCases with zZero | zNonzero . rcases zZero with ⟨zeroA, zShape⟩ rw zeroA at negativeA exfalso have impossible := realLess.not_reverse with realZero.real, realZero.real, negativeA exact impossible with negativeA . cases zNonzero with zPositive | zNegative . rcases zPositive with ⟨positiveA, zShape⟩ exfalso have impossible := realLess.not_reverse with realZero.real, positiveA exact impossible with negativeA . rcases zNegative with ⟨negativeAgain, zShape⟩ cc theorem realInv.function shows realInv : ℝ → ℝ proof constructor intros p member obtain ⟨bounded, witnesses⟩ := realInv.membership.forward with member exact bounded . constructor . exact realInv.functional . exact realInv.total -- Real division is the field operation x / y = x * y⁻¹. Its graph is -- obtained from the generic field construction, so `/` is selected by the -- same notation machinery as `+` and `*`. def realDiv : Set := fieldDiv(ℝ, realMul, realInv) theorem realDiv.function shows realDiv : ℝ × ℝ → ℝ proof unfold realDiv exact fieldDiv.function with realMul.function, realInv.function instance realDiv.operation shows DivOperation(ℝ, realDiv) proof exact realDiv.function notation infixl 70 "/" => call2 via DivOperation(ℝ, _) for Real def realInvValue (A : Real) : Real := realInv(A) theorem realInvValue.real (A : Real) shows Real(realInvValue(A)) proof have realA : A ∈ ℝ by simp [Real] obtain ⟨B, realB, mapped⟩ := FunctionBetween.exists_value with realInv.function, realA have applied := FunctionBetween.apply_value with realInv.function, mapped unfold realInvValue rw applied exact realB theorem realDiv.eq_mul_inv (A B : Real) shows A / B = A * realInvValue(B) proof have realA : A ∈ ℝ by simp [Real] have realB : B ∈ ℝ by simp [Real] have mapped := fieldDiv.relates with realMul.function, realInv.function, realA, realB have inputInProduct := product.pair with realA, realB have mappedByRealDiv : relates(realDiv, (A, B), realMul(A, realInv(B))) unfold realDiv exact mapped have applied := FunctionBetween.apply_value with realDiv.function, inputInProduct, mappedByRealDiv unfold call2 unfold realInvValue unfold call2 at applied exact applied theorem realDiv.real (A B : Real) shows Real(A / B) proof have realA : A ∈ ℝ by simp [Real] have realB : B ∈ ℝ by simp [Real] have input := product.pair with realA, realB have closed := FunctionBetween.apply_closed with realDiv.function, input unfold call2 exact closed theorem realDiv.zero_left (B : Real) shows 0 / B = 0 proof have inverseReal := realInvValue.real at B calc 0 / B = 0 * realInvValue(B) := realDiv.eq_mul_inv with realZero.real _ = 0 := realMulValue.zero_left at realInvValue(B) with inverseReal theorem realDiv.add_left (A B C : Real) shows (A + B) / C = A / C + B / C proof have inverseReal := realInvValue.real at C have sumReal := realAddValue.real at A, B with * calc (A + B) / C = (A + B) * realInvValue(C) := realDiv.eq_mul_inv with sumReal, assumption _ = A * realInvValue(C) + B * realInvValue(C) := realMulValue.distributive_right at A, B, realInvValue(C) with *{2}, inverseReal _ = A / C + B / C := by simp [realDiv.eq_mul_inv] theorem realDiv.neg_left (A B : Real) shows (-A) / B = -(A / B) proof have negAReal := realNegValue.real at A have inverseReal := realInvValue.real at B calc (-A) / B = (-A) * realInvValue(B) := realDiv.eq_mul_inv with negAReal, assumption _ = -(A * realInvValue(B)) := realMulValue.neg_left at A, realInvValue(B) with assumption, inverseReal _ = -(A / B) := by simp [realDiv.eq_mul_inv] theorem realInvValue.zero shows realInvValue(realZero) = realZero proof have applied := FunctionBetween.apply_value with realInv.function, realInv.relates_zero unfold realInvValue exact applied theorem realInvValue.of_positive (A : Real) requires positive : 0 < A shows realInvValue(A) = positiveRealInvCut(A) proof have mapped := realInv.relates_positive with positive have applied := FunctionBetween.apply_value with realInv.function, mapped unfold realInvValue exact applied theorem realInvValue.of_negative (A : Real) requires negative : A < 0 shows realInvValue(A) = realNegCut(positiveRealInvCut(realNegCut(A))) proof have mapped := realInv.relates_negative with negative have applied := FunctionBetween.apply_value with realInv.function, mapped unfold realInvValue exact applied theorem realInvValue.mul_right (A : Real) requires nonzero : A ≠ 0 shows A * realInvValue(A) = 1 proof have connected := realLess.connected_on have signs := connected with A, realZero, nonzero cases signs with negative | positive . have value := realInvValue.of_negative with negative rw value have law := realInv.negative_mul_eq_one with negative unfold realMulValue at law unfold call2 exact law . have value := realInvValue.of_positive with positive rw value have law := positiveRealInvCut.mul_eq_one with positive unfold realMulValue at law unfold call2 exact law theorem realDiv.self (A : Real) requires nonzero : A ≠ 0 shows A / A = 1 proof calc A / A = A * realInvValue(A) := realDiv.eq_mul_inv with *{2} _ = 1 := realInvValue.mul_right at A with nonzero -- Multiplication by a nonzero denominator cancels division. theorem realDiv.mul_left (A B : Real) requires nonzero : B ≠ 0 shows B * (A / B) = A proof have inverseReal := realInvValue.real at B have inverseLaw := realInvValue.mul_right with nonzero have oneA := realMulValue.one_left at A have associateBA := realMulValue.associative at B, A, realInvValue(B) with *{2}, inverseReal have commuteBA := realMulValue.commutative at B, A with *{2} have associateAB := realMulValue.associative at A, B, realInvValue(B) with *{2}, inverseReal have inverseProductReal := realMulValue.real at B, realInvValue(B) with assumption, inverseReal have commuteProduct := realMulValue.commutative at A, B * realInvValue(B) with assumption, inverseProductReal calc B * (A / B) = B * (A * realInvValue(B)) := by simp [realDiv.eq_mul_inv] _ = (B * A) * realInvValue(B) := by cc _ = (A * B) * realInvValue(B) := by cc _ = A * (B * realInvValue(B)) := by cc _ = (B * realInvValue(B)) * A := commuteProduct _ = 1 * A := by simp [inverseLaw] _ = A := oneA theorem realDiv.mul_right (A B : Real) requires nonzero : B ≠ 0 shows (A / B) * B = A proof have quotientReal := realDiv.real at A, B with * have commute := realMulValue.commutative at A / B, B with quotientReal, assumption calc (A / B) * B = B * (A / B) := commute _ = A := realDiv.mul_left at A, B with nonzero -- Two quotients agree once the cross products agree. theorem realDiv.eq_of_cross (P Q D E : Real) requires nonzeroQ : Q ≠ 0 requires nonzeroE : E ≠ 0 requires cross : D * Q = E * P shows P / Q = D / E proof have leftView := realDiv.eq_mul_inv at P, Q have rightView := realDiv.eq_mul_inv at D, E have invQ := realInvValue.real at Q have invE := realInvValue.real at E have unitQ := realInvValue.mul_right with nonzeroQ have unitE := realInvValue.mul_right with nonzeroE rw [leftView, rightView] linear_combination (D * realInvValue(E)) * unitQ - (realInvValue(Q) * realInvValue(E)) * cross - (P * realInvValue(Q)) * unitE -- A factor in the numerator may be pulled outside division. theorem realDiv.mul_numerator_left (A B C : Real) shows (A * B) / C = A * (B / C) proof have productReal := realMulValue.real at A, B with * have inverseReal := realInvValue.real at C have associate := realMulValue.associative at A, B, realInvValue(C) with *{2}, inverseReal have wholeDivision := realDiv.eq_mul_inv at A * B, C with productReal, assumption have factorDivision := realDiv.eq_mul_inv at B, C with *{2} calc (A * B) / C = (A * B) * realInvValue(C) := wholeDivision _ = A * (B * realInvValue(C)) := associate _ = A * (B / C) := by cc theorem realInvValue.mul_left (A : Real) requires nonzero : A ≠ 0 shows realInvValue(A) * A = 1 proof have inverseReal := realInvValue.real at A have commutative := realMulValue.commutative at realInvValue(A), A with inverseReal, assumption have right := realInvValue.mul_right with nonzero calc realInvValue(A) * A = A * realInvValue(A) := commutative _ = 1 := right theorem reals.multiplicative_inverse shows MultiplicativeInverse(ℝ, realMul, realZero, realOne, realInv) proof constructor . exact realInv.function . intros A realA nonzero have left := realInvValue.mul_left with nonzero have right := realInvValue.mul_right with nonzero unfold realInvValue at left unfold realInvValue at right constructor . unfold call2 unfold call2 at left exact left . unfold call2 unfold call2 at right exact right instance reals.field shows IsFieldWithInverse(ℝ, realAdd, realZero, realNeg, realMul, realOne, realInv) proof constructor . exact reals.comm_ring . constructor . exact reals.nontrivial . exact reals.multiplicative_inverse instance reals.ordered_field shows IsOrderedField( ℝ, realAdd, realZero, realNeg, realMul, realOne, realInv, realLess) proof constructor . exact reals.field . constructor . exact realLess.strict_linear_order . constructor . exact realAdd.strict_mono . exact realMul.positive theorem realInvValue.nonzero (A : Real) requires nonzero : A ≠ 0 shows realInvValue(A) ≠ 0 proof have inverseLaw := realInvValue.mul_right with nonzero intro inverseZero have zeroProduct := realMulValue.zero_right at A rw [inverseZero, zeroProduct] at inverseLaw apply realZero.ne_one exact inverseLaw -- A right inverse of a nonzero real is the inverse. This tiny uniqueness -- lemma keeps later reciprocal calculations close to their handwritten form. theorem realInvValue.eq_of_mul_right (A B : Real) requires nonzero : A ≠ 0 requires inverseLaw : A * B = 1 shows B = realInvValue(A) proof have inverseReal := realInvValue.real at A have canonical := realInvValue.mul_left with nonzero have associative := realMulValue.associative at realInvValue(A), A, B with inverseReal, *{2} have oneLeft := realMulValue.one_left at B have oneRight := realMulValue.one_right with inverseReal calc B = 1 * B := by cc _ = (realInvValue(A) * A) * B := by cc _ = realInvValue(A) * (A * B) := associative _ = realInvValue(A) * 1 := by cc _ = realInvValue(A) := oneRight theorem realInvValue.mul (A B : Real) requires nonzeroA : A ≠ 0 requires nonzeroB : B ≠ 0 shows realInvValue(A * B) = realInvValue(A) * realInvValue(B) proof have inverseAReal := realInvValue.real at A have inverseBReal := realInvValue.real at B have productReal := realMulValue.real at A, B with * have inverseA := realInvValue.mul_right with nonzeroA have inverseB := realInvValue.mul_right with nonzeroB have inverseALeft := realInvValue.mul_left with nonzeroA have productNonzero : A * B ≠ 0 intro productZero have zeroLeft := realMulValue.zero_right with inverseAReal have associative := realMulValue.associative at realInvValue(A), A, B with inverseAReal, *{2} have oneLeft := realMulValue.one_left at B apply nonzeroB cc have commute := realMulValue.commutative at B, realInvValue(A) with assumption, inverseAReal have candidateLaw : (A * B) * (realInvValue(A) * realInvValue(B)) = 1 have oneMul := realMulValue.one_left with realOne.real have oneLeftB := realMulValue.one_left at B have oneRightA := realMulValue.one_right at A have oneRightInverseA := realMulValue.one_right with inverseAReal have assocABInvA := realMulValue.associative at A, B, realInvValue(A) with *{2}, inverseAReal have assocAInvAB := realMulValue.associative at A, realInvValue(A), B with assumption, inverseAReal, assumption have assocOuter := realMulValue.associative with productReal, inverseAReal, inverseBReal have assocFinal := realMulValue.associative at A, B, realInvValue(B) with *{2}, inverseBReal calc (A * B) * (realInvValue(A) * realInvValue(B)) = ((A * B) * realInvValue(A)) * realInvValue(B) := by cc _ = (A * (B * realInvValue(A))) * realInvValue(B) := by cc _ = (A * (realInvValue(A) * B)) * realInvValue(B) := by cc _ = ((A * realInvValue(A)) * B) * realInvValue(B) := by cc _ = (1 * B) * realInvValue(B) := by cc _ = B * realInvValue(B) := by cc _ = 1 := inverseB have unique := realInvValue.eq_of_mul_right with productNonzero, candidateLaw calc realInvValue(A * B) = realInvValue(A) * realInvValue(B) := by cc