canonicalMinimalOrbitLevels_scaled_from_unit
plain-language theorem explainer
Any real amplitude scales the canonical minimal-orbit level sequence by simple multiplication against the unit-amplitude sequence. Normalization and amplitude-certificate arguments cite this identity. The proof unfolds the level definition and closes by ring arithmetic.
Claim. For every real amplitude $a$, every minimal discrete hierarchy $H$ (a geometric scale ladder closed under the first nontrivial composition step), and every level index $k$, the canonical minimal-orbit level at amplitude $a$ equals $a$ times the canonical minimal-orbit level at unit amplitude: $\mathrm{level}(a,H,k)=a\cdot\mathrm{level}(1,H,k)$.
background
The ambient module is the Unified Forcing Chain: T-1 through T8 are derived as inevitabilities from the Recognition Composition Law plus normalization and calibration, rather than assumed as compatible structure. Within that chain one needs a discrete geometric scale ladder.
A minimal hierarchy is exactly such a ladder: a geometric scale sequence closed under the first nontrivial composition step (the Fibonacci-type closure). Canonical minimal-orbit levels assign, to an amplitude and such a hierarchy, a real sequence indexed by level. The unit case is the same construction at amplitude $1$.
Upstream scaffolding includes the native unit predicate on finite $\delta$-orbits (only the one-step orbit is a multiplicative unit), canonical completed traces that repeat the primitive distinction act, and related canonical arithmetic and measure objects. Those fix what "canonical" means; this lemma only records the amplitude homogeneity of the level map.
proof idea
Fix the level index $k$. Unfold the definition of the canonical minimal-orbit level map at the given amplitude and at unit amplitude. After unfolding, both sides are identical up to the explicit scalar factor amplitude, so the equality is a ring identity. No hierarchy lemmas or positivity hypotheses are required; the proof is pure definitional linearity.
why it matters
Downstream, canonical_amplitude_normalization builds the canonical amplitude-normalization certificate for positive amplitudes on a minimal hierarchy. That certificate needs a clean bridge from arbitrary positive amplitude to the unit orbit; this scaling identity is the algebraic step that makes the bridge exact rather than approximate.
In the forcing-chain narrative the lemma is bookkeeping, not a new physical force. It keeps orbit-level data homogeneous so later normalization (and any comparison against the unit canonical orbit) does not smuggle extra scale dependence. It sits under the T0–T8 inevitability program in this module: once levels are well-defined on minimal hierarchies, amplitude is a free positive scalar that factors out cleanly before certificates about unit structure are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.