canonicalMinimalOrbitLevels
plain-language theorem explainer
Defines the canonical sequence-level orbit: each natural index k maps to amplitude times the k-th geometric scale of a minimal hierarchy. Anyone building closed observable frameworks or amplitude-normalization certificates on the minimal orbit cites this target sequence. The body is a one-line pointwise product; no proof obligations.
Claim. Given an amplitude $A \in \mathbb{R}$ and a minimal discrete hierarchy $H$ (a geometric scale ladder closed under the first nontrivial composition step), the canonical sequence-level orbit is the map $k \mapsto A \cdot s_H(k)$ from $\mathbb{N}$ to $\mathbb{R}$, where $s_H$ is the geometric scale sequence of $H$.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Within that chain one needs a concrete target sequence that a closed observable framework can realize on the countable state space $\mathbb{N}$.
A minimal hierarchy is a geometric scale ladder closed under the first nontrivial composition step (the Fibonacci-type closure). Its scale sequence supplies the rung heights; in RS settings those scales are typically powers of $\varphi$, though the definition here is parametric in any such hierarchy.
Amplitude is treated as a positive scalar gauge: the unit-amplitude orbit is the canonical representative, and every positive-amplitude orbit is its scalar multiple. This definition packages that product as the realizable target sequence; embedding it into a closed observable framework is a separate finite-description step.
proof idea
Pure definitional abbreviation: the function sends each $k$ to the product of the given amplitude with the $k$-th entry of the hierarchy's geometric scale sequence. No lemmas, tactics, or obligations; noncomputable only because the ambient real arithmetic is.
why it matters
This is the target sequence that the canonical minimal-orbit closed framework carries on $\mathbb{N}$. Downstream, the realization theorem states that framework realizes this sequence definitionally along the orbit from $0$; positivity and unit-scaling lemmas pin the amplitude gauge; and the amplitude-normalization certificate uses it to assert that every positive-amplitude framework is a scalar multiple of the unit one.
In the forcing-chain narrative it sits after hierarchy minimality and before the closed-framework bridge: once $\varphi$ and the discrete ladder are forced (T6 and the ledger/discreteness steps), one still needs an explicit orbit to realize. The doc-comment flags the remaining gap: embedding this sequence into a closed observable framework is a separate finite-description problem, not discharged here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.