RealizedClosedScaleNormalFormEquivalence
plain-language theorem explainer
Packages the direct equivalence certificate that a realized closed-scale model matches the canonical φ-uniform normal form: uniform adjacent scaling, growth orientation, seed-size additivity, base ratio equal to φ, levelwise orbit agreement, and the converted hierarchy normal-form certificate. Downstream orbit bridges and the T5→T6 self-similarity bridge cite it. Definitional Prop-structure; uniqueness is propositional (Subsingleton by rfl).
Claim. Fix a closed observable framework $F$ and a realized closed-scale model $H$ on $F$. A realized-closed-scale normal-form equivalence is a certificate that the multilevel composition built from $H$ obeys the canonical uniform-scale law (each adjacent level is the base ratio times the previous), the canonical growth orientation (level $1$ exceeds level $0$), and the canonical seed-size law (the seed-post index equals the sum of levels $0$ and $1$); that the canonical base ratio equals $\varphi$; that orbit levels $F.r(F.T^{[k]} H.\mathrm{base})$ agree with the $\varphi$-uniform normal-form levels; and that the converted realized-hierarchy view carries the corresponding hierarchy normal-form equivalence.
background
The module UnifiedForcingChain aims at a complete inevitability chain from the cost foundation (Recognition Composition Law, normalization, calibration) through T-1 to T8. T5 pins the unique cost $J(x)=(x+x^{-1})/2-1$ (equivalently the shifted $H=J+1$ satisfying d'Alembert); T6 forces the golden ratio $\varphi$ as the self-similar scale fixed point in a discrete ledger.
A realized closed-scale model supplies a base state whose orbit under the framework tick, read out by the observable $r$, yields a nontrivial multilevel composition. Three theorem-shaped replacements for raw hierarchy hypotheses appear here: CanonicalUniformScaleLaw (adjacent levels generated by the composition's own base ratio), CanonicalGrowthOrientation (first nontrivial step grows), and CanonicalSeedSizeLaw (posting seed levels $0$ and $1$ closes with additive size at the forced seed index).
The parallel certificate RealizedHierarchyNormalFormEquivalence does the same job on the converted realized-hierarchy view. The $\varphi$-uniform normal form is the multilevel composition whose levels are pure powers of $\varphi$ (cf. the cosmological scale ladder $\mathrm{scale}(k)=\varphi^k$).
proof idea
This declaration is a Prop-valued structure, not a proved theorem: it names the six fields that together constitute the direct normal-form equivalence. No tactic proof is attached to the structure itself.
The companion Subsingleton instance is a one-line propositional uniqueness argument (allEq by rfl): any two certificates for fixed $F,H$ are definitionally equal as pure Prop bundles.
Inhabitation is supplied downstream by canonical_realized_closed_scale_normal_form_equivalence, which fills the fields from the specialized lemmas realizedClosedScale_canonical_uniform, realizedClosedScale_canonical_growth, and their siblings for seed, base ratio, level agreement, and the converted hierarchy certificate.
why it matters
This certificate is the direct closed-scale face of the φ-normal-form identification used to force T6. Downstream, canonical_realized_closed_scale_normal_form_equivalence builds the canonical instance; MinimalClosedScaleOrbitBridge and RealizedClosedScaleAdmissibleOrbitBridge package it with admissible-orbit and minimal-orbit data so that closed-scale realization, admissible reflection, and φ-uniform form are one bridge.
Most importantly, T5_To_T6_SelfSimilarity_Bridge routes T5→T6 through internal hierarchy dynamics: a closed observable framework with realized hierarchy forces the scale ratio to be φ, while recording that bare closed-framework fields alone do not smuggle in ratio_self_similar or additive_posting. The present structure is the closed-scale half of that normal-form side of the bridge, tying the forcing chain's self-similarity step (T6, φ as fixed point) to concrete orbit-level data rather than an external ansatz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.