RealizedClosedScaleModel
A structure that packages a base state, positive amplitude, and closed geometric scale sequence inside a ClosedObservableFramework so the observable on the iterated orbit recovers the scaled sequence exactly. Researchers deriving hierarchy fields from scale primitives would cite it to turn ratio self-similarity and additive posting into theorems. The definition assembles the seven fields directly with no lemmas or tactics.
claimLet $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 real amplitude $a$, and a geometric scale sequence with ratio $r>1$ that is closed, such that the observable of $F$ applied to the $k$-fold iterate of the transition map on $s$ equals $a$ times the $k$-th term of the scale sequence, for every natural number $k$.
background
A ClosedObservableFramework comprises a countable state space $S$, a transition map $T$, and a positive observable $r$ that takes at least two distinct values, enforcing closure and finite description with no external input. GeometricScaleSequence supplies a positive ratio not equal to one together with a scale function; upstream results identify this scale with powers of phi. The module isolates the strongest derivation currently available: if an orbit realizes such a closed sequence, then the two target fields of RealizedHierarchy become theorems rather than assumptions.
proof idea
Direct structure definition. The seven fields are stated explicitly: base state, amplitude with positivity, the scale sequence, its closure property, the growth condition on the ratio, and the realization equation that equates the observable on the orbit to the scaled sequence.
why it matters in Recognition Science
Supplies the hypothesis that converts ratio self-similarity and additive posting into derived theorems, which in turn feed the bridge_T5_T6_from_realized_closed_scale result that derives the T5 to T6 step of the forcing chain from earlier scale primitives. The module documentation records the remaining open question of existence from ClosedObservableFramework alone. In the Recognition framework this packaging supports the transition from geometric scale sequences to hierarchy fields without extra assumptions.
scope and limits
- Does not prove existence of any RealizedClosedScaleModel from ClosedObservableFramework alone.
- Does not admit continuous moduli or external inputs.
- Does not treat non-closed scale sequences.
- Does not compute explicit numerical values for amplitude or ratio.
formal statement (Lean)
33structure RealizedClosedScaleModel (F : ClosedObservableFramework) where
34 baseState : F.S
35 amplitude : ℝ
36 amplitude_pos : 0 < amplitude
37 scales : GeometricScaleSequence
38 scales_closed : scales.isClosed
39 growth : 1 < scales.ratio
40 realize : ∀ k, F.r (F.T^[k] baseState) = amplitude * scales.scale k
41
42/-- In any geometric scale sequence, each adjacent ratio equals the
43base ratio. -/