realized_ratio_eq_base
plain-language theorem explainer
Realized hierarchies inside closed observable frameworks have every consecutive level ratio equal to the base ratio levels(1)/levels(0). Derivations of uniform scaling from self-similar J-cost dynamics cite this to close the carrier-to-observable bridge. The proof is a short induction that applies the ratio_self_similar field at each successor step.
Claim. Let $F$ be a closed observable framework and $H$ a realized hierarchy in $F$. Then for every natural number $k$, the ratio of consecutive level observables satisfies $H.levels(k+1)/H.levels(k) = H.levels(1)/H.levels(0)$.
background
A closed observable framework consists of a state space $S$, deterministic dynamics $T:S→S$, and positive observable $r:S→ℝ$ with at least two distinct values. A realized hierarchy augments this with a base state whose iterates define levels $ℓ(k)=r(T^k base)$, satisfying positivity, growth $ℓ(1)/ℓ(0)>1$, the self-similar ratio property $ℓ(k+2)/ℓ(k+1)=ℓ(k+1)/ℓ(k)$, and additive posting $ℓ(2)=ℓ(1)+ℓ(0)$. This module embeds the hierarchy directly into the framework, replacing external bridge hypotheses with native fields derived from J-cost self-similarity.
proof idea
Proof by induction on $k$. The base case $k=0$ holds by reflexivity. In the successor case, the ratio_self_similar property of the realized hierarchy rewrites the target ratio, after which the induction hypothesis identifies it with the base ratio.
why it matters
This theorem is invoked by realized_uniform_ratios to conclude that all adjacent ratios coincide. It supplies the uniform scaling needed for the phi-ladder in the T5 J-uniqueness to T6 phi fixed-point step of the forcing chain. The module doc notes that self-similar dynamics follows from J-cost invariance under scale phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.