seedClosedMultilevelComposition_preserves_base_ratio
plain-language theorem explainer
Any nontrivial multilevel hierarchy and its canonical seed-closed replacement share the same base adjacent ratio levels(1)/levels(0). Hierarchy and T5–T6 bridge arguments cite this to move φ-forcing from the closed ladder back to the original scale. The proof is a one-line application of ratio preservation under seed-closure equivalence.
Claim. For every nontrivial multilevel composition $M$ (positive level map $\mathbb{N}\to\mathbb{R}$ with at least three positive levels), if $M'$ is the canonical seed-closed replacement of $M$, then $$\frac{M'(1)}{M'(0)}=\frac{M(1)}{M(0)}.$$
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. T5 pins the unique cost $J$; T6 forces $\varphi$ as the self-similar fixed point of a discrete ledger hierarchy.
A NontrivialMultilevelComposition is a positive real level map with at least three levels. The canonical seed-closed replacement rebuilds such a hierarchy so that seed-size and uniformity constraints hold while remaining forcing-equivalent to the original under SeedClosureEquiv (matching level-0 and level-1 data and the replacement witness).
Upstream, seed-closure equivalence is already known to identify ratio fields of the two ladders when both sides carry their uniformity and growth witnesses. That ratio identity is what this theorem specializes to the canonical closed form of $M$.
proof idea
One-line term proof. Instantiate the general lemma that any seed-closure equivalence preserves the base ratio, feeding it the original hierarchy $M$, the canonical seed-closed replacement, and the already-proved equivalence certificate between them. No extra algebraic work: the equality is inherited from the equivalence structure.
why it matters
This is the ratio hinge between seed-closed normal form and the physicist's original hierarchy. Downstream, seedClosed_phi_transfers_to_original_ratio uses it: if the closed ladder is forced to base ratio $\varphi$, the original ladder has the same base ratio, hence is $\varphi$ as well. That transfer feeds canonical_seed_closure_preservation and the T5-to-T6 self-similarity bridge (t5_to_t6_bridge_holds), which is the forcing-chain step from unique $J$ (T5) to $\varphi$ as the discrete self-similar fixed point (T6).
Without base-ratio preservation, $\varphi$-forcing on the closed seed would not export to arbitrary positive multilevel compositions. The result is fully proved scaffolding for that export, not a new forcing axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.