uniformAfterGrowth_seed_size_law
plain-language theorem explainer
After growth closure then uniform closure, a nontrivial multilevel hierarchy obeys the canonical seed size law: the level at the seed post index equals the sum of levels 0 and 1. Hierarchy and φ-forcing arguments cite this to justify seed closure without changing levels. The proof is a short term argument: the uniform-closed seed-size criterion reduces to the golden constraint, the growth-closed base ratio is φ, and φ satisfies that constraint.
Claim. For every nontrivial multilevel composition $M$ (positive level sizes with at least three levels), the composition obtained by first applying growth closure and then uniform closure satisfies the canonical seed size law: if $M'$ is that closed hierarchy, then $M'(\mathrm{seed\_post}) = M'(0) + M'(1)$.
background
The module UnifiedForcingChain develops the complete inevitability chain T-1 through T8 from the Recognition Composition Law plus normalization and calibration. Here the local objects are multilevel hierarchies: maps $\mathbb{N}\to\mathbb{R}$ with strictly positive levels and at least three occupied rungs (NontrivialMultilevelComposition).
Growth closure produces a canonical growth-closed hierarchy whose adjacent base ratio is forced to $\varphi$ (the golden ratio fixed by T6 self-similarity). Uniform closure then enforces the no-free-scale normal form of adjacent ratios. The CanonicalSeedSizeLaw certificate isolates the remaining posting identity at the already-forced seed index 2: posting levels 0 and 1 is additive, $M(\mathrm{seed_post})=M(0)+M(1)$, so later seed closure can be stated without reopening size parameters.
Upstream, phi_satisfies records that $\varphi$ meets the golden constraint, and growthClosedMultilevelComposition_base_ratio identifies the growth-closed base ratio with $\varphi$. An intermediate equivalence links the uniform-closed seed size law to that same golden constraint on the base ratio.
proof idea
Term-mode, three steps. Apply the right-to-left direction of the equivalence that the uniform-closed hierarchy obeys the seed size law if and only if its base ratio satisfies the golden constraint, instantiated at the growth-closed form of $M$. Rewrite that base ratio via the growth-closure lemma, which equals $\varphi$. Discharge the golden constraint by the standard fact that $\varphi$ satisfies it. No further case splits or hierarchy induction.
why it matters
In the forcing chain this sits on the T6 φ-forcing side of hierarchy normal forms: growth closure pins the base ratio to $\varphi$, uniform closure removes free scale, and this theorem shows the resulting object already carries the additive seed size law needed for seed posting. Downstream, seedClosed_after_uniformAfterGrowth_idempotent_levels uses it to prove that seed closure after uniform-after-growth changes no levels, so the uniform-after-growth normal form is already seed-stable. That idempotence is part of closing the multilevel composition pipeline before ledger and eight-tick (T7) structure are read off. It does not itself force $D=3$ or the eight-tick octave; it only certifies seed-size readiness of the φ-normalized hierarchy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.