seedClosed_multilevel_forces_phi
plain-language theorem explainer
Given a nontrivial multilevel hierarchy with uniform consecutive ratios, growth above 1, and the canonical additive seed-size law, the seed-closed replacement ladder has forced ratio equal to the golden ratio φ. Cited by anyone closing the T5→T6 self-similarity bridge without re-proving uniformity on the closed object. Proof builds the additive level-2 identity from the seed-size law, then applies the hierarchy-forced-gives-φ lemma.
Claim. Let $M$ be a nontrivial multilevel composition whose consecutive level ratios are scale-free ($M_{j+1}/M_j$ independent of $j$) and satisfy $M_1/M_0>1$, and suppose posting seed levels $0$ and $1$ obeys the canonical size law $M_2=M_0+M_1$. Form the canonically seed-closed replacement of $M$. Then the uniform scale ladder forced from that replacement has common ratio equal to $\varphi=(1+\sqrt{5})/2$.
background
Module UnifiedForcingChain aims at a complete inevitability chain T-1 through T8 from the Recognition Composition Law plus normalization and calibration. Landmark T6 is that φ is forced as the self-similar fixed point of a discrete ledger hierarchy.
A NontrivialMultilevelComposition supplies a positive level-size sequence. Zero free scale means every consecutive ratio equals the same constant; the growth hypothesis requires that constant exceed 1. CanonicalSeedSizeLaw isolates the remaining local datum: the seed post index is already forced to 2, and posting levels 0 and 1 has additive size $M_2=M_0+M_1$. The seed-closed replacement is the hierarchy obtained by imposing that primitive closure, rather than a full all-pairs posting operation.
Upstream, hierarchy_forced packages uniform-ratio data into a UniformScaleLadder. The companion lemma hierarchy_forced_gives_phi then identifies the ladder ratio with φ once the additive seed relation at level 2 is available. The present theorem transfers those hypotheses from the original $M$ to its seed-closed form so the φ identification applies without re-assuming uniformity on the replacement.
proof idea
First prove the additive identity on the seed-closed object: its level 2 equals level 1 plus level 0. This is the seed-size law of the closed composition, rewritten with the canonical seed post index and commutativity of addition.
Then apply hierarchy_forced_gives_phi to the seed-closed multilevel composition, feeding the transferred no-free-scale and ratio-greater-than-one certificates (derived from the original hypotheses via the seed-size law) together with the additive identity just obtained. The conclusion is exactly that the forced ladder ratio equals PhiForcing.φ.
The argument is a short tactic proof: one intermediate have for additivity, then a single exact application of the upstream φ-forcing lemma.
why it matters
This certificate is the local engine behind the T5→T6 bridge. Downstream, t5_to_t6_bridge_holds records that the self-similarity bridge is theorem-backed, with clauses for internal hierarchy forcing φ and for realized closed-scale forcing φ; the present result supplies the seed-closed path that avoids assuming full all-pairs posting.
In the forcing chain, T5 uniqueness of the J-cost $J(x)=(x+x^{-1})/2-1$ precedes T6. Once a discrete multilevel ledger is present with uniform scale and additive seed closure, φ is forced as the unique growth ratio compatible with self-similarity. That pins the φ-ladder used later for masses, the eight-tick octave (T7), and $D=3$ (T8).
The doc-comment emphasizes the economy: uniformity and growth need only be checked on the original hierarchy; the seed-closed replacement inherits them, so φ drops out without a second free-scale argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.