contraction_converges
plain-language theorem explainer
The theorem shows that for any contraction c with rate r in (0,1) and any initial x0 > 0, the distance to the fixed point at 1 after n >= 1 steps satisfies r^n |x0 - 1| < |x0 - 1| unless x0 already equals 1. Researchers modeling R-hat attractors on lattices in Recognition Science cite it to bound error decay in J-cost dynamics. The proof uses case split on whether x0 equals 1, then applies the power inequality for rates strictly below one to the absolute deviation.
Claim. Let $c$ be a contraction on the positive reals with contraction rate $r$ satisfying $0 < r < 1$ and $|c(x) - 1| ≤ r |x - 1|$ for all $x > 0$. For any $x_0 > 0$ and natural number $n ≥ 1$, $r^n |x_0 - 1| < |x_0 - 1|$ or $x_0 = 1$.
background
The module develops R-hat fixed-point theory for J-cost contractions on finite lattices. R-hat denotes the recognition operator whose cost is given by the defect functional, which equals the J-cost J(x) for positive x. A Contraction structure packages a step map together with a rate r in (0,1) that strictly contracts distance to the fixed point at unity: |step x - 1| ≤ r |x - 1| whenever x > 0. Upstream results supply the cost maps: defect from LawOfExistence, derivedCost from MultiplicativeRecognizerL4, and the J-cost of recognition events from ObserverForcing. The local setting is that contractions on finite graphs converge to fixed points whose number and structure fix the thought vocabulary of the intelligence.
proof idea
The tactic proof splits on whether x0 equals 1. The right branch returns the equality hypothesis. The left branch first obtains strict positivity of the initial deviation via abs_pos, then shows r^n < 1 by chaining pow_le_pow_of_le_one (using rate_pos and rate_lt_one together with n > 0) down to r < 1, and finally applies mul_lt_of_lt_one_left to the positive deviation.
why it matters
This result closes the convergence step inside R-hat fixed-point theory, directly supporting the sibling claims that the global J-cost minimum is unique at x = 1 and that fixed points are local minima. It instantiates the general fact that J-cost contractions on finite structures reach the T5 J-uniqueness fixed point. The module records zero sorrys, so the lemma removes an open convergence question for lattice-based recognition models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.