Operational Observation Kernel and Metric

Abstract

Positive weighted centered effects induce the residual kernel and operational metric.

Definition 1.1 (Centered effects construct a weighted Euclidean analysis map).

Lean statement: D5/S3/Quantum/Measurement/OperationalObservationKernel.weightedEffectAnalysis

Formalization. D5/S3/Quantum/Measurement/OperationalObservationKernel.weightedEffectAnalysis (✓ std3).

Source. Repository-derived.

Commentary.

Each real trace-zero Hermitian direction is paired with every centered effect and scaled by the square root of its source weight.

Definition 1.2 (The observation seminorm is the weighted analysis norm).

Lean statement: D5/S3/Quantum/Measurement/OperationalObservationKernel.operationalObservationSeminorm

Formalization. D5/S3/Quantum/Measurement/OperationalObservationKernel.operationalObservationSeminorm (✓ std3).

Source. Repository-derived.

Commentary.

The Euclidean norm of the weighted analysis vector is exactly the source’s positive weighted observation seminorm.

Definition 1.3 (Density states have weighted centered-effect readouts).

Lean statement: D5/S3/Quantum/Measurement/OperationalObservationKernel.weightedDensityReadout

Formalization. D5/S3/Quantum/Measurement/OperationalObservationKernel.weightedDensityReadout (✓ std3).

Source. Repository-derived.

Commentary.

A positive trace-one density state is sent to its finite vector of real trace pairings, with the same square-root weights.

Definition 1.4 (State distance is Euclidean readout distance).

Lean statement: D5/S3/Quantum/Measurement/OperationalObservationKernel.operationalStateDistance

Formalization. D5/S3/Quantum/Measurement/OperationalObservationKernel.operationalStateDistance (✓ std3).

Source. Repository-derived.

Commentary.

The induced distance compares only observer-accessible weighted readouts.

Definition 1.5 (The operational quotient identifies equal readouts).

Lean statement: D5/S3/Quantum/Measurement/OperationalObservationKernel.OperationalStateQuotient

Formalization. D5/S3/Quantum/Measurement/OperationalObservationKernel.OperationalStateQuotient (✓ std3).

Source. Repository-derived.

Commentary.

The carrier is the canonical quotient by the kernel Setoid of the weighted density-state readout.

Definition 1.6 (Readout distance descends to operational classes).

Lean statement: D5/S3/Quantum/Measurement/OperationalObservationKernel.operationalQuotientDistance

Formalization. D5/S3/Quantum/Measurement/OperationalObservationKernel.operationalQuotientDistance (✓ std3).

Source. Repository-derived.

Commentary.

Quotient.liftOn2 constructs the representative-independent distance directly on operational classes.

Theorem 1.7 (The seminorm kernel is the invisible residual).

$$\begin{array}{c}\forall d:\mathbb{N},\mathrm{NeZero}\left(d\right),A:\mathrm{Type},\\ [\mathrm{Fintype}\left(A\right)],E:A\to {\mathrm{Herm}}_d^0,w:A\to \mathbb{R},\\ (\forall i\in A,0<w(i))\Rightarrow \\ \mathrm{let}\forall D:{\mathrm{Herm}}_d^0,{\Vert D\Vert }_O=\sqrt{\sum _{i\in A}w(i)⟨D,E_i{⟩}_{\mathbb{R}}^2},\\ \forall \rho :\mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),i:A,q(\rho )(i)=\Re \mathrm{Tr}\left(\mathrm{matrix}\left(\rho \right)E_i\right),\forall \rho :\mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),i:A,q_w(\rho )(i)=\sqrt{w(i)}q(\rho )(i),\\ \forall \rho :\mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),\sigma :\mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),d_O(\rho ,\sigma )={\Vert q_w(\rho )-q_w(\sigma )\Vert }_2,Q_O=\mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right)/\ker \left(q_w\right),\\ \forall \rho :\mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),\sigma :\mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),d_{quot}([\rho ],[\sigma ])=d_O(\rho ,\sigma ),\\ \ker \left(D\mapsto {\Vert D\Vert }_O\right)=\mathrm{span}{\left(\mathbb{R},\{E_i:i\in A\}\right)}^{\perp }\wedge \\ (\forall \rho :\mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),\sigma :\mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),0\le d_O(\rho ,\sigma ))\wedge (\forall \rho :\mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),d_O(\rho ,\rho )=0)\wedge \\ (\forall \rho :\mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),\sigma :\mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),d_O(\rho ,\sigma )=d_O(\sigma ,\rho ))\wedge (\forall \rho :\mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),\sigma :\mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),tau:\mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),d_O(\rho ,tau)\le d_O(\rho ,\sigma )+d_O(\sigma ,tau))\wedge \\ (\forall u:Q_O,v:Q_O,0\le d_{quot}(u,v))\wedge (\forall u:Q_O,d_{quot}(u,u)=0)\wedge \\ (\forall u:Q_O,v:Q_O,d_{quot}(u,v)=d_{quot}(v,u))\wedge (\forall u:Q_O,v:Q_O,z:Q_O,d_{quot}(u,z)\le d_{quot}(u,v)+d_{quot}(v,z))\wedge \\ (\forall u:Q_O,v:Q_O,d_{quot}(u,v)=0⟺u=v)\wedge \\ ((\forall \rho :\mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),\sigma :\mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),d_O(\rho ,\sigma )=0⟺\rho =\sigma )⟺\mathrm{Injective}\left(\rho :\mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right)\mapsto (i:A\mapsto q(\rho )(i))\right)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OperationalObservationKernel.operational_observation_kernel_and_metric (✓ std3). ∎

Source. Repository-derived.

Commentary.

Strictly positive weights make a zero weighted coordinate equivalent to a zero trace pairing. Orthogonality to every effect therefore equals orthogonality to their real span.

Euclidean readout distance supplies the state pseudometric laws. Its canonical kernel quotient is separated and retains symmetry and the triangle inequality.

Because every square-root weight is nonzero, the weighted and unweighted state signatures have the same fibers. Full-state separation is therefore equivalent to informational completeness.

References

• Truth anchor: D5/S3/Quantum/Measurement/OperationalObservationKernel.OperationalStateQuotient
• Truth anchor: D5/S3/Quantum/Measurement/OperationalObservationKernel.operationalObservationSeminorm
• Truth anchor: D5/S3/Quantum/Measurement/OperationalObservationKernel.operationalQuotientDistance
• Truth anchor: D5/S3/Quantum/Measurement/OperationalObservationKernel.operationalStateDistance
• Truth anchor: D5/S3/Quantum/Measurement/OperationalObservationKernel.operational_observation_kernel_and_metric
• Truth anchor: D5/S3/Quantum/Measurement/OperationalObservationKernel.weightedDensityReadout
• Truth anchor: D5/S3/Quantum/Measurement/OperationalObservationKernel.weightedEffectAnalysis
• Dependency: D5/S3/Quantum/Tomography/InformationalCompletenessEquivalence