Observer Diagonal Separation

Abstract

An information-complete quantum readout coexists with diagonal escape.

Definition 1.1 (Projector-trace context readout).

$$\begin{gathered} \forall n:Nat,context:\mathrm{Fin}(n+2)\to \mathrm{RankOneContext}\left(n+1\right),rho:\mathrm{Matrix}\left(\mathrm{Fin}(n+1),\mathrm{Fin}(n+1),Complex\right), \\ \mathrm{contextReadout}\left(context,rho\right)=\mathrm{fun}\left(l,j,,\mathrm{trace}\left(\mathrm{mul}\left(rho,\mathrm{projector}\left(context,l,j\right)\right)\right)\right). \end{gathered}$$

Formalization. D5/S3/Quantum/Tomography/ObserverDiagonalSeparation.contextReadout (✓ std3).

Source. Repository-derived.

Commentary.

The readout is built directly from the canonical rank-one context carrier: each coordinate is the complex trace of the state matrix times the named context projector.

Theorem 1.2 (Empirical observer and diagonal separation).

$$\begin{gathered} \exists context:\mathrm{Fin}(2)\to \mathrm{RankOneContext}\left(1\right), \\ \forall l,k,j,r,\mathrm{trace}\left(\mathrm{mul}\left(\mathrm{projector}\left(context,l,j\right),\mathrm{projector}\left(context,k,r\right)\right)\right)=\mathrm{if}\left(\mathrm{Eq}\left(l,k\right),\mathrm{if}\left(\mathrm{Eq}\left(j,r\right),1,0\right),\mathrm{inverse}\left(1\right)\right)\wedge \mathrm{Injective}\left(\mathrm{contextReadout}\left(context\right)\right)\wedge \exists evaluation:Unit\to \left(Unit\to Bool\right),\exists twist:Bool\to Bool, \\ \forall y,\mathrm{Neq}\left(\mathrm{twist}\left(y\right),y\right)\wedge \mathrm{fun}\left(a,,\mathrm{twist}\left(\mathrm{evaluation}\left(a,a\right)\right)\right)\neg \in \mathrm{range}\left(evaluation\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Tomography/ObserverDiagonalSeparation.empirical_observer_diagonal_separation (✓ std3). ∎

Source. Repository-derived.

Commentary.

The witness uses the repository’s exact rank-one context and matrix carrier. Complementary overlaps are public, and the resulting projector-trace readout is injective on all one-dimensional complex matrices by the imported tomography theorem.

Independently, a Unit-indexed Boolean evaluation list and a Boolean fixed-point-free twist satisfy the public diagonal non-capture clause by the imported Lawvere escape theorem.

Search found both exact supporting declarations but no combined existential; the two carriers and all hypotheses remain explicit in the statement.

References

• Truth anchor: D5/S3/Quantum/Tomography/ObserverDiagonalSeparation.contextReadout
• Truth anchor: D5/S3/Quantum/Tomography/ObserverDiagonalSeparation.empirical_observer_diagonal_separation
• Dependency: D5/S0/Diagonal/Lawvere/QualitativeEscape
• Dependency: D5/S3/Quantum/Tomography/CompleteContextTomography