realized_ratio_eq_base
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of any realized hierarchy.
- Does not derive the self-similar ratio property from the functional equation.
- Does not apply inside frameworks admitting continuous moduli.
- Does not compute explicit numerical level values.
Lean usage
rw [realized_ratio_eq_base F H j, realized_ratio_eq_base F H k]formal statement (Lean)
83theorem realized_ratio_eq_base (F : ClosedObservableFramework)
84 (H : RealizedHierarchy F) :
85 ∀ k, H.levels (k + 1) / H.levels k = H.levels 1 / H.levels 0 := by
proof body
Term-mode proof.
86 intro k
87 induction k with
88 | zero => rfl
89 | succ k ih =>
90 have h := H.ratio_self_similar k
91 rw [h, ih]
92
93/-- All adjacent ratios in a realized hierarchy are equal. -/