Reference · Signed rationals

rainbow.math.rational.signed.rational

Signed rationals src/rainbow/math/rational/signed/rational.clj12 definitions, 4 theorems

Signed rationals as proof data: a pair (positive, negative) of nonnegative rationals denoting positive - negative. Subtraction is expressed with nnrat addition only, so the kernel never needs a primitive subtraction and the nonnegative-rational machinery is reused directly. Equivalence is the Grothendieck relation (p1,n1) ~ (p2,n2) iff p1 + n2 ~ p2 + n1, again additive. This unlocks signed differences (e.g. value of information, descent updates) while keeping every kernel reduction inside the existing exact-rational base.

signed/SignedRational

DefinitionSource, line 60

signed/SignedRational :
  → Type

signed/make

DefinitionSource, line 64

signed/make :
  (x₁ x₂ : ℚ≥0)
  → ℚ

ℚ = signed/SignedRationalℚ≥0 = nnrat/NonnegativeRational

signed/positive

DefinitionSource, line 70

signed/positive :
  (x₁ : ℚ)
  → ℚ≥0

ℚ = signed/SignedRationalℚ≥0 = nnrat/NonnegativeRational

signed/negative

DefinitionSource, line 79

signed/negative :
  (x₁ : ℚ)
  → ℚ≥0

ℚ = signed/SignedRationalℚ≥0 = nnrat/NonnegativeRational

signed/from-nnrat

DefinitionSource, line 88

signed/from-nnrat :
  (x₁ : ℚ≥0)
  → ℚ

ℚ = signed/SignedRationalℚ≥0 = nnrat/NonnegativeRational

signed/zero

DefinitionSource, line 93

signed/zero :
  → ℚ

ℚ = signed/SignedRational

signed/one

DefinitionSource, line 97

signed/one :
  → ℚ

ℚ = signed/SignedRational

signed/add

DefinitionSource, line 101

signed/add :
  (x₁ x₂ : ℚ)
  → ℚ

ℚ = signed/SignedRational

signed/negate

DefinitionSource, line 109

signed/negate :
  (x₁ : ℚ)
  → ℚ

ℚ = signed/SignedRational

signed/subtract

DefinitionSource, line 115

signed/subtract :
  (x₁ x₂ : ℚ)
  → ℚ

ℚ = signed/SignedRational

signed/equivalent

DefinitionSource, line 123

signed/equivalent :
  (x₁ x₂ : ℚ)
  → Prop

ℚ = signed/SignedRational

signed/nonnegative

DefinitionSource, line 132

signed/nonnegative :
  (x₁ : ℚ)
  → Prop

ℚ = signed/SignedRational

signed/positive-of-make

TheoremHolds by unfolding a definitionNo axiomsSource, line 145

signed/positive-of-make :
  (positive negative : ℚ≥0)
  → signed/positive (signed/make positive negative) = positive

= = equality/Eqℚ≥0 = nnrat/NonnegativeRational

signed/negative-of-make

TheoremHolds by unfolding a definitionNo axiomsSource, line 155

signed/negative-of-make :
  (positive negative : ℚ≥0)
  → signed/negative (signed/make positive negative) = negative

= = equality/Eqℚ≥0 = nnrat/NonnegativeRational

signed/subtract-unfold

TheoremHolds by unfolding a definitionNo axiomsSource, line 165

signed/subtract-unfold :
  (left right : ℚ)
  → left - right = signed/make (signed/positive left + signed/negative right) (signed/negative left + signed/positive right)

+ = nnrat/add- = signed/subtract= = equality/Eqℚ = signed/SignedRational

signed/equivalent-reflexive

TheoremFor all inputsNo axiomsSource, line 181

signed/equivalent-reflexive :
  (value : ℚ)
  → value = value

= = signed/equivalent: equality of rational valuesℚ = signed/SignedRational