realized_closed_scale_ratio_step
Any orbit in a ClosedObservableFramework that realizes a closed geometric scale sequence has constant adjacent ratios equal to the sequence ratio. Researchers deriving hierarchy fields from scale primitives cite it to obtain ratio self-similarity as a theorem. The proof substitutes the realization equation at consecutive steps, cancels the positive amplitude, and reduces to the scale step lemma.
claimLet $F$ be a closed observable framework and $H$ a realized closed scale model of $F$ with base state $b$, positive amplitude $a$, and geometric scale sequence $s$. For every natural number $k$, the ratio $F.r(F.T^{[k+1]} b)/F.r(F.T^{[k]} b)$ equals the fixed ratio of $s$.
background
A ClosedObservableFramework supplies a state space, transition map $T$, and positive observable $r$ with non-triviality. A RealizedClosedScaleModel augments this with a base state, positive amplitude, and a GeometricScaleSequence whose scale values are recovered exactly by the orbit under $T$ scaled by the amplitude; the sequence is required to be closed. The module isolates the strongest derivation currently available, turning the two target fields of RealizedHierarchy into theorems once such a model exists.
proof idea
Apply the realization equation at steps $k+1$ and $k$ to replace both observables by amplitude times the corresponding scale value. Cancel the common positive amplitude factor via mul_div_mul_left. The resulting adjacent scale ratio equals the fixed ratio by the scale_step_ratio lemma.
why it matters in Recognition Science
The result supplies the constant-ratio step required by ratio_self_similar_of_realized_closed_scale and by the packaging into toRealizedHierarchy. It therefore converts the ratio_self_similar field from assumption to theorem, as stated in the module documentation. Within the Recognition framework it supports the self-similar fixed point and the eight-tick octave by confirming invariance of the realized orbit.
scope and limits
- Does not prove existence of a RealizedClosedScaleModel from ClosedObservableFramework alone.
- Does not address additive posting properties.
- Does not apply to non-closed scale sequences.
- Does not bound the numerical value of the ratio.
formal statement (Lean)
53theorem realized_closed_scale_ratio_step
54 (F : ClosedObservableFramework) (H : RealizedClosedScaleModel F) (k : ℕ) :
55 F.r (F.T^[k + 1] H.baseState) / F.r (F.T^[k] H.baseState) = H.scales.ratio := by
proof body
Tactic-mode proof.
56 rw [H.realize (k + 1), H.realize k]
57 have ha : H.amplitude ≠ 0 := ne_of_gt H.amplitude_pos
58 calc
59 H.amplitude * H.scales.scale (k + 1) / (H.amplitude * H.scales.scale k)
60 = H.scales.scale (k + 1) / H.scales.scale k := by
61 rw [mul_div_mul_left _ _ ha]
62 _ = H.scales.ratio := scale_step_ratio H.scales k
63
64/-- Therefore the realized orbit satisfies ratio self-similarity. -/