Restricted Context Minimality

Abstract

A complete complementary-context family is minimal among its context subfamilies.

Definition 1.1 (Restricted context readout).

$$\begin{gathered} \forall n\in \mathbb{N},C:\mathrm{Fin}\left(n+2\right)\to \mathrm{RankOneContext}\left(n+1\right),S:\mathrm{Finset}\left(\mathrm{Fin}\left(n+2\right)\right), \\ X:\mathrm{Matrix}\left(\mathrm{Fin}\left(n+1\right),\mathrm{Fin}\left(n+1\right),\mathbb{C}\right),ell\in S,j\in \mathrm{Fin}\left(n+1\right), \\ \mathrm{restrictedContextReadout}\left(C,S,X,ell,j\right)=\mathrm{trace}\left(\mathrm{mul}\left(X,\mathrm{projector}\left(C,ell,j\right)\right)\right). \end{gathered}$$

Formalization. D5/S3/Quantum/Tomography/RestrictedContextMinimality.restrictedContextReadout (✓ std3).

Source. Repository-derived.

Commentary.

For a finite subfamily S of the supplied contexts, the readout retains exactly the projector-trace coordinates indexed by S.

Theorem 1.2 (An omitted context supplies indistinguishable projectors).

$$\begin{gathered} \forall n\in \mathbb{N},1\le n,C:\mathrm{Fin}\left(n+2\right)\to \mathrm{RankOneContext}\left(n+1\right), \\ \forall ell,k,j,r,\mathrm{trace}\left(\mathrm{mul}\left(\mathrm{projector}\left(C,ell,j\right),\mathrm{projector}\left(C,k,r\right)\right)\right)=\mathrm{if}\left(\mathrm{Eq}\left(ell,k\right),\mathrm{if}\left(\mathrm{Eq}\left(j,r\right),1,0\right),\mathrm{inverse}\left(n+1\right)\right),S:\mathrm{Finset}\left(\mathrm{Fin}\left(n+2\right)\right),ell\in \mathrm{Fin}\left(n+2\right),ell\neg \in S\Rightarrow \\ \mathrm{projector}\left(C,ell,0\right)\ne \mathrm{projector}\left(C,ell,1\right)\wedge \mathrm{restrictedContextReadout}\left(C,S,\mathrm{projector}\left(C,ell,0\right)\right)=\mathrm{restrictedContextReadout}\left(C,S,\mathrm{projector}\left(C,ell,1\right)\right). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

In dimension n+1 at least two, assume the complete complementary overlap law. If context ell is absent from S, its outcome-zero and outcome-one projectors are distinct but every retained context gives them the same trace coordinates.

The two matrices are explicit and uniform for every omitted context; no positivity or density-state premise is used.

Theorem 1.3 (Exact classification of injective context subfamilies).

$$\begin{gathered} \forall n\in \mathbb{N},1\le n,C:\mathrm{Fin}\left(n+2\right)\to \mathrm{RankOneContext}\left(n+1\right), \\ \forall ell,k,j,r,\mathrm{trace}\left(\mathrm{mul}\left(\mathrm{projector}\left(C,ell,j\right),\mathrm{projector}\left(C,k,r\right)\right)\right)=\mathrm{if}\left(\mathrm{Eq}\left(ell,k\right),\mathrm{if}\left(\mathrm{Eq}\left(j,r\right),1,0\right),\mathrm{inverse}\left(n+1\right)\right),S:\mathrm{Finset}\left(\mathrm{Fin}\left(n+2\right)\right), \\ \mathrm{Injective}\left(\mathrm{restrictedContextReadout}\left(C,S\right)\right)⟺S=\mathrm{univ}\left(\right). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Under the same dimension and overlap hypotheses, the restricted readout is injective on the full complex matrix carrier exactly when S is the full finite context family.

The forward obstruction uses the explicit omitted-context pair; the reverse implication reuses complete context tomography.

References

• Truth anchor: D5/S3/Quantum/Tomography/RestrictedContextMinimality.omitted_context_projectors_indistinguishable
• Truth anchor: D5/S3/Quantum/Tomography/RestrictedContextMinimality.restrictedContextReadout
• Truth anchor: D5/S3/Quantum/Tomography/RestrictedContextMinimality.restricted_contextReadout_injective_iff
• Dependency: D5/S3/Quantum/Tomography/ObserverDiagonalSeparation