Core submeasurement structures for the low individual degree test

Foundational measurement, submeasurement, and projective-measurement structures.

structure MIPStarRE.LDT.SubMeas (α : Type u_1) [Fintype α] (ι : Type u_2) [Fintype ι] [DecidableEq ι] : Type (max u_1 u_2)

A paper-local submeasurement with outcomes in α and Hilbert space index ι.

There is intentionally no global Inhabited instance: the zero family satisfies these raw axioms, but using it as an ambient default would silently turn later arguments into vacuous submeasurement statements.

• outcome : α → Quantum.Op ι
• total : Quantum.Op ι
• outcome_pos (a : α) : 0 ≤ self.outcome a
• sum_eq_total : ∑ a : α, self.outcome a = self.total
• total_le_one : self.total ≤ 1

structure MIPStarRE.LDT.Measurement (α : Type u_1) (ι : Type u_2) [Fintype α] [Fintype ι] [DecidableEq ι] extends MIPStarRE.LDT.SubMeas α ι : Type (max u_1 u_2)

A paper-local measurement: a POVM whose PSD effects sum to the identity.

• outcome : α → Quantum.Op ι
• total : Quantum.Op ι
• outcome_pos (a : α) : 0 ≤ self.outcome a
• sum_eq_total : ∑ a : α, self.outcome a = self.total
• total_le_one : self.total ≤ 1
• total_eq_one : self.total = 1

noncomputable def MIPStarRE.LDT.Measurement.trivialDistinguishedOutcome {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (a₀ : α) : Measurement α ι

⚠️ DEGENERATE — Construct a trivial measurement where only the distinguished outcome a₀ is the identity and all other outcomes are zero.

This is a valid POVM but highly degenerate: it is only used in vacuous fallback branches of the proof where the error bound is ≥ 1 (see Test/MainTheorem.lean:mainFormal_trivial_witness).

Call this function explicitly with a chosen outcome. There is intentionally no ambient Inhabited (Measurement α ι) instance: choosing a hidden default : α would make degenerate witnesses available to paper-facing existential statements without displaying the selected outcome.

Equations

• One or more equations did not get rendered due to their size.

structure MIPStarRE.LDT.ProjSubMeas (α : Type u_1) [Fintype α] (ι : Type u_2) [Fintype ι] [DecidableEq ι] extends MIPStarRE.LDT.SubMeas α ι : Type (max u_1 u_2)

A paper-local projective submeasurement (each effect is idempotent).

There is intentionally no global Inhabited instance: any such default would again collapse to the degenerate zero family.

• outcome : α → Quantum.Op ι
• total : Quantum.Op ι
• outcome_pos (a : α) : 0 ≤ self.outcome a
• sum_eq_total : ∑ a : α, self.outcome a = self.total
• total_le_one : self.total ≤ 1
• proj (a : α) : self.outcome a * self.outcome a = self.outcome a

structure MIPStarRE.LDT.ProjMeas (α : Type u_1) (ι : Type u_2) [Fintype α] [Fintype ι] [DecidableEq ι] extends MIPStarRE.LDT.Measurement α ι : Type (max u_1 u_2)

A paper-local projective measurement (complete POVM + projective).

• outcome : α → Quantum.Op ι
• total : Quantum.Op ι
• outcome_pos (a : α) : 0 ≤ self.outcome a
• sum_eq_total : ∑ a : α, self.outcome a = self.total
• total_le_one : self.total ≤ 1
• total_eq_one : self.total = 1
• proj (a : α) : self.outcome a * self.outcome a = self.outcome a

noncomputable def MIPStarRE.LDT.ProjMeas.trivialDistinguishedOutcome {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (a₀ : α) : ProjMeas α ι

⚠️ DEGENERATE — Construct a trivial projective measurement where only the distinguished outcome a₀ is the identity and all other outcomes are zero.

This is a valid projective POVM but highly degenerate: see the discussion at Measurement.trivialDistinguishedOutcome. Prefer calling this function explicitly (with a chosen outcome) rather than relying on the ambient Inhabited instance. As for Measurement, there is intentionally no ambient Inhabited (ProjMeas α ι) instance.

Equations

• MIPStarRE.LDT.ProjMeas.trivialDistinguishedOutcome a₀ = { toMeasurement := MIPStarRE.LDT.Measurement.trivialDistinguishedOutcome a₀, proj := ⋯ }

Derived properties

theorem MIPStarRE.LDT.SubMeas.ext {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] {A B : SubMeas α ι} (houtcome : ∀ (a : α), A.outcome a = B.outcome a) (htotal : A.total = B.total) : A = B

Two submeasurements are equal when they have the same outcome operators and the same total operator.

theorem MIPStarRE.LDT.SubMeas.ext_iff {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] {A B : SubMeas α ι} : A = B ↔ (∀ (a : α), A.outcome a = B.outcome a) ∧ A.total = B.total

theorem MIPStarRE.LDT.Measurement.ext {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] {A B : Measurement α ι} (houtcome : ∀ (a : α), A.outcome a = B.outcome a) : A = B

Two measurements are equal when they have the same outcome operators.

theorem MIPStarRE.LDT.Measurement.ext_iff {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] {A B : Measurement α ι} : A = B ↔ ∀ (a : α), A.outcome a = B.outcome a

theorem MIPStarRE.LDT.ProjMeas.ext {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] {A B : ProjMeas α ι} (houtcome : ∀ (a : α), A.outcome a = B.outcome a) : A = B

Two projective measurements are equal when they have the same outcome operators.

theorem MIPStarRE.LDT.ProjMeas.ext_iff {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] {A B : ProjMeas α ι} : A = B ↔ ∀ (a : α), A.outcome a = B.outcome a

def MIPStarRE.LDT.SubMeas.singleOutcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] (A : Quantum.Op ι) (hA_pos : 0 ≤ A) (hA_le_one : A ≤ 1) : SubMeas Unit ι

A one-outcome submeasurement associated to a single positive operator bounded by the identity.

Equations

• MIPStarRE.LDT.SubMeas.singleOutcome A hA_pos hA_le_one = { outcome := fun (x : Unit) => A, total := A, outcome_pos := ⋯, sum_eq_total := ⋯, total_le_one := hA_le_one }

@[simp]

theorem MIPStarRE.LDT.SubMeas.singleOutcome_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] (A : Quantum.Op ι) (hA_pos : 0 ≤ A) (hA_le_one : A ≤ 1) (u : Unit) : (singleOutcome A hA_pos hA_le_one).outcome u = A

