realized_uniform_ratios
In a realized hierarchy inside a closed observable framework, every adjacent ratio of level observables equals every other. Recognition Science researchers working on the T5 to T6 bridge cite this to obtain uniform scaling directly from carrier dynamics without external bridge hypotheses. The proof is a one-line wrapper that rewrites each ratio to the common base ratio via the realized_ratio_eq_base lemma.
claimLet $F$ be a closed observable framework and let $H$ be a realized hierarchy of carrier states generated by iterating the dynamics of $F$. Denote by $l_m$ the observable value on the $m$-th iterate of the base state. Then for all natural numbers $j$ and $k$, $l_{j+1}/l_j = l_{k+1}/l_k$.
background
A ClosedObservableFramework consists of a state space $S$, deterministic dynamics $T:S→S$, and positive observable $r:S→ℝ$ satisfying nontriviality and closure (no continuous moduli). A RealizedHierarchy over $F$ is the structure whose levels are defined by $l_k = r(T^{[k]} s_0)$ for base state $s_0$, equipped with the fields levels_pos, growth, ratio_self_similar, and additive_posting. The module replaces earlier external hypotheses on sensitivity and additive composition with these RS-native fields derived from self-similar J-cost dynamics. The upstream lemma realized_ratio_eq_base states that every adjacent ratio equals the base ratio $l_1/l_0$.
proof idea
The term proof fixes $j$ and $k$ by intro, then rewrites both target ratios using the lemma realized_ratio_eq_base applied at $j$ and at $k$, reducing each to the common base ratio $H.levels 1 / H.levels 0$.
why it matters in Recognition Science
The result feeds directly into the definition realized_to_ladder, which constructs a UniformScaleLadder, and into NontrivialMultilevelComposition. It closes the T5→T6 step in the forcing chain by deriving uniform ratios from the self-similar dynamics field of RealizedHierarchy, consistent with the Recognition Composition Law and the phi fixed point. The module doc notes that this replaces the earlier free-floating HasMultilevelComposition interface.
scope and limits
- Does not prove existence of any realized hierarchy.
- Does not fix the numerical value of the common ratio.
- Does not apply outside closed observable frameworks.
- Does not derive self-similarity or additive posting.
Lean usage
noncomputable def example_ladder (F : ClosedObservableFramework) (H : RealizedHierarchy F) : UniformScaleLadder := realized_to_ladder F Hformal statement (Lean)
94theorem realized_uniform_ratios (F : ClosedObservableFramework)
95 (H : RealizedHierarchy F) :
96 ∀ j k, H.levels (j + 1) / H.levels j = H.levels (k + 1) / H.levels k := by
proof body
Term-mode proof.
97 intro j k
98 rw [realized_ratio_eq_base F H j, realized_ratio_eq_base F H k]
99
100/-- Construct a `UniformScaleLadder` from a realized hierarchy. -/