UniformSeedClosureCompatibility
plain-language theorem explainer
Compatibility certificate between uniform hierarchy closure and seed-size closure on a nontrivial multilevel composition. Seed-size additivity on the uniform normal form is equivalent to the golden constraint on the base ratio; with growth orientation that forces the base ratio to equal φ. The T5→T6 self-similarity bridge cites it. Definitional Prop bundle: two fields plus a Subsingleton instance by reflexivity.
Claim. For a nontrivial multilevel composition $M$ (positive real levels, at least three), a uniform/seed closure compatibility certificate asserts: (1) the seed-size law on the uniform closed form of $M$ (posting levels $0$ and $1$ sums to the value at the canonical seed index) holds if and only if the canonical base ratio of $M$ satisfies the golden constraint $r^2 = r+1$; (2) if $M$ is growth-oriented ($\mathrm{level}_0 < \mathrm{level}_1$) and that seed-size law holds on the uniform closed form, then the canonical base ratio equals $\varphi$.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. T5 pins the unique cost $J(x)=(x+x^{-1})/2-1$; T6 forces the self-similar scale $\varphi$. The bridge between them runs through hierarchy dynamics: multilevel compositions whose adjacent ratios are uniform and whose seed posting is additive.
A nontrivial multilevel composition is a positive real sequence of levels with at least three entries. The seed-size law isolates the remaining size condition once the seed index is fixed at $2$: posting levels $0$ and $1$ must equal the level at the canonical seed index. Growth orientation is the order fact $\mathrm{level}_0 < \mathrm{level}_1$, replacing a bare ratio-greater-than-one hypothesis. The golden constraint is the fixed-point equation that $\varphi$ uniquely solves among positive reals greater than one.
Uniform closure produces a normal form of the hierarchy with constant adjacent ratios. The certificate records that this normal form still preserves seed posting exactly when the base ratio obeys the golden equation, so uniformization does not smuggle extra scale freedom past the seed surface.
proof idea
Definitional structure, not a proved theorem. The two fields are Prop-valued obligations: an iff between seed-size law on the uniform closed composition and the golden constraint on the base ratio, and an implication from growth orientation plus that seed-size law to base ratio equals $\varphi$. A companion Subsingleton instance shows any two such certificates are propositionally equal by rfl (proof-irrelevant Prop fields). The inhabited canonical instance is supplied separately by canonical_uniform_seed_closure_compatibility, which fills the fields from uniformClosed_seed_size_law_iff_golden and a short intro/apply chain.
why it matters
This is the Lean stand-in for the informal claim that uniformizing a hierarchy still preserves seed posting. Downstream, canonical_uniform_seed_closure_compatibility builds the inhabited certificate, and T5_To_T6_SelfSimilarity_Bridge routes the T5→T6 step through hierarchy dynamics: a closed observable framework with a realized hierarchy forces the scale ratio to be $\varphi$. The bridge doc stresses that bare closed-observable fields alone do not force hierarchy fields (ratio_self_similar, additive_posting), so this certificate is the explicit seam rather than a hidden assumption.
In the forcing chain landmarks, T5 is J-uniqueness and T6 is $\varphi$ as the self-similar fixed point. The certificate ties seed additivity on the uniform normal form to the golden equation, which is exactly the algebraic content of T6 once growth orientation selects the root greater than one. Without it, the chain would still need an external postulate that uniform closure commutes with seed posting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.