canonical_unit_amplitude_pos
plain-language theorem explainer
Unit amplitude, the real scalar 1, is strictly positive. Anyone assembling the canonical unit-amplitude minimal-orbit closed framework cites this as the positivity witness. The proof is a one-line numerical check that 0 < 1 on the reals.
Claim. As real numbers, $0 < 1$. Equivalently, the unit amplitude scalar is strictly positive.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law together with normalization $F(1)=0$ and calibration $F''(1)=1$. Downstream of that chain, observable frameworks are closed under a minimal-orbit hierarchy, and amplitudes enter as positive real gauges on those frameworks.
Unit amplitude means the scalar $1$ in that gauge. The surrounding definitions package a closed observable framework at a chosen positive amplitude; the unit case is the canonical representative, with every other positive-amplitude framework a scalar multiple of it. Related upstream objects (canonical arithmetic, dyadic protocols, completed traces, orbit units) fix the discrete ledger side; this lemma only supplies the real inequality needed to instantiate the amplitude slot at $1$.
proof idea
Term-mode proof discharged by norm_num: the goal $0 < (1:\mathbb{R})$ is a ground numerical fact on the reals, with no lemmas from the forcing chain required.
why it matters
This positivity certificate is the amplitude hypothesis for the canonical unit-amplitude minimal-orbit framework: that definition applies the general minimal-orbit constructor at amplitude $1$ with this proof. The matching bridge theorem then shows that framework realizes the canonical unit orbit (orbit index $0$, amplitude $1$).
It also feeds the structure CanonicalAmplitudeNormalization, which certifies that amplitude is a positive scalar gauge: the unit-amplitude framework is canonical, and every positive-amplitude framework is its scalar multiple. In the forcing-chain narrative this is bookkeeping after T5–T8 (unique $J$, $\varphi$, eight-tick, $D=3$), not a new forcing step; it pins the gauge so closed frameworks can be compared without amplitude drift.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.