RealizedClosedScaleModel
plain-language theorem explainer
Physicists deriving hierarchy fields from scale primitives cite RealizedClosedScaleModel when a closed observable framework orbit matches a closed geometric scale sequence. It assembles a base state, positive amplitude, the sequence with closure and growth ratio exceeding one, plus the explicit realization equation linking the observable to scaled iterates. The structure definition packages these components directly with no separate derivation steps.
Claim. Let $F$ be a closed observable framework. A realized closed scale model for $F$ consists of a base state $s_0$ in the state space of $F$, a positive real amplitude $A > 0$, a closed geometric scale sequence with ratio $r > 1$, and the condition that the observable of $F$ applied to the $k$-fold iterate of the transition on $s_0$ equals $A$ times the $k$-th scale value, for every natural number $k$.
background
ClosedObservableFramework supplies a state space $S$, transition map $T$, positive observable $r$, and nontriviality, modeling closed systems with countable states and no external input. GeometricScaleSequence carries a positive ratio not equal to one together with a scale function, where isClosed asserts invariance under ledgerCompose. The module isolates the case in which an orbit realizes an earlier closed geometric scale sequence, making the ratio self-similarity and additive posting fields of RealizedHierarchy theorems rather than assumptions. Upstream, scale is defined as powers of phi and baseState appears in obstruction constructions.
proof idea
This is a structure definition. It requires supplying a base state, a positive amplitude, a geometric scale sequence that is closed and satisfies growth ratio greater than one, and verifying the realization equation for all iterates. No lemmas or tactics are applied; the declaration simply records the fields and their constraints.
why it matters
The structure feeds toRealizedHierarchy and thereby supports the bridge theorem from T5 to T6 with no extra hierarchy assumptions. It fulfills the module goal of converting earlier scale primitives into derived properties. The open question left explicit in the module documentation is proving existence of such a realized closed scale model from ClosedObservableFramework alone. It connects directly to geometric scaling and the phi-forcing steps in the Recognition chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.