RealizedHierarchyNormalFormEquivalence
plain-language theorem explainer
Packages the full equivalence between a realized hierarchy on a closed observable framework and the canonical φ-uniform normal form. Anyone citing the T6 φ-forcing step or hierarchy normal-form closure uses this certificate bundle. It is a pure Prop structure (six fields) with a Subsingleton instance, so certificates are propositionally unique for fixed data.
Claim. For a closed observable framework $F$ and a realized hierarchy $H$ on $F$, the following hold of the multilevel composition $M$ induced by $H$: (i) adjacent levels obey the canonical uniform scale law $M_{k+1}=r\,M_k$; (ii) the first step grows, $M_0<M_1$; (iii) seed levels close additively at the canonical seed index, $M_2=M_0+M_1$; (iv) the canonical base ratio equals $\varphi$; (v) every level of $H$ equals the corresponding level of the $\varphi$-uniform normal form of $M$; (vi) the realized-ladder ratio equals $\varphi$.
background
The module UnifiedForcingChain develops the complete inevitability chain T-1 through T8 from the Recognition Composition Law plus normalization and calibration. T6 forces $\varphi$ as the self-similar fixed point of the discrete ledger; hierarchy machinery then asks when a realized ladder is the same object as the $\varphi$-uniform normal form.
A realized hierarchy $H$ on a closed observable framework $F$ induces a nontrivial multilevel composition $M$. Three theorem-shaped certificates replace raw scale hypotheses on $M$: the canonical uniform-scale law (every adjacent step multiplies by the hierarchy's own base ratio), canonical growth orientation (the first nontrivial level exceeds the base), and the canonical seed-size law (posting levels 0 and 1 closes additively at the forced seed index 2).
The $\varphi$-uniform closed multilevel composition is the normal form built from those laws with base ratio fixed to $\varphi$. This structure is the Prop that says the realized route and that normal-form route agree.
proof idea
Definitional structure, not a proved theorem. The body is six named fields of type Prop (or equality) on the multilevel composition induced by $H$, plus a separate Subsingleton instance whose proof is rfl (all certificates of this type are definitionally equal for fixed $F,H$). No lemmas are applied; consumers inhabit the fields or pass an existing certificate.
why it matters
Sits in the T6 corridor of the forcing chain: once $\varphi$ is forced as the self-similar ratio, realized hierarchies must be identified with the $\varphi$-uniform normal form rather than treated as a parallel construction. The six fields collect exactly the data needed for that identification: uniform scaling, growth orientation, seed closure, base ratio $\varphi$, levelwise equality with the normal form, and agreement of the realized-ladder ratio with $\varphi$.
Downstream hierarchy and constants work can cite a single certificate instead of re-proving scale, seed, and ratio facts. The Subsingleton instance guarantees there is at most one such certificate propositionally, which keeps normal-form reasoning coherent. No used_by edges are recorded yet; the declaration is the interface that later closure theorems are expected to inhabit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.