Empirical and Reflexive Completeness Separate

Abstract

A complete quantum-state readout does not make internal self-evaluation exhaustive.

Theorem 1.1 (The embedded square root of two).

$$(Real.sqrt\left(2\right):Complex{)}^2=2$$

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

Source. Repository-derived.

Commentary.

The real square root of two, embedded in Complex, has square two. This identity normalizes the rank-one qubit projectors.

Theorem 1.2 (Normalized rank-one densities are projections).

$$\forall v\in \mathrm{Fin}\left(2\right)\to Complex,\mathrm{dotProduct}\left(\mathrm{star}\left(v\right),v\right)=1\Rightarrow \mathrm{IsNormalizedRankOneProjection}\left(\mathrm{rankOneDensity}\left(v\right)\right)$$

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

Source. Repository-derived.

Commentary.

The density matrix of a unit vector is a normalized rank-one projection.

Theorem 1.3 (Empirical completeness coexists with reflexive incompleteness).

$$\exists context\in \mathrm{Fin}\left(3\right)\to \mathrm{RankOneContext}\left(2\right),\mathrm{Injective}\left((rho:\mathrm{DensityState}\left(\mathrm{Fin}\left(2\right)\right)\mapsto \mathrm{contextReadout}\left(context,\mathrm{matrix}\left(rho\right)\right))\right)\wedge \left(\forall evaluation\in \mathrm{DensityState}\left(\mathrm{Fin}\left(2\right)\right)\to \left(\mathrm{DensityState}\left(\mathrm{Fin}\left(2\right)\right)\to Bool\right),\neg (state\mapsto \mathrm{not}\left(\mathrm{evaluation}\left(state,state\right)\right))\in \mathrm{range}\left(evaluation\right)\right)$$

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

Source. Repository-derived.

Commentary.

There is a three-context rank-one qubit observer whose projector-trace readout is injective on the canonical carrier of positive, trace-one qubit density states. This is the public current-state reconstruction clause.

For every Boolean evaluation table indexed twice by that same density-state carrier, the function obtained by negating the table on its diagonal is outside the table’s range. This is exactly the public internal self-evaluation non-capture clause.

The concrete witness uses the three standard mutually unbiased qubit bases. The proof then applies the repository’s complete-context tomography and fixed-point-free Lawvere escape theorems.

References

• Truth anchor: D5/S3/Observer/Existence/EmpiricalReflexiveSeparation.complex_sqrt_two_sq
• Truth anchor: D5/S3/Observer/Existence/EmpiricalReflexiveSeparation.empirical_complete_reflexive_incomplete
• Truth anchor: D5/S3/Observer/Existence/EmpiricalReflexiveSeparation.rankOneDensity_isNormalized
• Dependency: D5/S3/Quantum/Foundation/FiniteStateChannel
• Dependency: D5/S3/Quantum/PureState/PureStateHandshake
• Dependency: D5/S3/Quantum/Tomography/ObserverDiagonalSeparation