constant_ratio
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not enforce positivity of the ratio r or the terms K ℓ.
- Does not include the Fibonacci recurrence relation.
- Does not derive any specific value for r.
- Does not reference J-cost or defect distances explicitly.
formal statement (Lean)
67def constant_ratio (K : ℕ → ℝ) (r : ℝ) : Prop :=
proof body
Definition body.
68 ∀ ℓ : ℕ, K (ℓ + 1) = r * K ℓ
69
70/-- **KEY LEMMA**: Fibonacci recurrence + constant positive ratio → r² = r + 1.
71
72This is the rigorous replacement for the hand-wavy "self-similar cost" argument. -/