Contraction
Researchers studying R-hat attractors cite the Contraction structure to formalize a map that pulls states toward the unit fixed point at a uniform rate strictly less than one. The structure is invoked whenever convergence of iterated updates on finite lattices must be established. It packages the step map and rate together with the inequality that guarantees J-cost decrease per application.
claimA contraction consists of a function $f : {R} {to} {R}$ and a rate $r {in} {R}$ with $0 < r < 1$ such that $|f(x) - 1| {leq} r |x - 1|$ holds for all $x > 0$.
background
The module develops Q2c on R-hat fixed-point theory: R-hat is realized as a J-cost contraction on a finite lattice, where the J-cost (imported from JcostCore) measures recognition cost of a configuration and the point at unity is the global minimum. The upstream CellularAutomata.step applies a local rule to produce the successor tape, supplying the concrete iteration mechanism abstracted here to a real-valued map. The for structure from UniversalForcingSelfReference records the meta-realization axioms that close the self-reference loop in the forcing chain.
proof idea
The declaration is a structure definition that directly bundles the step function, the contraction rate, and the three required properties (rate positivity, rate less than one, and the contraction inequality). No lemmas or tactics are invoked; the object is introduced to serve as the hypothesis type for later convergence statements.
why it matters in Recognition Science
The structure supplies the hypothesis for the contraction_converges theorem, which shows that iterated application shrinks distance to the fixed point at 1. It thereby supports the module's listed results on existence of fixed points, uniqueness of the global J-cost minimum, and topology-induced local minima. In the framework it implements the contraction step that realizes T5 J-uniqueness and T6 self-similar fixed point on the phi-ladder.
scope and limits
- Does not prove existence of a fixed point for the given step.
- Does not restrict the underlying space to a finite lattice.
- Does not derive the contraction rate from an explicit J-cost formula.
- Does not address multiplicity or stability of fixed points.
formal statement (Lean)
27structure Contraction where
28 step : ℝ → ℝ
29 contraction_rate : ℝ
30 rate_pos : 0 < contraction_rate
31 rate_lt_one : contraction_rate < 1
32 contracts : ∀ x, 0 < x → |step x - 1| ≤ contraction_rate * |x - 1|
33
34/-- Iterated contraction converges: for n >= 1, the error shrinks. -/