| /- |
| Copyright (C) 2026 HCALC contributors |
| SPDX-License-Identifier: AGPL-3.0-only |
|
|
| Minimal Real stub (no Mathlib). Infrastructure Gap-Real-arith only. |
| Production domain symbols are defs in other modules (PRODUCTION.md). |
| -/ |
|
|
| namespace Hcalc |
|
|
| axiom Real : Type |
| axiom realZero : Real |
| axiom realOne : Real |
| axiom realAdd : Real → Real → Real |
| axiom realMul : Real → Real → Real |
| axiom realNeg : Real → Real |
| axiom realAbs : Real → Real |
| axiom realLt : Real → Real → Prop |
| axiom realDiv : Real → Real → Real |
| axiom natToReal : Nat → Real |
| axiom realLog : Real → Real |
| axiom realMin : Real → Real → Real |
| axiom finMax : {n : Nat} → (Fin n → Real) → Real |
|
|
| noncomputable instance : Zero Real := ⟨realZero⟩ |
| noncomputable instance : One Real := ⟨realOne⟩ |
| noncomputable instance : Add Real := ⟨realAdd⟩ |
| noncomputable instance : Mul Real := ⟨realMul⟩ |
| noncomputable instance : Neg Real := ⟨realNeg⟩ |
|
|
| noncomputable def realSub (a b : Real) : Real := realAdd a (realNeg b) |
| noncomputable instance : Sub Real := ⟨realSub⟩ |
|
|
| infix:50 " <ᵣ " => realLt |
| notation "‖" x "‖ᵣ" => realAbs x |
| def realLe (a b : Real) : Prop := realLt a b ∨ a = b |
| infix:50 " ≤ᵣ " => realLe |
|
|
| axiom real_add_comm (a b : Real) : a + b = b + a |
| axiom real_add_assoc (a b c : Real) : (a + b) + c = a + (b + c) |
| axiom real_mul_comm (a b : Real) : a * b = b * a |
| axiom real_mul_assoc (a b c : Real) : (a * b) * c = a * (b * c) |
| axiom real_zero_add (a : Real) : (0 : Real) + a = a |
| axiom real_add_zero (a : Real) : a + (0 : Real) = a |
| axiom real_one_mul (a : Real) : (1 : Real) * a = a |
| axiom real_mul_one (a : Real) : a * (1 : Real) = a |
| axiom real_zero_mul (a : Real) : (0 : Real) * a = (0 : Real) |
| axiom real_mul_zero (a : Real) : a * (0 : Real) = (0 : Real) |
| axiom real_neg_add_cancel (a : Real) : a + (-a) = (0 : Real) |
| axiom real_abs_nonneg (a : Real) : (0 : Real) ≤ᵣ ‖a‖ᵣ |
| axiom real_abs_zero : ‖(0 : Real)‖ᵣ = (0 : Real) |
| axiom real_abs_abs (a : Real) : ‖‖a‖ᵣ‖ᵣ = ‖a‖ᵣ |
| axiom real_lt_irrefl (a : Real) : ¬ (a <ᵣ a) |
| axiom real_lt_asymm {a b : Real} : a <ᵣ b → ¬ b <ᵣ a |
| axiom real_abs_eq_zero_iff (a : Real) : ‖a‖ᵣ = (0 : Real) ↔ a = (0 : Real) |
| axiom real_mul_add (a b c : Real) : a * (b + c) = a * b + a * c |
| axiom real_abs_mul (a b : Real) : ‖a * b‖ᵣ = ‖a‖ᵣ * ‖b‖ᵣ |
| axiom natToReal_pos {n : Nat} (h : 0 < n) : (0 : Real) <ᵣ natToReal n |
| axiom natToReal_zero : natToReal 0 = (0 : Real) |
| axiom natToReal_one : natToReal 1 = (1 : Real) |
| axiom softScaleFactor : Real → Real → Real |
| axiom softScaleFactor_of_le (ε q : Real) |
| (_h : q <ᵣ ((1 : Real) - ε) ∨ q = ((1 : Real) - ε)) : |
| softScaleFactor ε q = (1 : Real) |
| axiom softScaleFactor_of_gt (ε q : Real) |
| (_h : ((1 : Real) - ε) <ᵣ q) : |
| softScaleFactor ε q = realDiv ((1 : Real) - ε) q |
| axiom realMin_le_left (a b : Real) : realMin a b ≤ᵣ a |
| axiom realMin_le_right (a b : Real) : realMin a b ≤ᵣ b |
| axiom finMax_abs_eq_zero_of {n : Nat} (x : Fin n → Real) |
| (h : finMax (fun j => ‖x j‖ᵣ) = (0 : Real)) : ∀ j, x j = (0 : Real) |
| axiom real_contract_force_zero (a q : Real) |
| (hnn : (0 : Real) ≤ᵣ a) (hq : q <ᵣ (1 : Real)) (hle : a ≤ᵣ q * a) : a = (0 : Real) |
| axiom real_le_of_eq (a b : Real) (h : a = b) : a ≤ᵣ b |
| axiom deltaGuard : Real |
| axiom deltaGuard_pos : (0 : Real) <ᵣ deltaGuard |
| axiom tolDefault : Real |
| axiom tolDefault_pos : (0 : Real) <ᵣ tolDefault |
| noncomputable def epsDefault : Real := realDiv realOne (natToReal 20) |
| noncomputable def oneSub (ε : Real) : Real := (1 : Real) - ε |
|
|
| theorem real_sub_self (a : Real) : a - a = (0 : Real) := by |
| change a + (-a) = (0 : Real) |
| exact real_neg_add_cancel a |
|
|
| abbrev Scalar := Real |
|
|
| end Hcalc |
|
|
