seedClosureEquiv_forces_phi_iff
plain-language theorem explainer
Seed-closure equivalence of two multilevel hierarchies preserves whether the forced uniform scale ratio equals φ. Anyone citing the T5→T6 self-similarity bridge needs this: replacing a hierarchy by a seed-closed equivalent does not change the φ-forcing proposition. The proof is a two-direction rewrite from equality of the forced ratios under that equivalence.
Claim. Let $M$ and $N$ be nontrivial multilevel compositions that are seed-closure equivalent, each with constant adjacent level ratios strictly greater than one. Then the forced hierarchy ratio of $N$ equals $\varphi$ if and only if the forced hierarchy ratio of $M$ equals $\varphi$.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. The T5→T6 step is where unique $J$ forces the golden ratio $\varphi$ as the self-similar fixed point of a discrete ledger hierarchy.
A nontrivial multilevel composition is a positive real level sequence with at least three levels. Under the no-free-scale hypotheses (all adjacent ratios equal, and the base ratio $>1$), hierarchy_forced builds the corresponding uniform scale ladder and records its common ratio.
Seed-closure equivalence is the forcing-relevant quotient used on this bridge: $N$ is a seed-closed replacement of $M$, levels $0$ and $1$ agree, and the seed level of $N$ is the canonical additive closure $M_0+M_1$. The point is that only this equivalence class matters for whether the forced ratio is $\varphi$.
proof idea
One short term proof. First apply the upstream equality lemma seedClosureEquiv_hierarchy_forced_ratio_eq to the same data: under seed-closure equivalence and the two no-free-scale packages, the forced hierarchy ratios of $M$ and $N$ are equal as reals. Then split the biconditional. Each direction is a single rewrite along that equality (forward or backward) followed by the given hypothesis that one side equals $\varphi$. No new arithmetic is done here; the content is pure transport of the $\varphi$-equality along ratio identity.
why it matters
This is the precise preservation theorem for the seed-closed normal form on the T5→T6 bridge. Downstream it is consumed by t5_to_t6_bridge_holds, whose doc-comment states that the T5-to-T6 self-similarity bridge is theorem-backed; that bridge packages internal hierarchy forcing of $\varphi$ together with realized closed-scale forcing and normal-form equivalence.
In the primer landmarks this sits at T6: $\varphi$ forced as the self-similar fixed point once T5 has unique $J$. Without ratio preservation under seed closure, one could not freely replace a hierarchy by its seed-closed equivalent when arguing that the forced ratio is $\varphi$. The declaration closes that gap for the complete inevitability chain rather than leaving a compatibility claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.