seedClosedLevels_two
plain-language theorem explainer
Evaluating the canonically seed-closed level sequence at the seed-post index recovers the sum of the two adjacent seed levels. Hierarchy and seed-size arguments cite this as the defining evaluation identity at that index. The proof is a one-line simplification unfolding the seed-closure map and the fact that the canonical post index is 2.
Claim. For any nontrivial multilevel composition $M$ (a positive real level sequence with at least three levels), the canonically seed-closed level sequence of $M$, evaluated at the canonical seed-post index, equals $M$'s level $0$ plus level $1$.
background
The module builds the complete inevitability chain T-1 through T8 from the cost foundation (Recognition Composition Law plus normalization and calibration). Multilevel hierarchy forcing sits in that chain: a nontrivial multilevel composition is a positive map $\mathbb{N}\to\mathbb{R}$ with at least three strictly positive levels.
Local second-order hierarchy treats levels $0$ and $1$ as the adjacent seed. Their first local closure is posted at the next index. The canonical seed-post index is defined to be $2$. Seed-closure replaces only that index by the sum of the two seed levels and leaves every other level unchanged.
This lemma records the evaluation of that replacement at the post index itself, so later seed-size and fixed-point arguments can treat the sum identity as a simp fact rather than reopening the definition.
proof idea
One-line wrapper: simp unfolds seedClosedLevels and canonical_seed_post_index. The former is the pointwise if k = 2 then levels 0 + levels 1 else levels k; the latter is the constant $2$. The branch fires and the goal is definitional.
why it matters
Parent results are the two seed-size comparison theorems: seed-closure preserves the original level sequence exactly when (and, in one direction, if) the hierarchy already obeys the canonical seed-size law. Both reduce the post-index case to this evaluation identity.
In the forcing chain, seed-size compatibility is the discrete self-similarity constraint that feeds $\varphi$-forcing (T6) and the eight-tick / $D=3$ steps (T7–T8). Without a clean identity at the seed-post slot, those later equalities would carry definitional noise. The lemma is small bookkeeping, but it is the hinge between the seed-closure construction and the seed-size law characterizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.