canonicalMinimalOrbitLevels_eq_unit_iff_amplitude_one
plain-language theorem explainer
Exact pointwise equality between the amplitude-scaled canonical minimal orbit levels and the unit-amplitude levels holds if and only if the amplitude is already 1. Anyone normalizing the discrete hierarchy gauge before the amplitude-normalization certificate will cite this. The proof is a two-line iff: specialize at index 0 and unfold the geometric scale, or rewrite by amplitude = 1.
Claim. Let $A \in \mathbb{R}$ be an amplitude and let $H$ be a minimal discrete hierarchy (a geometric scale ladder closed under the first nontrivial composition step). Write $L(A,H,k)$ for the $k$-th canonical minimal orbit level at amplitude $A$. Then $\forall k,\, L(A,H,k) = L(1,H,k)$ if and only if $A = 1$.
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. Inside that chain one works with a minimal discrete hierarchy: a geometric scale sequence (ratio $r > 0$, $r \neq 1$) closed under the first nontrivial composition step, which is the Fibonacci relation on scales.
Canonical minimal orbit levels package that ladder together with a real amplitude scalar. The amplitude is a positive gauge factor on the orbit; the unit-amplitude choice is the intended canonical representative. The geometric scale at index $k$ is the usual power $r^k$ (or $\varphi^k$ once $\varphi$ is forced), so the amplitude multiplies into the level data and is visible already at $k = 0$.
Upstream structure used here is exactly that minimal hierarchy and its geometric scale sequence; the present statement isolates when the scaled orbit coincides with the unit orbit.
proof idea
Term-mode constructor on the biconditional.
Forward: from $\forall k$ equality, specialize at $k = 0$. Unfold the definition of the canonical minimal orbit levels and the geometric scale map; simpa recovers $A = 1$ because the amplitude sits as the leading factor at the base index.
Reverse: assume $A = 1$, introduce arbitrary $k$, and rewrite; both sides become the unit-amplitude levels.
why it matters
This is the exactness half of the amplitude gauge story in the forcing chain. Downstream it is consumed by canonical_amplitude_normalization, the certificate that amplitude is a positive scalar gauge: the unit-amplitude framework is canonical, and every positive-amplitude framework is its scalar multiple.
In framework terms it sits after hierarchy minimality and $\varphi$-forcing derived scales (T6 territory), before the packaged normalization used by later chain steps. It does not itself force $\varphi$, the eight-tick octave, or $D = 3$; it only pins when the orbit levels have already been reduced to the unit gauge. Without this iff, the normalization certificate would lack the uniqueness direction that unit amplitude is the unique amplitude giving the unit orbit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.