Contraction
plain-language theorem explainer
Contraction structures encode mappings that reduce distance to the unit state at a uniform rate strictly between zero and one. Researchers modeling R-hat attractors on finite lattices cite this definition to set up convergence arguments for J-cost reductions. The declaration assembles five fields that directly enforce the contraction inequality with no additional lemmas required.
Claim. A contraction consists of a function $step : ℝ → ℝ$ and rate $r ∈ ℝ$ such that $0 < r < 1$ and $|step(x) - 1| ≤ r |x - 1|$ holds for every $x > 0$.
background
The module develops existence and uniqueness conditions for R-hat attractors on finite lattices, where R-hat functions as a J-cost contraction. J-cost is the functional $J(x) = (x + x^{-1})/2 - 1$ from the unified forcing chain, and the step operation is supplied by global application of a local cellular automaton rule. The structure records the contraction rate together with the bound that forces distance to the fixed point at 1 to decrease at each iteration.
proof idea
The declaration is a structure definition with no proof body. It directly lists the five fields: the step map, the rate value, positivity of the rate, the rate being less than one, and the contraction inequality that must hold for all positive inputs.
why it matters
This definition supplies the hypothesis type for the convergence theorem contraction_converges in the same module. It supports the module's key results that R-hat converges on finite lattices to the unique global J-cost minimum at the unit state, linking to J-uniqueness in the forcing chain and the determination of thought vocabulary by the number of fixed points. It addresses how lattice topology can produce additional local minima beyond the global one.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.