Reference · Signed rationals

rainbow.math.rational.signed.geometric-bridge

Signed rationalssrc/rainbow/math/rational/signed/geometric_bridge.clj0 definitions, 5 theorems

Bridge exact NNRAT geometry into signed-rational proof data. The Grothendieck embedding `signed/from-nnrat` preserves NNRAT equivalence, order, and multiplication, and reflects order back: a signed comparison between embedded values yields the NNRAT comparison of the originals. These quotient-safe laws identify the native signed half-power recurrence with the existing exact NNRAT sequence `nnrat/geometric-half`. The bridge lets signed vector contraction reuse the established harmonic domination and rate-null machinery rather than duplicating its arithmetic. Native, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-half-iterate-rate

signed/from-nnrat-respects-equivalence :
  (left right : ℚ≥0)
  (same : left = right)
  → signed/from-nnrat left = signed/from-nnrat right

signed/from-nnrat-at-most :
  (left right : ℚ≥0)
  (ordered : left ≤ right)
  → signed/from-nnrat left ≤ signed/from-nnrat right

signed/from-nnrat-at-most-reverse :
  (left right : ℚ≥0)
  (ordered : signed/from-nnrat left ≤ signed/from-nnrat right)
  → left ≤ right

signed/from-nnrat-multiply :
  (left right : ℚ≥0)
  → signed/from-nnrat left · signed/from-nnrat right = signed/from-nnrat (left · right)

signed/half-power-one-geometric :
  (steps : ℕ)
  → signed/half-power-scale steps 1 = signed/from-nnrat (nnrat/geometric-half steps)