Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Exact ranks and entropy for direct concatenation

Abstract

Legal direct two-page concatenation has exact auxiliary ranks and simultaneous entropy maxima.

Theorem 1.1 (Two-page rank and entropy optimum).

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

Source. Repository-derived.

Commentary.

W(m) is the full Boolean computational word carrier Fin m to Bool. L(k,m,w) is the native DBonacciAdmissible predicate, append is Fin.append, and the first bit is (List.ofFn w).head?. The initial run p(w) is (List.ofFn w).findIdx Bool.not and the terminal run t(w) is p of the reversed word. All-true words contribute their full length, including windows shorter than k. The integer weights G(j) retain the powers-of-two initialization and k-term recurrence; the length-m interval normalization is G(m)=dbonacci(k,m+2). No address decoder is required by this regional encoder.

P(N,b) consists of actual integers n at most N with decide(Nat.Prime n)=b. Its cardinality is M(b); orderIsoOfFin gives the original increasing page enumeration. Zero and one belong to page false, and two belongs to page true, so both logical pages are nonzero. HL is their dependent sum. K(m,b) consists of actual legal words with first bit b and c(m,b) is its cardinality. Pi and Q are the corresponding diagonal projections, embedded into the full computational spaces. NatDiv is integer floor division. The threshold minimum ranges over every state from zero to k-1.

C(J,sigma) requires one complex isometry, both page projection identities, density support, the exact partial trace identity for every logical matrix A, and zero illegal amplitude for every logical vector psi. sigma(b) in the formulas is the complex matrix underlying DensityState W(mX). S is native vonNeumannEntropy, with natural logarithms and zero-log-zero equal to zero. A pure page vector has norm one and vanishes outside that logical page; SchmidtRank is the rank of its actual X-by-Y amplitude matrix. T is totalRowSpectralNecessity for the true page: it asserts the five true-page spectral reconstruction, support, span and threshold clauses defined in Lean. The separate two-page spectral result is supplied by KBonacciDirectSupportObstruction.actual_encoder_spectral_obstruction, not a literal expansion of T.

The necessary bound uses the arbitrary positive spectrum and eigenvector basis of the given sigma. Its weighted computational rows q span the nonzero spectral coordinates. Removing a(s) low-state rows loses at most a(s) dimensions. The actual total row amplitudes map the remaining span into B(s), and the extracted isometry gives M(true) dim V(s) at most n(s). This includes cancellation between Schmidt terms. The neighborhoods are nested, with B(k-1) empty. The result gives no rank-only feasibility criterion for a density matrix whose eigenvectors were specified beforehand.

For any positive ranks within the stated bounds, page-one X words are chosen by terminal state, then lexicographic order. Exactly max(0,d1-a(s)) selected rows have state at least s. Each selected row needs M(true) distinct labels. For a nonempty subset of these cloned demands, its minimum state identifies the union neighborhood B(s), and the threshold inequality bounds its cardinality. Hall’s theorem supplies one jointly injective assignment of actual Y words. Page zero uses arbitrary distinct legal X words and M(false)d0 distinct legal Y words.

The uniform construction combines both pages in the same ambient J. Its matrix units have partial trace delta(r,t)sigma(b) within a page and zero across pages, because the actual Y labels are globally distinct. Linear extension gives the identity for every matrix, and each chosen concatenation is legal, so all input amplitudes satisfy the support condition. The uniform pointer mixtures have ranks d0,d1 and entropies log(d0),log(d1). The actual nonzero density spectrum bounds every entropy by log(rank), proving both endpoints and the feasibility equivalence.

The stronger two-page spectral supplier is the existing theorem D5.S3.Quantum.Entanglement.KBonacciDirectSupportObstruction.actual_encoder_spectral_obstruction. The following display is explanatory supplier context with its own bound spectrum and page-dependent witness; it is not a literal unfolding of T and is not an additional authored assertion.

UniformConstruction is the selected common witness for one permitted positive pair d0,d1. Its binders include the selected page-specific X words and one globally injective dependent-sum Y labeling; the identities below describe that selected witness only, while the capacity threshold is used only for s<k. complexDelta(u,v) is the complex Kronecker delta, invSqrt(d) is the complex scalar 1/sqrt(d), inv(d) is the complex scalar 1/d, and projector(w) is the computational pointer projector. The d1-a(s) subtraction is truncated natural subtraction.

References