OrthogonalCoherentEmbedding
Abstract
Orthogonal component coding with complete CPTP padding attains the exact minimum coherent port dimension.
The component quotient retains the arbitrary original probe family. Its finiteness follows from orthonormal representatives in finite dimension. An orthonormal basis of each actual component supplies a coordinate frame. Zero padding embeds these coordinates into a common coherent block whose dimension is the largest component dimension. The encoder stores the component as a classical flag; the decoder applies the frame inverse on the encoded support and prepares a fixed unit probe on the unused complement. Thus the decoder is completely positive and trace preserving on the entire coherent block. The composite pinches between orthogonal components, and every original probe belongs to one component, so its probability is preserved for all density inputs. Conversely every actual encoder-decoder Kraus matrix factors through the coherent block; the scalarity theorem and normalization force one nonzero scalar on each component, yielding the matching rank bound. This is the measurement-relative compression structure described by Bluhm, Rauber, and Wolf, with the nondisturbance rigidity of Mayer and Knill.
Application to static real probes and physical compression. Work in the complex qubit space ℂ² with orthonormal basis e₀, e₁. Set t = 1/√2 and take v₀ = e₀, v₁ = e₁, v₂ = t(e₀ + e₁). For each j separately, Pⱼ = vⱼvⱼ† is the yes effect of the binary measurement {Pⱼ, I − Pⱼ}; its probability on a density matrix ρ is Tr(Pⱼρ). These are three alternative binary settings. The unweighted three-effect menu is not one POVM: P₀ + P₁ + P₂ = I + P₂. Normalization follows from t² = 1/2: every vⱼ has squared norm one. Each Pⱼ is Hermitian, positive semidefinite, trace one and idempotent, hence a rank-one projection; I − Pⱼ is also positive semidefinite, so 0 ≤ Pⱼ ≤ I. Explicitly, P₀ = [[1, 0], [0, 0]], P₁ = [[0, 0], [0, 1]], and P₂ = ½[[1, 1], [1, 1]].
The static observation map records only the three probabilities for the same input state. Write a qubit density as ρ = [[a, z], [conj(z), 1 − a]], where a is real. The menu gives (a, 1 − a, 1/2 + Re(z)); the complementary outcomes add no information. In particular, u₊ = t(e₀ + i e₁) and u₋ = t(e₀ − i e₁) are normalized and have inner product zero. Their density matrices are ρ₊ = ½[[1, −i], [i, 1]] and ρ₋ = ½[[1, i], [−i, 1]]. They are positive semidefinite with trace one, are distinct, and satisfy ρ₊ρ₋ = 0. Nevertheless both yield (1/2, 1/2, 1/2). Thus this static real menu does not identify an arbitrary complex density state, even among pure states with orthogonal supports. This example makes no claim about extra measurement settings or interventions.
The operational hypothesis of the compression theorem is different. Fix one encoder and one decoder before choosing either the input density or the probe setting. The encoder has a finite classical outcome f and a coherent output space ℂ^q indexed by a finite type q; write its Kraus matrices A_fα : ℂ² → ℂ^q. Conditional on f, the decoder has Kraus matrices B_fβ : ℂ^q → ℂ². Require Σ_f,α A_fα†A_fα = I₂ and, for every f, Σ_β B_fβ†B_fβ = I_q. These equations make the encoder an instrument and every conditional decoder CPTP on the entire coherent block, including directions not reached by that branch. Only f and ℂ^q reach the decoder: all input-dependent quantum systems must be counted in q, and there is no quantum bypass. Any finite number of flags and Kraus indices is allowed, and flag probabilities may depend on the input. The single composite channel is T(X) = Σ_f,β,α K_fβα X K_fβα†, with K_fβα = B_fβ A_fα. Impose Tr(PⱼT(ρ)) = Tr(Pⱼρ) for every j ∈ {0, 1, 2} and EVERY density input ρ. Agreement merely on ρ₊ and ρ₋, or a different channel for each setting or input, does not meet this condition.
The exact parameter correspondence uses d = Fin 2, J = Fin 3 and v = (v₀, v₁, v₂) in ProbeComponentRigidity.connected_probability_preserving_identity. Its normalization premise is the unit-vector calculation above. Its span premise is the full COMPLEX linear span, already supplied by v₀ and v₁. Its relation SameComponent is the equivalence relation generated by nonzero inner products of these actual vectors: ⟨v₀, v₁⟩ = 0, but ⟨v₀, v₂⟩ = ⟨v₁, v₂⟩ = t ≠ 0, so the path 0–2–1 connects the whole menu. This is a direct computation of this probe graph, with no correspondence assumed to any FIB graph. For a normalized Kraus family K, the theorem’s finite index s is the actual Kraus index; for the port it is F × b × a and K is port.kraus. The theorem’s two nonempty witnesses can both be chosen as index 0, respectively in J and d. Its DensityState d is precisely a positive semidefinite complex matrix of trace one, represented through CStarMatrix; its probe is vv† and its hprob is exactly the universal trace equality just stated.
Under those hypotheses the existing connected theorem yields T(X) = X for EVERY complex 2 × 2 matrix X, and K_k = K_k(0, 0)I₂ for the same Kraus representation. The mechanism uses more than static readout separation: the all-density equalities fix the rank-one effects under the dual map; complete positivity and trace preservation force each Kraus matrix to commute with those projections. Its scalar actions then agree along the computed nonzero-overlap path and extend over the full complex span. Hence the channel preserves the imaginary coherence separating ρ₊ and ρ₋ even though the static observation map forgets it. The effects also generate the full complex matrix algebra: P₀P₂P₁ = ½E₀₁ and its adjoint gives ½E₁₀, in addition to the diagonal matrix units P₀ and P₁. Here E_ab denotes the matrix with its only nonzero entry, one, in row a and column b. Generated algebra alone is not a general compression lower bound: the inference here uses the stated rank-one effects, universal density-input preservation and physical channel premises.
For OrthogonalCoherentEmbedding.exact_component_port_dimension use the SAME d, J, v, normalization and complex-span proof. Its Component v is the quotient by that actual overlap relation. There is one component, its hilbertComponent is all of ℂ², and maxComponentDimension v hv = 2. The theorem’s universally quantified FlagPort has exactly the A_fα and B_fβ normalization equations above; the finite types F, a and b place no fixed bound on classical flags. Its lower-bound clause therefore gives 2 ≤ card(q) for every such port preserving the three probabilities on every density input. Its existence clause attains coherent dimension two with component flags, complete CPTP encoder and decoder, and composite equal to component pinching. With one full component this pinching is identity; the ordinary identity encoder and decoder also attain the bound. Thus the minimum coherent Hilbert-space dimension in this precise model is two. A purely classical finite flagged port would have a one-dimensional coherent block and cannot satisfy these premises, despite the static indistinguishability of the displayed orthogonal pair.
For the distinction between positive preservation of real readouts and complete positivity, see D5/S3/Quantum/QuantumChannels/RealPartPositiveObstruction. Its discussion supplies the complementary obstruction and is not repeated here. This qubit calculation is an application of the existing results and their cited suppliers, not a physical realization or a literature-novelty claim. Within the ongoing AURIC FIB research it isolates the operational bridge still needed: native preparation and all-density input coverage, the stated measurement availability and controls, a legal coherent encoder and whole-block CPTP decoder, and a resource interpretation counting every quantum system must each be established for the intended FIB model. None is supplied by this application. The general FIB graph-to-probe and implementation bridges remain unresolved here; this computed three-vector example neither assumes nor replaces them.
Theorem 1.1 (components finite).
Lean statement: D5/S3/Quantum/Reduction/OrthogonalCoherentEmbedding.components_finite
Proof. Machine-checked in Lean as D5/S3/Quantum/Reduction/OrthogonalCoherentEmbedding.components_finite (✓ std3). ∎
Source. Repository-derived.
Acknowledgement. Karl Mayer and Emanuel Knill (2018). Quantum process fidelity bounds from sets of input states. URL: https://arxiv.org/html/1805.04491v1.
Commentary.
The quotient of any family of unit probes by the nonorthogonality component relation is finite.
Theorem 1.2 (components orthogonal).
Lean statement: D5/S3/Quantum/Reduction/OrthogonalCoherentEmbedding.components_orthogonal
Proof. Machine-checked in Lean as D5/S3/Quantum/Reduction/OrthogonalCoherentEmbedding.components_orthogonal (✓ std3). ∎
Source. Repository-derived.
Acknowledgement. Karl Mayer and Emanuel Knill (2018). Quantum process fidelity bounds from sets of input states. URL: https://arxiv.org/html/1805.04491v1.
Commentary.
The actual Hilbert spans of distinct components are orthogonal.
Theorem 1.3 (components span).
Lean statement: D5/S3/Quantum/Reduction/OrthogonalCoherentEmbedding.components_span
Proof. Machine-checked in Lean as D5/S3/Quantum/Reduction/OrthogonalCoherentEmbedding.components_span (✓ std3). ∎
Source. Repository-derived.
Acknowledgement. Karl Mayer and Emanuel Knill (2018). Quantum process fidelity bounds from sets of input states. URL: https://arxiv.org/html/1805.04491v1.
Commentary.
When the original arbitrary probe family has full complex span, the supremum of its component Hilbert subspaces is the full space.
Theorem 1.4 (probe channel block form).
Lean statement: D5/S3/Quantum/Reduction/OrthogonalCoherentEmbedding.probe_channel_block_form
Proof. Machine-checked in Lean as D5/S3/Quantum/Reduction/OrthogonalCoherentEmbedding.probe_channel_block_form (✓ std3). ∎
Source. Repository-derived.
Acknowledgement. Andreas Bluhm, Lukas Rauber, and Michael M. Wolf (2018). Quantum compression relative to a set of measurements. URL: https://arxiv.org/html/1708.04898v4.
Acknowledgement. Karl Mayer and Emanuel Knill (2018). Quantum process fidelity bounds from sets of input states. URL: https://arxiv.org/html/1805.04491v1.
Commentary.
Universal probe probability preservation gives normalized environment coefficients on the proved-finite graph components. Every Kraus matrix is their scalar-weighted projection sum. The channel action on every matrix is the double component sum weighted by the overlaps of those environment vectors.
Theorem 1.5 (orthogonal decomposition port).
Lean statement: D5/S3/Quantum/Reduction/OrthogonalCoherentEmbedding.orthogonal_decomposition_port
Proof. Machine-checked in Lean as D5/S3/Quantum/Reduction/OrthogonalCoherentEmbedding.orthogonal_decomposition_port (✓ std3). ∎
Source. Repository-derived.
Acknowledgement. Andreas Bluhm, Lukas Rauber, and Michael M. Wolf (2018). Quantum compression relative to a set of measurements. URL: https://arxiv.org/html/1708.04898v4.
Acknowledgement. Karl Mayer and Emanuel Knill (2018). Quantum process fidelity bounds from sets of input states. URL: https://arxiv.org/html/1805.04491v1.
Commentary.
Every finite orthogonal spanning decomposition with unit vectors in its components admits an actual finite flagged port at any coherent dimension bounding the component dimensions. The encoder and every decoder Kraus matrix are identified explicitly by the orthonormal frame, zero padding, and the complement-filled decoder family. The fixed unit vector lies in its component, and the fixed density is proved to satisfy P times the density times P equals that density.
Theorem 1.6 (exact component port dimension).
Lean statement: D5/S3/Quantum/Reduction/OrthogonalCoherentEmbedding.exact_component_port_dimension
Proof. Machine-checked in Lean as D5/S3/Quantum/Reduction/OrthogonalCoherentEmbedding.exact_component_port_dimension (✓ std3). ∎
Source. Repository-derived.
Acknowledgement. Andreas Bluhm, Lukas Rauber, and Michael M. Wolf (2018). Quantum compression relative to a set of measurements. URL: https://arxiv.org/html/1708.04898v4.
Acknowledgement. Karl Mayer and Emanuel Knill (2018). Quantum process fidelity bounds from sets of input states. URL: https://arxiv.org/html/1805.04491v1.
Commentary.
For any arbitrary unit probe family with full complex span in a finite Hilbert space, the minimum coherent port dimension equals the maximum dimension of its nonorthogonality components. The lower bound covers arbitrary finite flags whose probabilities may depend on the input. The constructed port has the proved-finite component quotient as flags and preserves every original probe probability on every density input. At this dimension, every component embedding has adjoint Gram matrix equal to its actual component projection, the port decoder Kraus matrices are the explicit complement-filled family, and the prepared probe density is proved to be supported in that component. Its composite is exactly orthogonal component pinching. The same theorem also supplies actual canonical completely positive trace-preserving encoder and decoder maps on the flagged algebra, whose all-matrix composition equals that pinching map and whose encoder is proved to have classical diagonal flag outputs.
For a finite coordinate type V, arbitrary original edge labels E, and endpoint maps u and v, FiniteEdgeProbeCorrespondence.construction supplies the unit and spanning hypotheses for its loop-corrected vertex-and-edge menu. Apply exact_component_port_dimension to that menu: its actual component spaces are the coordinate spaces of the endpoint-generated graph classes, and their dimensions are exactly the numbers of vertices in those classes. Thus the existing coherent-port minimum is the largest component vertex count, independently of repeated labels, orientation, loops, or isolated vertices. For actual FIB choices at t at least two, use ActiveVertex(c) and every label in Fin(3t-3), lift the endpoints of chosenPair, and apply restricted_endpoint_closure. Product extensionality identifies the ambient endpoint generators with SupportArrow(c), deriving the activeSetoid(c) correspondence. Finiteness and nonemptiness of the active domain follow from the nonzero modulus and an endpoint of label zero; Balanced is unnecessary. The channel block theorem applies with its trace-preserving Kraus identity and probability preservation for every density input and every original probe. Its cross-component environment Gram coefficients remain in the formula. The native state, observer, preparation and instrument interpretation is an additional unsupplied bridge.
References
- Truth anchor:
D5/S3/Quantum/Reduction/OrthogonalCoherentEmbedding.components_finite - Truth anchor:
D5/S3/Quantum/Reduction/OrthogonalCoherentEmbedding.components_orthogonal - Truth anchor:
D5/S3/Quantum/Reduction/OrthogonalCoherentEmbedding.components_span - Truth anchor:
D5/S3/Quantum/Reduction/OrthogonalCoherentEmbedding.exact_component_port_dimension - Truth anchor:
D5/S3/Quantum/Reduction/OrthogonalCoherentEmbedding.orthogonal_decomposition_port - Truth anchor:
D5/S3/Quantum/Reduction/OrthogonalCoherentEmbedding.probe_channel_block_form - Dependency: D5/S3/Quantum/Reduction/CoherentFlagPort
- Dependency: D5/S3/Quantum/Reduction/ProbeComponentRigidity
- Narrative reference: D5/S3/Quantum/QuantumChannels/RealPartPositiveObstruction