Reference · Non-negative rationals

rainbow.math.rational.nnrat.contraction-uniqueness

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

Banach fixed-point UNIQUENESS, the collapse half (the convergence half is nnrat-general-contraction). For any rational gamma = a/(a+g) < 1 (a = ap+1, g = gp+1) and any x = nx/dx: nnrat/contraction-collapse : x <= gamma * x -> x ~ 0 i.e. a nonnegative quantity dominated by its own gamma-contraction must be zero. Together with contraction-converges this pins the fixed point: if two fixed points x, y satisfy |x-y| <= gamma*|x-y| then |x-y| ~ 0, so x ~ y -- uniqueness. PROOF (all in the nat cross-product after at-most-to-cross): base(x)(gamma*x) is nx * den(gamma*x) <= (a*nx) * dx. den(gamma*x) = succ(combine (ap+g) dxp) = (a+g)*dx (denominator-combine law), so nat-ring puts it as (a*M + g*M) <= a*M with M = nx*dx. Pad the RHS to a*M + 0 and cancel the a*M prefix (at-most-add-left-cancel): g*M <= 0 -> g*M = 0. g = succ gp reduces g*M to M + gp*M (multiply recurses on the LEFT arg), so sum-zero-left gives M = 0; M = nx*dx = nx + nx*dxp (multiply-successor-right on the right factor), sum-zero-left again gives nx = 0; and nx = 0 collapses the cross-product equivalence nx*1 = 0*dx (RHS reduces since 0*dx = 0). Native and axiom-free; chains nnrat-order-equivalence (to-cross + the nat additive cancellation and sum-zero-left bricks) and nat-ring.

Depends onmath.rational.nnrat.order-equivalence

nnrat/contraction-collapse :
  (ap gp nx dxp : ℕ)
  (h : nnrat/make nx dxp ≤ nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp)) · nnrat/make nx dxp)
  → nnrat/make nx dxp = 0