TFPT scientific source excerpt
Original repository path: documents/archive--tfpt-45--source_extracts--04_qft_source/sections/004-source.tex
Original file SHA-256: a5d1cc26f80d2f1d5af3d89b94cf8ff8912b572040614d4e1c27f1fe3b747126
Inclusive original lines: 282-299
Line numbers below refer to the original source.
This bounded excerpt is source evidence; it is not a new proof/checker run.
Conversation metadata and personal execution details are omitted where indicated.

000282 | \begin{lemma}[Diagonal admissibility weights separate the retained basis]
000283 | \label{lem:diagonal-weights-separate-basis}
000284 | Let $\mathcal D_V$ be the commuting family of diagonal admissibility weights entering the blocked
000285 | transfer operator on the retained basis of $\mathcal K_{+,\mathrm{adm}}^{(V)}$. If
000286 | \[
000287 | u\neq v
000288 | \]
000289 | are two retained basis words, then there exists $D\in\mathcal D_V$ such that
000290 | \[
000291 | D_{uu}\neq D_{vv}.
000292 | \]
000293 | \end{lemma}
000294 | 
000295 | \begin{proof}
000296 | Two distinct retained basis words differ in at least one blocked admissibility datum: local
000297 | transport count, carrier label, or retained selector weight. The blocked diagonal admissibility
000298 | weights were constructed precisely from these discrete data, so some diagonal weight separates the
000299 | two words. Hence the family $\mathcal D_V$ separates the retained basis.