GrowthClosurePreservation
plain-language theorem explainer
A certificate that growth-closure of a nontrivial multilevel hierarchy is growth-oriented, has base ratio φ, is idempotent, and leaves levels fixed exactly when the hierarchy already steps by φ. Cited by the T5→T6 self-similarity bridge and by the canonical certificate constructor. Pure structure of four Prop fields; uniqueness is propositional (Subsingleton).
Claim. For a nontrivial multilevel composition $M$, a growth-closure preservation certificate asserts four facts about its growth-closed normal form $M^\sharp$: (i) $M^\sharp$ is growth-oriented ($M^\sharp_0 < M^\sharp_1$); (ii) the canonical base ratio of $M^\sharp$ equals $\varphi$; (iii) $M^\sharp$ agrees with $M$ at every level if and only if $M_1 = M_0\cdot\varphi$; (iv) growth-closure is idempotent on levels: $(M^\sharp)^\sharp_k = M^\sharp_k$ for all $k$.
background
The Unified Forcing Chain module aims to derive T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. T5 pins the unique cost $J$; T6 forces the golden ratio $\varphi$ as the self-similar fixed point of discrete ledger growth.
A nontrivial multilevel composition is a hierarchy of positive scale levels. Growth closure produces a normal form that enforces consistent multiplicative growth. Canonical growth orientation is the order-level statement that the first nontrivial level strictly exceeds the base level (the replacement for a divided ratio-greater-than-one hypothesis).
This structure packages the preservation properties of that normal form relative to $\varphi$ from PhiForcing, so later bridges can cite a single Prop rather than four separate lemmas.
proof idea
Definitional structure only: four named Prop fields with no proof body. A companion Subsingleton instance shows any two certificates for fixed $M$ are definitionally equal (allEq by rfl), so the certificate type is propositionally unique. The inhabiting theorem canonical_growth_closure_preservation fills the fields from the growth-closed orientation, base-ratio, and level-equality lemmas; this declaration itself is just the interface.
why it matters
Sits on the T5→T6 path: once $J$ is unique, self-similarity in a realized hierarchy must force scale ratio $\varphi$. Downstream, canonical_growth_closure_preservation supplies the standard witness, and T5_To_T6_SelfSimilarity_Bridge routes through hierarchy-dynamics so that a closed observable framework with a realized hierarchy forces the scale ratio to be $\varphi$, while recording that bare closed-observable fields alone do not smuggle hierarchy data.
In primer terms this is the bookkeeping layer for T6 ($\varphi$ forced as self-similar fixed point): growth closure must land on a $\varphi$-step, stay oriented, and stabilize under reapplication. Without exact-preservation iff and idempotence, the forcing chain could not treat $\varphi$ as the unique discrete growth ratio rather than an optional normalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.