Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Total spectral rows and direct concatenation

Abstract

A given complex encoder supported on legal direct concatenations obeys every total-row rank bound.

Theorem 1.1 (The necessary spectral and threshold bounds).

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/KBonacciDirectSupportObstruction.actual_encoder_spectral_obstruction (✓ std3). ∎

Source. Repository-derived.

Commentary.

All coordinate spaces are the actual finite word spaces. W(m) is Fin m to Bool, L(k,m,w) is DBonacciAdmissible k m w, and append(x,y) is Fin.append x y. head(w) means (List.ofFn w).head?. The initial run p(w) is (List.ofFn w).findIdx Bool.not; t(w) is p of i mapped to w(Fin.rev i). An all-true word contributes its entire width. Natural subtraction is truncated at zero.

P(N,b) is the actual bounded prime or nonprime integer page. Its cardinality is M(b), and orderIsoOfFin gives its increasing enumeration from Fin M(b). The logical carrier is the dependent sum of these pages. K(m,b) is the finite set of legal words with optional first bit some b; c(m,b) is its cardinality. Pi(b) is the logical diagonal page indicator and Q(m,b) is the diagonal indicator of K(m,b) in all words W(m). sigma(b) denotes the underlying complex matrix of a DensityState W(mX), namely CStarMatrix.ofMatrix.symm of its value.

C(J,sigma) includes isometry, both physical page projection identities, density support, the exact identity for every logical matrix, and vanishing illegal amplitude for every logical vector. E and lambda are the eigenvectorBasis and eigenvalues of the Hermitian proof obtained from positivity of that actual sigma(b). D is the nonzero eigenvalue subtype. The displayed rank is Matrix.rank and dim is Module.finrank over Complex.

The matrix-unit contract restricts the given J to the actual Y page before spectral contraction. A zero eigenvalue has zero contraction by the kernel identity for the actual column Gram matrix. Orthonormal spectral expansion reconstructs each total row. The weighted row Gram matrix is the positive diagonal spectrum, so all rows span D. Removing the a(s) earlier rows loses at most a(s) dimensions. Every remaining total row maps into B(s); the extracted isometry then forces M(true) dim V(s) at most n(s). This uses total amplitudes and permits cancellation between spectral terms.

This is a necessary bound for an arbitrary given encoder. It does not characterize feasibility of a specified page-one density matrix by its rank and does not assert attainment or an entropy endpoint. The two-page existence and simultaneous entropy construction require a separate joint choice of actual word labels.

References