Reference · Analysis

rainbow.math.analysis.geometric-threshold

Analysissrc/rainbow/math/analysis/geometric_threshold.clj0 definitions, 1 theorems

The first fully-general-over-n convergence statement for the geometric contraction: for the worked start distance d0 = 8 and threshold eps = 1, the distance is at most 1 at EVERY step from the modulus 3 onward: forall n. (3 <= n) -> seq 8 n <= 1. This is `convergence/converges-to` specialised to a concrete (d0, eps) with the explicit modulus 3 -- no longer a finite list of worked instances but a single theorem covering all n past the modulus. The proof unpacks the order witness n = 3 + extra (proposition/use-witness on nat/at-most), commutes it to extra + 3 (algebra/nat-add-commutative), bounds seq 8 (extra + 3) <= seq 8 3 by the monotone-convergence bridge (geometric/seq-decreases-with-iteration), chains with the worked seq 8 3 <= 1 through nnrat/at-most-transitive, and transports the bound back along n = extra + 3 with equality/substitution. The remaining generalisation -- arbitrary d0 and eps with a computed modulus -- needs the archimedean/2^n bound and is tracked separately.

geometric/reaches-one-after-step-3 :
  (n : ℕ)
  (bound : 3 ≤ n)
  → geometric/seq 8 n ≤ 1