@[simp]

theorem MIPStarRE.LDT.SubMeas.singleOutcome_total {ι : Type u_1} [Fintype ι] [DecidableEq ι] (A : Quantum.Op ι) (hA_pos : 0 ≤ A) (hA_le_one : A ≤ 1) : (singleOutcome A hA_pos hA_le_one).total = A

theorem MIPStarRE.LDT.SubMeas.outcome_hermitian {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (A : SubMeas α ι) (a : α) : Matrix.conjTranspose (A.outcome a) = A.outcome a

PSD outcomes are Hermitian.

theorem MIPStarRE.LDT.Measurement.outcome_hermitian {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (M : Measurement α ι) (a : α) : Matrix.conjTranspose (M.outcome a) = M.outcome a

PSD outcomes are Hermitian.

theorem MIPStarRE.LDT.Measurement.outcome_le_one {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (M : Measurement α ι) (a : α) : M.outcome a ≤ 1

Each POVM element is bounded by the identity: outcome a ≤ 1. Proof: outcome a = 1 - ∑_{b ≠ a} outcome b ≤ 1 since all terms are PSD.

theorem MIPStarRE.LDT.Measurement.sum_eq {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (M : Measurement α ι) : ∑ a : α, M.outcome a = 1

The outcome operators of a measurement sum to the identity.

theorem MIPStarRE.LDT.SubMeas.sum_eq_one_iff_total_eq_one {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (A : SubMeas α ι) : ∑ a : α, A.outcome a = 1 ↔ A.total = 1

A submeasurement is complete exactly when its outcome operators sum to 1.

def MIPStarRE.LDT.SubMeas.toMeasurement {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (A : SubMeas α ι) (hcomplete : A.total = 1) : Measurement α ι

Promote a complete submeasurement to a measurement.

This is the explicit bridge from the paper's sub-measurement convention ∑ a, A_a ≤ I to the POVM convention ∑ a, A_a = I: callers must supply the completion proof rather than relying on a degenerate default.

Equations

• A.toMeasurement hcomplete = { toSubMeas := A, total_eq_one := hcomplete }

@[simp]

theorem MIPStarRE.LDT.SubMeas.toMeasurement_toSubMeas {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (A : SubMeas α ι) (hcomplete : A.total = 1) : (A.toMeasurement hcomplete).toSubMeas = A

@[simp]

theorem MIPStarRE.LDT.SubMeas.toMeasurement_outcome {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (A : SubMeas α ι) (hcomplete : A.total = 1) (a : α) : (A.toMeasurement hcomplete).outcome a = A.outcome a

theorem MIPStarRE.LDT.SubMeas.outcome_le_total {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (A : SubMeas α ι) (a : α) : A.outcome a ≤ A.total

Every submeasurement outcome is bounded by the total operator.

theorem MIPStarRE.LDT.SubMeas.outcome_le_one {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (A : SubMeas α ι) (a : α) : A.outcome a ≤ 1

Every submeasurement outcome is bounded by the identity.

theorem MIPStarRE.LDT.SubMeas.total_nonneg {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (A : SubMeas α ι) : 0 ≤ A.total

The total operator of a submeasurement is PSD.

theorem MIPStarRE.LDT.ProjSubMeas.outcome_hermitian {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (P : ProjSubMeas α ι) (a : α) : Matrix.conjTranspose (P.outcome a) = P.outcome a

Projective submeasurement outcomes are Hermitian (PSD from idempotence).

theorem MIPStarRE.LDT.ProjSubMeas.outcome_mul_total_eq_outcome {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (P : ProjSubMeas α ι) (a : α) : P.outcome a * P.total = P.outcome a

Each projective outcome is absorbed by the total operator.

theorem MIPStarRE.LDT.ProjSubMeas.total_proj {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (P : ProjSubMeas α ι) : P.total * P.total = P.total

The total operator of a projective submeasurement is itself a projector.

theorem MIPStarRE.LDT.ProjSubMeas.outcome_orthogonal {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (P : ProjSubMeas α ι) (a b : α) (hab : a ≠ b) : P.outcome a * P.outcome b = 0

Distinct outcomes of a projective submeasurement are orthogonal.

theorem MIPStarRE.LDT.ProjMeas.outcome_hermitian {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (P : ProjMeas α ι) (a : α) : Matrix.conjTranspose (P.outcome a) = P.outcome a

Projective measurement outcomes are Hermitian (inherited from Measurement.outcome_pos).

theorem MIPStarRE.LDT.ProjMeas.outcome_orthogonal {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (P : ProjMeas α ι) (a b : α) (hab : a ≠ b) : P.outcome a * P.outcome b = 0

Distinct outcomes of a projective measurement are orthogonal.

theorem MIPStarRE.LDT.ProjMeas.outcome_commute {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (P : ProjMeas α ι) (a b : α) : P.outcome a * P.outcome b = P.outcome b * P.outcome a

Any two outcomes of a ProjMeas commute.