MinimalHierarchyCanonicality
plain-language theorem explainer
A Prop certificate that a minimal hierarchy is the canonical one: its scale ratio equals φ and its scale sequence matches the canonical ladder pointwise. Anyone proving T6 (φ forced by self-similarity) or the T5→T6 bridge cites this shape. It is a definitional Prop bundle, not a proved theorem; uniqueness of certificates is immediate by subsingleton.
Claim. For a minimal hierarchy $H$, the certificate asserts two equalities: the hierarchy scale ratio equals $\varphi$, and for every index $k$ the scale $H.{\mathrm{scale}}(k)$ equals the corresponding scale of the canonical minimal hierarchy.
background
The module UnifiedForcingChain aims at a complete inevitability chain T-1 through T8 from the Recognition Composition Law plus normalization and calibration. T5 pins the unique cost $J(x)=(x+x^{-1})/2-1$ (equivalently the shifted $H=J+1$ satisfying d'Alembert). T6 then forces $\varphi$ as the self-similar fixed point of the discrete ledger.
A minimal hierarchy packages a discrete scale sequence with a constant ratio under hierarchy-minimality constraints. The canonical object is the $\varphi$-ladder (scales of the form $\varphi^k$). Canonicality here means: the ratio field is exactly $\varphi$, and the entire scale sequence agrees with that canonical ladder.
Upstream cost algebra supplies $H(x)=J(x)+1=\frac12(x+x^{-1})$, under which RCL becomes the standard d'Alembert identity used to force uniqueness of $J$ before self-similarity is imposed.
proof idea
No proof body: this is a structure extending Prop with two fields, ratio_eq and scale_eq. Inhabitants are built downstream by supplying those equalities (see canonical_minimal_hierarchy_canonicality, which fills them via minimalHierarchy_ratio_eq_phi and minimalHierarchy_scale_eq_canonical). The companion Subsingleton instance is a one-line rfl: any two certificates for fixed $H$ are definitionally equal as pure equality bundles.
why it matters
This certificate is the typed target of the canonicality theorem for every minimal hierarchy, and it is consumed by the T5→T6 self-similarity bridge. That bridge routes φ-forcing through internal hierarchy dynamics: a closed observable framework with a realized hierarchy forces the scale ratio to be φ, while recording that bare closed-observable fields alone do not smuggle hierarchy data.
In the forcing chain this sits at the T5→T6 step: after J-uniqueness, self-similarity on the discrete ledger forces φ. Packaging ratio and full scale agreement as a single Prop keeps the bridge honest about what extra hierarchy structure is assumed versus what T5 already gives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.