seedClosedLevels_pos

The module UnifiedForcingChain aims at a complete inevitability chain from the cost foundation (Recognition Composition Law plus normalization and calibration) through T-1 and T0–T8. Multilevel hierarchy data sit in that chain as the discrete scale structure that later forces uniform adjacent ratios and self-similarity toward $\varphi$.

A nontrivial multilevel composition is a map $\mathrm{levels}:\mathbb{N}\to\mathbb{R}$ with $\mathrm{levels},k>0$ for all $k$, and with the first three levels positive (so at least three genuine layers). Seed-closure rebuilds that sequence so a distinguished canonical seed-post index carries a combined seed contribution rather than an independent free level.

Upstream, positivity of sums of positive reals (standard add_pos) and the positivity field of $M$ are the only arithmetic inputs. The canonical seed-post index marks where the seed is folded into the level list; elsewhere the seed-closed sequence agrees with $M$.

Term-style tactic proof. Introduce $k$, unfold the seed-closed level definition, and case on whether $k$ equals the canonical seed-post index.

• If yes: simplify; the value is the sum of $M$'s levels at $0$ and $1$, hence positive by add_pos applied to M.levels_pos 0 and M.levels_pos 1.
• If no: simplify; the value is exactly M.levels k, positive by M.levels_pos k.

No deeper hierarchy lemmas are needed beyond the structure fields of $M$.

This lemma is the positivity witness for seedClosedMultilevelComposition, the canonical seed-closed multilevel composition attached to any positive multilevel composition. That definition sets levels := seedClosedLevels M and levels_pos := seedClosedLevels_pos M, so without this theorem the seed-closed object would not typecheck as a NontrivialMultilevelComposition.

In the forcing chain, seed-closure is bookkeeping that keeps hierarchy data inside the positive cone while folding the seed into a single post index. It supports the discrete multilevel side of the path toward T6 ($\varphi$ as self-similar fixed point) and the broader claim that scale structure is forced rather than parameterized. It does not itself prove ratio rigidity or $\varphi$; it only keeps the rebuilt level sequence strictly positive so later forcing steps can run on a well-formed composition.