seedClosureEquiv_hierarchy_forced_ratio_eq
plain-language theorem explainer
Seed-closure equivalence of two multilevel hierarchies forces their uniform scale ladders to carry identical ratios. Anyone working the T6 φ-forcing bridge, or replacing a hierarchy by its seed-closed form, cites this equality. The proof unfolds the forced-ladder constructor and applies base-ratio preservation from the equivalence.
Claim. Let $M$ and $N$ be nontrivial multilevel compositions related by seed-closure equivalence. Suppose each has uniform adjacent level ratios and base ratio strictly greater than $1$. Then the ratio of the forced uniform scale ladder of $N$ equals that of $M$.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Hierarchy forcing sits on the path to T6 (φ forced by self-similarity in a discrete ledger).
A nontrivial multilevel composition is a positive real level function with at least three levels. Uniform adjacent ratios (no free scale) plus base ratio $>1$ produce a uniform scale ladder via hierarchy_forced; that ladder’s ratio is exactly levels 1 / levels 0.
Seed-closure equivalence is the forcing-relevant quotient: non-seed levels agree, levels 0 and 1 are preserved, and the seed level is the canonical additive closure of levels 0 and 1. Upstream, seed-closure already preserves the bare base ratio levels 1 / levels 0.
proof idea
Term proof. Unfold the definition of the forced uniform scale ladder on both sides; its ratio field is the base ratio. Discharge the goal by the upstream lemma that seed-closure equivalence preserves levels 1 / levels 0. The uniformity and growth witnesses are only needed to type the forced ladders; they are not re-proved here.
why it matters
This is the ratio-field half of the seed-closure bridge on the universal forcing spine. Downstream, seedClosureEquiv_forces_phi_iff uses it to show that replacing a hierarchy by a seed-closed equivalent does not change whether the forced ratio equals φ. That preservation is required so T6 (φ as the self-similar fixed point of the discrete ledger) is stable under the canonical seed-closure quotient used elsewhere in the chain. Without ratio equality, φ-forcing could flip under a mere bookkeeping replacement of levels.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.