Qubit Empirical-Image Reflexive Gap

Abstract

The exact qubit density-state readout is predicate-complete on its image but reflexively incomplete.

Theorem 1.1 (Qubit empirical completeness does not imply reflexive completeness).

$$\begin{gathered} \exists C:\mathrm{Fin}\left(3\right)\to \mathrm{RankOneContext}\left(2\right), \\ \mathrm{let}\left(R,:,\mathrm{DensityState}\left(\mathrm{Fin}\left(2\right)\right)\to \left(\mathrm{Fin}\left(3\right)\to \left(\mathrm{Fin}\left(2\right)\to \mathbb{C}\right)\right),\mathrm{fun}\left(rho,\mathrm{contextReadout}\left(C,\mathrm{ofMatrixInv}\left(\mathrm{value}\left(rho\right)\right)\right)\right)\right), \\ \mathrm{Injective}\left(R\right)\wedge \\ \mathrm{Bijective}\left(\mathrm{observablePullback}\left(R\right)\right)\wedge \\ \forall catalog:\mathrm{DensityState}\left(\mathrm{Fin}\left(2\right)\right)\to \left(\mathrm{range}\left(R\right)\to Bool\right),\neg \mathrm{Surjective}\left(catalog\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Existence/QubitEmpiricalImageReflexiveGap.qubit_empirical_image_reflexive_gap (✓ std3). ∎

Source. Repository-derived.

Commentary.

In the displayed statement, ofMatrixInv denotes the Lean conversion CStarMatrix.ofMatrix.symm, which reads a density state’s underlying matrix as a C*-matrix; R is the context readout. There is a three-context rank-one qubit observer whose readout R is injective on the full density-state subtype.

For that same R, pullback from Boolean predicates on its realized range is bijective, while every density-state-indexed catalog into that predicate space is non-surjective.

This specializes the abstract strict-gap theorem to the existing public qubit witness. It does not include concrete context-subfamily minimality because the source Pauli context is private.

References

• Truth anchor: D5/S3/Observer/Existence/QubitEmpiricalImageReflexiveGap.qubit_empirical_image_reflexive_gap
• Dependency: D5/S3/ConceptDynamics/ObservationTopology/LosslessReadoutReflexiveGap
• Dependency: D5/S3/Observer/Existence/EmpiricalReflexiveSeparation