seedClosed_after_uniformAfterGrowth_idempotent_levels
plain-language theorem explainer
Seed closure applied after growth-then-uniform closure leaves every level unchanged. Hierarchy and φ-forcing arguments cite this idempotence when reducing the three-step closure stack to the two-step uniform-after-growth form. The proof is a one-line term application of the seed-size-law equality lemma to the already seed-compatible uniform-after-growth hierarchy.
Claim. Let $M$ be a nontrivial multilevel composition (a positive level map $\mathbb{N}\to\mathbb{R}$ with at least three positive levels). For every index $k$, the $k$-th level of the seed-closed form of the uniform-closed form of the growth-closed form of $M$ equals the $k$-th level of the uniform-closed form of the growth-closed form of $M$.
background
The module UnifiedForcingChain proves T0–T8 as forced consequences of the Recognition Composition Law plus normalization and calibration. Inside that chain, multilevel hierarchies carry a level sequence levels : ℕ → ℝ with positivity and a nontriviality lower bound of three positive levels (NontrivialMultilevelComposition).
Three canonical closures act on such hierarchies: growth closure (canonical growth-closed replacement), uniform closure (forces uniform adjacent ratios when free scale parameters are absent), and seed closure (canonical seed-closed replacement). Seed closure is idempotent on any hierarchy that already obeys the compatible seed-size law: if CanonicalSeedSizeLaw M holds, then seed-closed levels equal the original levels (seedClosedLevels_eq_original_of_seed_size_law).
Upstream, uniformAfterGrowth_seed_size_law records that the uniform normal form obtained after growth closure already satisfies that seed-size law, so the seed step is expected to be a no-op on levels.
proof idea
One-line term proof. Instantiate seedClosedLevels_eq_original_of_seed_size_law at the intermediate hierarchy
uniformClosedMultilevelComposition (growthClosedMultilevelComposition M),
and feed it the hypothesis uniformAfterGrowth_seed_size_law M, which asserts CanonicalSeedSizeLaw for that intermediate. The equality lemma then yields pointwise level equality between the seed-closed intermediate and the intermediate itself, which is exactly the claimed identity.
why it matters
This is the seed-idempotence half of the canonical three-closure stack. Downstream, canonical_closure_normal_form_composition packages it as the field seed_after_uniform_growth_idempotent in the closure normal-form certificate. The sibling landing theorem seedUniformGrowthClosed_eq_phiUniform uses the same identity to conclude that growth, then uniform, then seed lands on the direct φ-uniform normal form.
In the forcing chain this sits under T6 (φ forced as the self-similar fixed point of the discrete ledger): once growth and uniform closures have produced the φ-ratio hierarchy, seed closure must not disturb levels, or the normal form would not be unique. The result closes that gap without new analytic input; it only consumes the already-proved seed-size law for the uniform-after-growth object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.