Reference · Non-negative rationals

rainbow.math.rational.nnrat.inverse-gap-certificate

Non-negative rationalssrc/rainbow/math/rational/nnrat/inverse_gap_certificate.clj0 definitions, 1 theorems

Sharp inverse-gap residual arithmetic directly in NNRAT. If rate + gap = 1, inverse * gap = 1, and distance <= residual + rate*distance, then distance <= inverse*residual. This is the NNRAT counterpart of the signed affine certificate and is the scalar endpoint needed by finite Bellman residual bounds. Because every NNRAT is nonnegative, scaling monotonicity needs no extra sign premise. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.nnrat.add-cancellationmath.rational.nnrat.multiply-monotonemath.rational.nnrat.ringmath.rational.nnrat.identities

nnrat/inverse-gap-residual-bound :
  (distance residual rate gap inverse : ℚ≥0)
  (rate-plus-gap-one : rate + gap = 1)
  (inverse-times-gap-one : inverse · gap = 1)
  (self-bound : distance ≤ residual + rate · distance)
  → distance ≤ inverse · residual