toRealizedHierarchy
plain-language theorem explainer
This definition converts a realized closed scale model on a closed observable framework into an instance of the realized hierarchy interface. It supplies the base state directly from the model and derives the remaining fields from scale closure. Workers on the T5-T6 bridge in the forcing chain cite it to obtain a hierarchy with proved rather than assumed self-similarity and additive posting. The construction assembles fields by reflexivity for level equality, the framework positivity axiom, and direct application of two prior closure theorems.
Claim. Let $F$ be a closed observable framework and $H$ a realized closed scale model for $F$. Then there exists a realized hierarchy for $F$ whose base state equals the base state of $H$, whose levels match the observable values under iterated dynamics, whose levels are positive, whose growth ratio equals the scale ratio at step zero, whose ratios are self-similar, and whose additive posting follows from scale closure.
background
A closed observable framework consists of a state space $S$, dynamics $T:S→S$, and positive observable $r:S→ℝ$ with nontriviality. A realized closed scale model augments this with a base state, positive amplitude, and a geometric scale sequence that is closed under ledgerCompose, such that the observable on the orbit equals amplitude times the scale values. The realized hierarchy structure packages a base state together with levels, positivity, growth, self-similar ratios, and additive posting. Upstream, the additive posting theorem states that scale closure yields $r(T^2 s)=r(T s)+r(s)$ for the base state $s$.
proof idea
The definition sets baseState to the model's baseState. Level equality holds by reflexivity. Positivity invokes the framework's r_pos axiom. Growth rewrites via the realized closed scale ratio step at zero and applies the model's growth field. Self-similarity applies the ratio self similar theorem for realized closed scales. Additive posting simplifies the corresponding additive posting theorem via simpa.
why it matters
This supplies the concrete packaging from scale primitives to the hierarchy interface, which is then fed directly into the T5-T6 bridge theorem. It fulfills the module goal of turning ratio_self_similar and additive_posting into derived theorems. It touches the open question of deriving a realized closed scale model from the framework alone and connects to J-uniqueness and the phi fixed point in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.