seedClosedLevels_zero
plain-language theorem explainer
Seed-closing a multilevel composition leaves the base level unchanged: the closed sequence at index 0 equals the original level-0 value. Hierarchy and phi-forcing arguments that rewrite with seed-closed levels cite this as the k=0 identity. Proof is a one-line simp unfolding the seed-closure definition against the canonical post index 2.
Claim. For every nontrivial multilevel composition $M$ (a strictly positive real sequence of levels with at least three positive entries), the canonically seed-closed level sequence agrees with $M$ at index $0$: the value at $0$ is unchanged.
background
The module UnifiedForcingChain derives the full inevitability chain T-1 through T8 from the Recognition Composition Law plus normalization and calibration. Multilevel compositions enter when discrete ledger self-similarity forces scale ratios (the T6/phi step and related hierarchy forcing).
A nontrivial multilevel composition is a map $\mathbb{N}\to\mathbb{R}$ of positive level values with at least the first three levels strictly positive. The canonical seed-post index is the constant $2$: seed levels $0$ and $1$ close locally at the next rung. Seed-closed levels replace the entry at that index by the sum of levels $0$ and $1$, and leave every other index equal to the original sequence.
This lemma is the base-index case of that definition: index $0$ is not the post index, so seed-closure is the identity there.
proof idea
One-line wrapper. Unfold seed-closed levels and the canonical seed-post index (equal to $2$). The defining conditional is then $0=2$, which is false, so the else branch returns the original level at $0$. No arithmetic or positivity hypotheses are needed beyond the structure type.
why it matters
In the forcing chain, seed-closure is the local second-order move that posts adjacent seed levels onto the next rung before uniform-ratio and self-similarity arguments run. This simp identity keeps rewrites honest at the base of that construction: closing does not disturb level $0$.
No downstream theorems currently list this declaration as a dependency, so it is infrastructure rather than a cited chain step. It still belongs next to the seed-closed-levels definition inside Foundation.UnifiedForcingChain, supporting hierarchy forcing that feeds T6 (phi as the self-similar fixed point) and the discrete ledger story. It does not itself pin phi, the eight-tick octave, or $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.