canonical_amplitude_normalization
plain-language theorem explainer
For any positive real amplitude and any minimal discrete hierarchy, there is a canonical amplitude-normalization certificate: the unit-amplitude minimal orbit is realized, every positive-amplitude orbit is that unit orbit scaled by the amplitude, and exact coincidence with the unit orbit holds if and only if the amplitude is 1. Cited by the T5→T6 self-similarity bridge. The proof is a three-field structure constructor wiring three prior orbit lemmas.
Claim. Let $a > 0$ be a real amplitude and let $H$ be a minimal discrete hierarchy (a geometric scale ladder closed under the first nontrivial composition step). Then the canonical amplitude-normalization certificate holds for $(a,H)$: the unit-amplitude minimal-orbit framework realizes the canonical unit orbit; for every level $k$, the $a$-amplitude canonical orbit level equals $a$ times the unit-amplitude level; and the $a$-amplitude orbit equals the unit orbit at every level if and only if $a = 1$.
background
The module UnifiedForcingChain aims to force the full T0–T8 chain from the Recognition Composition Law plus normalization and calibration. T5 pins the unique cost $J$; T6 forces $\varphi$ as the self-similar fixed point of a discrete ledger hierarchy.
A MinimalHierarchy is a geometric scale sequence closed under the first nontrivial composition step (the Fibonacci-type closure). Amplitude here is a positive scalar gauge on the canonical minimal orbit: the unit-amplitude framework is the reference, and every other positive amplitude is treated as a pure rescaling of that reference.
Upstream, three facts are already proved: the unit-amplitude framework realizes the canonical unit orbit through the minimal-orbit bridge; any positive-amplitude canonical orbit is the unit orbit multiplied by the amplitude; and exact equality with the unit orbit holds precisely when the amplitude is already $1$. The structure CanonicalAmplitudeNormalization packages those three facts as a single certificate.
proof idea
Term-mode structure construction, not a tactic script. The three fields of CanonicalAmplitudeNormalization are filled by direct application of three lemmas:
unit_bridge:=canonicalUnitMinimalOrbitFramework_bridge minimal(unit framework realizes the canonical unit orbit).scaled_levels:=canonicalMinimalOrbitLevels_scaled_from_unit amplitude minimal(positive-amplitude levels are amplitude times unit levels).exact_unit_iff:=canonicalMinimalOrbitLevels_eq_unit_iff_amplitude_one amplitude minimal(orbit identity with the unit case iff amplitude $= 1$).
No extra algebraic work occurs at this site; the theorem is the certificate assembler.
why it matters
This certificate is the gauge-normalization step that lets the forcing chain treat amplitude as a pure scalar redundancy rather than a free physical parameter. Downstream it is consumed by T5_To_T6_SelfSimilarity_Bridge and the theorem t5_to_t6_bridge_holds, which assert that the T5→T6 self-similarity bridge is theorem-backed: a closed observable framework with a realized hierarchy forces the scale ratio to be $\varphi$.
In the primer landmarks, that is exactly the T5 (unique $J$) to T6 ($\varphi$ forced) link. Without a unit-canonical orbit and the scaling/exactness facts, self-similarity could smuggle an unfixed overall scale. Packaging them here keeps the bridge free of hidden amplitude choices and aligns with the module claim that every level of the chain is forced, not merely compatible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.