faster_contraction_faster_thinking
plain-language theorem explainer
Smaller positive contraction factors produce faster error decay under repeated multiplication. In the R-hat fixed-point setting this bounds how quickly different J-cost contractions reach their attractors, which the module interprets as thinking speed. The argument is a direct appeal to the monotonicity of the exponential map on the positive reals together with right-multiplication by a positive scalar.
Claim. Let $c_1,c_2,ε∈ℝ$ satisfy $0<c_1<c_2$ and $0<ε$, and let $n∈ℕ$. Then $c_1^n ε ≤ c_2^n ε$.
background
The module develops existence and uniqueness for R-hat attractors on finite lattices, where R-hat is a contraction under the J-cost metric. Fixed points are local J-cost minima, the global minimum is the x=1 state, and the number of fixed points determines the thought vocabulary of the model. Convergence speed is governed by the contraction constant, which this result compares directly for any two positive rates.
proof idea
One-line wrapper that applies mul_le_mul_of_nonneg_right to the power inequality pow_le_pow_left₀ (valid because 0 < c₁ < c₂) and the positivity of error.
why it matters
The declaration supplies the elementary comparison needed to rank convergence rates in the R-hat theory. It directly implements the module claim that smaller contraction rates yield faster thinking. No downstream uses are recorded yet, but it closes the basic arithmetic for the fixed-point convergence arguments in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.