constant_ratio
plain-language theorem explainer
constant_ratio defines the property that a sequence K from naturals to reals obeys K at ell plus one equals r times K at ell for every ell. Researchers on phi-hierarchy growth cite it to establish self-similarity in cache cost models. The declaration is a direct encoding of the constant ratio condition used as a hypothesis in forcing theorems.
Claim. The function $K : ℕ → ℝ$ satisfies the constant ratio property with value $r$ when $K(ℓ + 1) = r · K(ℓ)$ for every natural number $ℓ$.
background
The Local Cache module develops machine-verified results on optimal caching hierarchies that minimize access costs under assumptions A1-A3. constant_ratio captures the self-similarity condition on the sequence K of costs or bridge ratios across levels ℓ. Upstream, K is the dimensionless bridge ratio defined non-circularly as $K = ϕ^{1/2}$, while cost functions derive from J-cost in ObserverForcing and derived costs on positive ratios in MultiplicativeRecognizerL4.
proof idea
constant_ratio is introduced as a definition that directly states the universal property ∀ ℓ, K(ℓ+1) = r * K ℓ. No lemmas or tactics are invoked in its declaration; it functions as an assumption in theorems such as fibonacci_ratio_forces_golden that combine it with fibonacci_recurrence to obtain the quadratic equation for r.
why it matters
This definition provides the self-similarity hypothesis required by the φ-OPTIMAL HIERARCHY THEOREM (Theorem 4.2) stated in fibonacci_partition_forces_phi. It also supports phi_hierarchy_is_unique_fixed_point and no_alternative_ratio. Within Recognition Science it instantiates the self-similar fixed point at T6 of the forcing chain, confirming that the hierarchy must adopt the golden ratio to satisfy both Fibonacci partitioning and constant ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.