seedClosed_no_free_scale_of_original
plain-language theorem explainer
If a multilevel hierarchy already has uniform adjacent level ratios and obeys the canonical seed-size law, its canonically seed-closed replacement inherits the same uniform-ratio (no free scale) property. Anyone proving that seed closure forces φ from an original hierarchy cites this transfer. The proof rewrites seed-closed levels back to the original levels and reapplies the given uniformity.
Claim. Let $M$ be a nontrivial multilevel composition (positive real levels, at least three). Suppose posting the two seed levels closes additively at the canonical seed index, and suppose adjacent ratios are scale-free: $M_{j+1}/M_j = M_{k+1}/M_k$ for all $j,k$. Then the canonically seed-closed replacement $M'$ satisfies the same uniformity: $M'_{j+1}/M'_j = M'_{k+1}/M'_k$ for all $j,k$.
background
The module builds the complete inevitability chain T-1 through T8 from the Recognition Composition Law plus normalization and calibration. T5 pins the unique cost $J$; T6 forces the golden ratio $\varphi$ as the self-similar fixed point of a discrete ledger hierarchy.
A nontrivial multilevel composition is a positive real sequence of levels with at least three entries. The no-free-scale condition says every adjacent ratio equals every other, so there is a single geometric scale rather than independent rung factors. The canonical seed-size law isolates the remaining posting constraint: levels at the forced seed index equal the sum of the two seed levels.
Seed closure replaces $M$ by a canonical seed-closed multilevel composition. Under the seed-size law, that replacement agrees with the original level sequence, which is what lets ratio properties transfer without fresh hypotheses on the closed object.
proof idea
Term-mode, essentially a one-line transfer. Introduce arbitrary indices $j,k$. Repeatedly rewrite each occurrence of a seed-closed level via seedClosedLevels_eq_original_of_seed_size_law (using the seed-size certificate), so every ratio of seed-closed levels becomes the corresponding ratio of original levels. Finish by applying the assumed no-free-scale hypothesis at $j,k$.
why it matters
This lemma is the uniformity half of the seed-closure package that feeds T6. Downstream, seedClosed_multilevel_forces_phi uses it so that once the original hierarchy is scale-free and seed-size compatible, the closed replacement forces $\varphi$ without separately assuming uniformity or growth fields on the replacement. That result sits inside the T5-to-T6 self-similarity bridge certificate and the theorem that the bridge holds.
In the forcing chain, T5 gives unique $J$; T6 needs self-similarity on a discrete hierarchy to pin $\varphi$. Compatible seed closure is the bookkeeping step that lets hierarchy data on $M$ become hierarchy data on the closed object the bridge actually quotes. Without this transfer, the closed-scale route to $\varphi$ would reintroduce free scale parameters by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.