CanonicalGrowthOrientation
plain-language theorem explainer
Canonical growth orientation is the pure order condition that level 1 exceeds level 0 in a nontrivial multilevel composition. It replaces the older divided-ratio hypothesis “base ratio > 1” with a scale-free inequality on the hierarchy values. Downstream φ-forcing and posting-closure theorems take it as a named hypothesis. The declaration is a one-field Prop structure; uniqueness is immediate by proof irrelevance.
Claim. For a nontrivial multilevel composition $M$ (a positive real sequence of levels with at least three positive entries), the canonical growth orientation asserts $M.{\rm levels}(0) < M.{\rm levels}(1)$. Equivalently (via the companion iff), the canonical base ratio of $M$ is strictly greater than $1$.
background
The Unified Forcing Chain module aims to derive the full T0–T8 stack from the Recognition Composition Law plus normalization and calibration. Inside that chain, self-similar discrete hierarchies are packaged as multilevel compositions: a map $\mathbb{N}\to\mathbb{R}$ of positive level sizes with at least three positive levels.
Earlier φ-forcing arguments often assumed a divided inequality on adjacent ratios (base ratio $>1$). That form mixes order with a quotient. Canonical growth orientation isolates the order content alone: the first nontrivial step is strictly larger than the base level. Because all levels are already required positive, this is well-defined without further side conditions.
The companion lemma equates the orientation to $1 < $ canonical base ratio, so older ratio-based proofs can be rewritten without changing mathematical content. Admissible orbits in closed observable frameworks supply the inequality directly by comparing the observable at $T^0$ and $T^1$ of a base state.
proof idea
No proof body: this is a Prop-valued structure with a single field base_step_grows, namely the strict inequality between levels 0 and 1. The attached Subsingleton instance is a one-line rfl on proof irrelevance of Prop, so any two certificates for fixed $M$ are definitionally equal. Downstream theorems either construct the field (e.g. from an admissible orbit by rewriting the observable comparison) or consume it as a named hypothesis alongside uniform scale and seed-size laws.
why it matters
This certificate is the growth half of the T6 φ-forcing package in the unified chain. Parent results include: admissible orbits yield the orientation; the orientation is equivalent to base ratio $>1$; uniform scale plus growth plus seed size force the canonical base ratio to equal $\varphi$; the same triple yields posting closure and the uniform-growth seed theorems that pin $\varphi$.
In the primer landmarks, T6 is “φ forced as the self-similar fixed point.” Growth orientation is the directedness assumption that selects expansion rather than contraction on the discrete ladder, so the golden fixed point is the expanding one. Without it, uniform ratios alone would not distinguish $\varphi$ from $1/\varphi$. The structure therefore sits between hierarchy forcing data and the φ-forcing theorems that close the self-similarity step of the complete inevitability chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.