constant_ratio
plain-language theorem explainer
The constant-ratio property states that a sequence K from naturals to reals obeys K(ℓ+1) = r · K(ℓ) for every natural ℓ. Researchers proving self-similar cache hierarchies cite this definition to derive that Fibonacci recurrences force the ratio r to equal φ. The definition is a direct universal quantification with no lemmas or reductions.
Claim. A sequence $K : ℕ → ℝ$ has constant ratio $r$ when $K(ℓ+1) = r · K(ℓ)$ for all $ℓ ∈ ℕ$.
background
In the Local Cache module the sequence K tracks partition sizes or access costs across hierarchy levels ℓ. The constant-ratio property encodes self-similarity of the hierarchy. MODULE_DOC states the main results are local_cache_benefit and fibonacci_partition_forces_phi, which combine this property with the Fibonacci recurrence to force φ. Upstream, cost is defined as J-cost in ObserverForcing and as derivedCost in MultiplicativeRecognizerL4; the constant K from Constants is the separate bridge ratio φ^{1/2}.
proof idea
The declaration is a direct definition via the single universal quantifier ∀ ℓ, K(ℓ+1) = r * K ℓ. No lemmas are applied; it is a one-line wrapper that supplies the self-similarity hypothesis for downstream theorems.
why it matters
This definition supplies the self-similarity hypothesis for fibonacci_partition_forces_phi (Theorem 4.2) and the variants no_alternative_ratio, phi_hierarchy_is_unique_fixed_point, and phiHierarchy_unique. It fills the self-similar fixed point step (T6) in the forcing chain by enabling the algebraic derivation r² = r + 1 under the Fibonacci recurrence. DOWNSTREAM_RESULTS quote it as the rigorous replacement for hand-wavy self-similar cost arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.