canonicalUnitMinimalOrbitFramework
plain-language theorem explainer
Specializes the canonical minimal-orbit closed observable framework to unit amplitude. Anyone fixing the positive scalar gauge on observables cites this as the reference instance. The body is a one-line application of the general minimal-orbit constructor at amplitude 1 with the unit-positivity witness.
Claim. Given a minimal discrete hierarchy $H$ (a geometric scale ladder closed under the first nontrivial composition step), there is a closed observable framework obtained by running the canonical minimal-orbit construction at amplitude $1$. The resulting framework has positive-valued observables, a ratio interface, and a conserved charge, and is nontrivial and finitely described.
background
The module UnifiedForcingChain assembles the complete inevitability chain T-1 through T8 from the cost foundation (Recognition Composition Law plus normalization and calibration). Within that chain one needs closed observable frameworks: structures with a state space, a dynamics map, a positive real observable, nontriviality of the observable, and finite description (no continuous moduli).
A minimal hierarchy is a geometric scale ladder closed under the first nontrivial composition step (Fibonacci-type closure). The general constructor builds a closed observable framework from a positive amplitude and such a hierarchy. The unit case is the natural gauge choice: amplitude is a positive scalar redundancy, so amplitude $1$ is the canonical representative.
Upstream, the unit predicate in the orbit-divisibility calculus marks the one-step orbit as the only multiplicative unit in a finite $\delta$-orbit, aligning the amplitude-$1$ choice with the native unit of the discrete ledger.
proof idea
One-line wrapper. It applies the general canonical minimal-orbit framework constructor at amplitude $1$, feeding the positivity lemma for the unit amplitude and the supplied minimal hierarchy. No extra algebraic work: the general constructor already returns a closed observable framework once amplitude positivity and hierarchy minimality are in hand.
why it matters
This definition is the unit-gauge anchor for amplitude normalization in the forcing chain. Downstream, CanonicalAmplitudeNormalization packages the certificate that the unit-amplitude framework is canonical and every positive-amplitude framework is its scalar multiple. The companion bridge theorem states that this unit framework realizes the canonical unit orbit (via the minimal-orbit realization bridge at index $0$ with amplitude $1$).
In the T0–T8 story, observables and recognition sit at T4 and feed the unique $J$ at T5; fixing the amplitude gauge keeps the closed-framework data free of an arbitrary positive scale before $\varphi$ and the eight-tick structure are forced. Without a named unit instance, the normalization certificate and orbit bridge would have no canonical left-hand side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.