canonicalMinimalOrbitFramework
plain-language theorem explainer
Canonical closed observable framework on the naturals carrying a minimal geometric orbit scaled by a positive amplitude. Cited by the T5-to-T6 self-similarity bridge and by minimal-orbit realization lemmas in the unified forcing chain. Construction fills the closed-framework fields directly: successor tick, hierarchy levels, trivial conserved charge, and discreteness via absence of an injection from the reals into the naturals.
Claim. Given an amplitude $a>0$ and a minimal hierarchy, there is a closed observable framework whose state space is $\mathbb{N}$, whose tick is the successor $n\mapsto n+1$, and whose level map is the canonical minimal-orbit sequence scaled by $a$. The framework has strictly positive levels, at least two distinct levels, countable states, no continuous moduli, and identically zero conserved charge.
background
The Unified Forcing Chain module aims to derive T0 through T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. The T5-to-T6 step needs a concrete closed observable framework that already carries a realized discrete hierarchy, so that self-similarity can force the golden ratio $\varphi$ as scale ratio.
A closed observable framework packages a state space $S$, a tick map $T:S\to S$, a positive real level (observable) map $r$, countability of $S$, an obstruction to continuous moduli, and a conserved charge. Hierarchy minimality supplies a geometric scale sequence whose successive ratio is not $1$, together with the discrete posting data used later for self-similarity.
Upstream arithmetic supplies the successor on $\mathbb{N}$ as the free generator of the initial Peano object. The level sequence here is the minimal hierarchy scales multiplied by the chosen amplitude, so the orbit from $0$ is a pure geometric ladder on a countable ledger.
proof idea
Definitional structure package, not a deep proof. State space is $\mathbb{N}$ and tick is Nat.succ. Levels and positivity are delegated to the canonical minimal-orbit level sequence and its positivity lemma. Nontriviality exhibits states $0$ and $1$: if their levels agreed, left-cancellation by $a\neq 0$ would force equal bare scales at $0$ and $1$, contradicting the hierarchy's ratio_ne_one. Countability is witnessed by the identity enumeration. Continuous moduli are ruled out by the standard fact that there is no injection $\mathbb{R}\hookrightarrow\mathbb{N}$. Charge is the zero function; conservation is reflexivity.
why it matters
This is the standard carrier object for minimal-orbit arguments inside the forcing chain. Downstream, canonicalMinimalOrbitFramework_realization shows the target sequence is realized definitionally along the orbit from $0$, and canonicalMinimalOrbitFramework_bridge projects the package into the full minimal-orbit bridge. The unit-amplitude specialization is the default instance used when no extra scale factor is needed.
The T5-to-T6 self-similarity bridge routes through closed frameworks equipped with realized hierarchy data: bare closed-framework fields alone do not force $\varphi$; the hierarchy (ratio self-similarity and additive posting) must be present. This definition supplies that discrete orbit on $\mathbb{N}$ so the bridge can conclude the scale ratio is $\varphi$ (landmark T6) once T5 uniqueness of $J$ is available. It does not itself close T6; it is the canonical input shape those certificates consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.