Persistence of SPT-Legality from Channelized Feasibility in a Multiscale Hilbert/Cell Model

Multiscale arguments often certify that a state is spread out at fine scales and then assume that this property survives the dynamics. This paper asks when that assumption is justified in a finite multiscale model: a real inner product space split into depth bands, each band split into cells, with a normalized concentration κj that equals 1 for a state spread evenly over the cells of band j and equals the number of cells for a state confined to one cell. A state is SPT-legal if κj stays below a fixed threshold at every depth. Admissible band states are the range of a synthesis map built from finitely many channels. Three results are proved. If every channel is spread over the cells and the channels form a stable (Riesz) system, every admissible vector satisfies κj ≤ κ0(βj/αj) mj, and the factor mj is attained. If the dynamics maps admissible states to admissible states, every trajectory that starts admissible obeys this bound at all times; legality of the initial state alone does not suffice. If the dynamics only keeps the inadmissible part of each band small in every cell, at level εfj, then κj ≤ (√K + √ε)2, where K bounds κj on admissible vectors. All three bounds are machine-checked in Lean 4 with Mathlib. Explicit counterexamples show what fails when each hypothesis is dropped or weakened: a localized channel, ill-conditioned channels, an unrestricted channel count (even linear growth of the channel count permits unbounded concentration), and leakage measured against the whole state instead of the band. Conservation of energy, by itself, places no restriction on concentration beyond its trivial ceiling. Nine numerical experiments with automated assumption audits illustrate the bounds and these counterexamples. The construction is read through the Six Birds primitives of emergence calculus (packaging, gating, staged interfaces, and audits), but the proofs use only elementary Hilbert-space inequalities. The results concern finite-dimensional linear representations and make no claim about regularity for partial differential equations. Code, Lean sources, experiment configurations, and frozen experiment outputs: github.com/ioannist/six-birds-legality. Version 2 (3 October 2026). This is the first Zenodo deposit of the paper; version 1 of the manuscript is dated 15 February 2026. The three bounds, the concentration ceiling, and the localized-vector equality are proved in Lean without gaps. The persistence theorem uses invariance of the whole feasible set with per-band constants, and the cellwise-defect bound is stated pointwise in time. New results show that the static bound is attained and give a band-leakage bound. All counterexamples carry explicit constructions and quantifiers. The numerical code was corrected, all experiments, figures, and tables were regenerated, and the exposition was rewritten.