CanonicalAmplitudeNormalization
plain-language theorem explainer
Amplitude is a positive scalar gauge on the minimal closed-scale orbit: the unit-amplitude framework is the canonical reference, every positive amplitude is its scalar multiple, and levelwise equality with the unit orbit holds exactly at amplitude 1. Anyone citing the T5→T6 self-similarity bridge or hierarchy dynamics uses this certificate. It is a three-field Prop bundle (definition), not a proved theorem.
Claim. For a positive real amplitude $a>0$ and a fixed minimal hierarchy, a canonical amplitude-normalization certificate asserts three facts: (i) the unit-amplitude closed framework admits a minimal-orbit realization bridge (unique fixed-data realization projecting to the minimal closed-scale orbit and matching the canonical sequence); (ii) for every level index $k$, the amplitude-$a$ orbit levels equal $a$ times the unit-amplitude levels; (iii) the amplitude-$a$ levels agree with the unit levels for all $k$ if and only if $a=1$.
background
The Unified Forcing Chain module aims to force T0–T8 from the Recognition Composition Law plus normalization and calibration. Between unique $J$ (T5) and forced $\varphi$ (T6) sits hierarchy dynamics on closed observable frameworks: discrete scale orbits must be realized and compared without smuggling extra structure.
A minimal hierarchy packages the least closed scale data used by the orbit constructions. The minimal-orbit realization bridge certifies that a fixed-data realization is unique, projects to the minimal closed-scale orbit, and agrees with the canonical sequence-level orbit. Amplitude enters as a positive real scalar multiplying those levels.
This structure packages the gauge statement: unit amplitude is the reference framework (via the unit bridge), general positive amplitude is homogeneous scaling of that reference, and exact coincidence of orbits pins amplitude to $1$.
proof idea
No proof body: this is a structure (Prop bundle) with three fields. unit_bridge demands a MinimalOrbitRealizationBridge for the canonical unit-amplitude minimal-orbit framework at base state $0$ with amplitude $1$. scaled_levels is the pointwise identity that amplitude-$a$ canonical levels equal $a$ times unit levels. exact_unit_iff is the biconditional that full levelwise equality with the unit orbit holds exactly when $a=1$. A companion Subsingleton instance records propositional uniqueness for fixed data (all certificates equal by rfl). The inhabiting theorem canonical_amplitude_normalization fills the fields from the unit-framework bridge and the scaling lemmas.
why it matters
In the forcing chain, T5 uniqueness of $J$ must connect to T6 self-similarity ($\varphi$ as the discrete ledger fixed point). Downstream, canonical_amplitude_normalization supplies the inhabited certificate, and T5_To_T6_SelfSimilarity_Bridge routes through hierarchy dynamics on closed frameworks with realized hierarchy data. Without amplitude as a pure gauge, scale ratios could be confounded with overall normalization.
The certificate makes that separation explicit: only the unit orbit is canonical; other positive amplitudes are scalar copies; equality forces $a=1$. That keeps the self-similarity ratio intrinsic rather than an artifact of amplitude choice, aligning with the chain’s claim that $\varphi$ is forced once hierarchy is realized, not assumed by a hidden scale convention.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.