RealizedClosedScaleModel
plain-language theorem explainer
A structure that packages an orbit of a ClosedObservableFramework realizing a closed geometric scale sequence with positive amplitude and ratio exceeding one. Researchers deriving hierarchy fields from scale primitives cite it to convert realization data into proved self-similarity and additive posting. The definition assembles the required fields directly with no internal proof obligations.
Claim. Let $F$ be a closed observable framework. A realized closed scale model for $F$ consists of a base state $s$ in the state space of $F$, a positive amplitude $a>0$, a geometric scale sequence with ratio $r>1$ that is closed, and the condition that the observable of $F$ satisfies $F.r(F.T^k s)=a$ times the $k$-th scale term for every natural number $k$.
background
ClosedObservableFramework is a structure with state space $S$, transition $T$, and positive observable $r$ obeying nontriviality, closure under the dynamics, and finite description with countable states. GeometricScaleSequence supplies a positive ratio not equal to one together with a scale function returning the $n$-th term. The module isolates the strongest honest derivation supported by the codebase: when an orbit realizes an earlier GeometricScaleSequence closed under ledgerCompose, the ratio_self_similar and additive_posting fields of RealizedHierarchy become theorems rather than assumptions. The module documentation states that what remains open is proving existence of such a model from ClosedObservableFramework alone. Upstream, scale is defined noncomputably as phi to the power $k$.
proof idea
This is a structure definition that directly collects the fields baseState, amplitude with its positivity proof, scales together with its closure and growth conditions, and the realize predicate. No lemmas or tactics are invoked inside the declaration.
why it matters
The structure supplies the input to the parent theorems bridge_T5_T6_from_realized_closed_scale, additive_posting_of_realized_closed_scale, ratio_self_similar_of_realized_closed_scale, realized_closed_scale_ratio_step, and toRealizedHierarchy. It converts the realization condition into derived hierarchy fields, closing the gap described in the module documentation between ClosedObservableFramework and RealizedHierarchy. It touches the open existence question and sits inside the forcing chain at the T5 J-uniqueness to T6 phi step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.