seedClosed_ratio_gt_one_of_original
plain-language theorem explainer
Compatible seed closure preserves strict growth of the first adjacent ratio: if the original multilevel hierarchy satisfies levels(1)/levels(0) > 1 and the canonical seed-size law, the seed-closed replacement has the same inequality. Cited by the T5→T6 self-similarity bridge when forcing φ from a closed hierarchy. Proof is two rewrites of seed-closed levels back to the original levels, then the given ratio hypothesis.
Claim. Let $M$ be a nontrivial multilevel composition (positive level sizes, at least three levels). Suppose the canonical seed-size law holds: posting seed levels $0$ and $1$ has additive size at the canonical seed index. If $1 < M.\mathrm{levels}(1)/M.\mathrm{levels}(0)$, then the same strict inequality holds for the canonically seed-closed replacement of $M$.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. The T5→T6 step forces the golden ratio φ as the self-similar scale of a discrete ledger hierarchy.
A nontrivial multilevel composition is a positive real sequence of level sizes with at least three levels. The canonical seed-size law isolates the remaining size constraint once the seed index is fixed at 2: posting levels 0 and 1 closes with additive size, $M.\mathrm{levels}(\mathrm{seed_index}) = M.\mathrm{levels}(0)+M.\mathrm{levels}(1)$. Seed closure builds a canonical replacement hierarchy that satisfies this law by construction.
The ratio condition $1 < \mathrm{levels}(1)/\mathrm{levels}(0)$ is the growth half of self-similarity: adjacent scales expand rather than shrink. Downstream φ-forcing needs this on the closed object; the present lemma transfers it from the original data when the seed-size law holds.
proof idea
Term-style tactic proof in three steps. Rewrite the seed-closed level at index 1 via seedClosedLevels_eq_original_of_seed_size_law (under the seed-size law certificate), so the closed ratio's numerator matches the original. Rewrite the closed level at index 0 the same way. The goal collapses to the input hypothesis 1 < M.levels 1 / M.levels 0, discharged by exact. No new arithmetic: equality of levels under seed-size compatibility does all the work.
why it matters
Feeds seedClosed_multilevel_forces_phi, which states that once the original hierarchy has zero-free-scale uniformity and a compatible seed-size law, the seed-closed replacement forces φ without separately assuming the replacement's uniformity or growth fields. That theorem is the concrete hierarchy-dynamics engine behind T5_To_T6_SelfSimilarity_Bridge and the certificate t5_to_t6_bridge_holds.
In the primer chain this is the T5→T6 hinge: unique J (T5) plus self-similar discrete hierarchy forces φ (T6). The bridge structure explicitly records that bare closed-observable fields do not smuggle hierarchy data; growth and additive posting must be supplied or transferred. This lemma is the transfer of the growth inequality under seed closure, so the φ-forcing path can start from original-side hypotheses only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.