Reference · Signed rationals

rainbow.math.rational.signed.absolute

Signed rationalssrc/rainbow/math/rational/signed/absolute.clj1 definitions, 5 theorems

Native absolute value for signed rational proof data. `signed/absolute x` is the lattice expression `max x (-x)`. It bounds both orientations of `x`, is nonnegative by decidable total-order case analysis, and is at most a threshold exactly when both linear deviation rows are. This is the scalar prerequisite for signed-vector distances and quantitative affine contraction. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.signed.deviation-rows

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

signed/absolute-unfold :
  (value : ℚ)
  → signed/absolute value = signed/max value (signed/negate value)

signed/at-most-absolute :
  (value : ℚ)
  → value ≤ signed/absolute value

signed/negate-at-most-absolute :
  (value : ℚ)
  → signed/negate value ≤ signed/absolute value

signed/absolute-nonnegative :
  (value : ℚ)
  → 0 ≤ signed/absolute value

signed/absolute-bounded-iff-deviation-rows :
  (value threshold : ℚ)
  → proposition/conjunction (signed/absolute value ≤ threshold → conjunction) (conjunction → signed/absolute value ≤ threshold)
  where conjunction := proposition/conjunction (value ≤ threshold) (signed/negate value ≤ threshold)