Reference · Rationals

rainbow.math.rational.value

Rationalssrc/rainbow/math/rational/value.clj0 definitions, 8 theorems

Exact nonnegative-rational worked values, proven through cross-product equivalence rather than pair equality. `nnrat/multiply` and `nnrat/add` are not definitionally reducible to a canonical `nnrat/make` pair, so a worked value like `1/2 * 1 = 1/2` cannot be proven by reflexivity on the pair. It CAN be proven on the equivalence relation: `nnrat/equivalent l r` is defined as the nat equality `numerator(l) * denominator(r) = numerator(r) * denominator(l)`, and nat multiplication does reduce, so each worked value below discharges by reflexivity on the reduced cross-product. This packages the reusable pattern: any exact rational worked value in an algorithm proof (cooling factors, learning rates, importance ratios, ...) should be stated with `nnrat/equivalent` and proven the same way, then carried by `nnrat/multiply-respects-equivalence` / `nnrat/add-respects-equivalence`.

rvalue/half-times-one :
  → nnrat/half · 1 = nnrat/half

rvalue/half-times-half :
  → nnrat/half · nnrat/half = nnrat/quarter

rvalue/half-plus-half :
  → nnrat/half + nnrat/half = 1

rvalue/quarter-plus-quarter :
  → nnrat/quarter + nnrat/quarter = nnrat/half

rvalue/one-times-quarter :
  → 1 · nnrat/quarter = nnrat/quarter

rvalue/one-over-half :
  → nnrat/divide 1 nnrat/half = 2

rvalue/half-over-quarter :
  → nnrat/divide nnrat/half nnrat/quarter = 2

rvalue/quarter-over-half :
  → nnrat/divide nnrat/quarter nnrat/half = nnrat/half