ConvergenceRate
plain-language theorem explainer
The ConvergenceRate structure packages a real number r with 0 ≤ r < 1 to serve as the contraction factor for iterative J-cost reduction on the recognition landscape for an n-variable formula. Researchers bounding iteration counts in spectral analyses of SAT or J-cost minimization would cite it when linking the Laplacian gap to geometric convergence speed. The definition is a direct packaging of the two inequalities with no lemmas or reduction steps.
Claim. A real number $r$ satisfying $0 ≤ r < 1$ that acts as the contraction factor for gradient-descent reduction of J-cost below a tolerance ε on the landscape induced by a multiplicative recognizer for formulas with n variables.
background
J-cost is the cost function induced by a multiplicative recognizer, given by the derived cost of its comparator on positive ratios, and equivalently the J-cost of any recognition event. The module treats the spectral gap λ₂ of the J-cost Laplacian as the quantity that controls how quickly the recognition process R̂ converges to the minimum under gradient-descent dynamics on that landscape. Upstream structures supply the J-cost definition from PhiForcingDerived and the discrete φ-tier organization of physical quantities from NucleosynthesisTiers.
proof idea
This is a definition that directly constructs the structure with the rate field together with the two field proofs rate_lt_one and rate_nonneg. No lemmas are applied and no tactics are used; the object is a pure packaging of the rate bounds.
why it matters
The definition supplies the geometric rate object required by iteration_bound_from_clauses to scale iteration count with m/λ. It fills the convergence-rate slot in the spectral-gap analysis of the J-cost Laplacian, connecting the phi-forcing and multiplicative-recognizer machinery to the eight-tick octave and D=3 spatial structure of the Recognition framework. It touches the open Cheeger-type inequality left as a sorry in unsat_has_spectral_gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.