Documentation

MIPRE.Background.LIDT.MIPStarRE.LDT.MakingMeasurementsProjective.ProjectivizationChain.Basic

Section 5 — basic projectivization data #

This module contains the scalar estimates and elementary transport lemmas used by the orthonormalization projectivization chain. The mathematical source is the orthonormalization-and-completion argument in inductive_step.tex, lines 130--149, together with the orthonormalization theorem and the completion proposition cited there.

The declarations here are deliberately prior to the construction of the final projective measurements. They record the literal scalar obtained by composing orthonormalization with completion, its absorbed form in the unit-error regime, the right-register transport available under permutation invariance, and the residual hypotheses passed to the self-consistency handoff theorem. The actual projective-measurement output theorem is in ProjectivizationChain.Output.

The scalar computation is

ζ₂ = 2 · (100·ζ^{1/4}) + 4 · √(100·ζ^{1/4}) + 2·ζ
   = 200·ζ^{1/4} + 40·ζ^{1/8} + 2·ζ.

The paper prints the closed form ζ₂ = 200·ζ^{1/4} + 40·ζ^{1/8}. The Lean cascade uses the slightly widened absorbed scalar 200·ζ^{1/4} + 42·ζ^{1/8} downstream, since in the non-vacuous regime 0 ≤ ζ ≤ 1 gives 2·ζ ≤ 2·ζ^{1/8}.

Status #

References #

Error functions #

source
noncomputable def MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizeAndCompleteError (ζ : Error) :
Error

The combined error of the orthonormalization and completion chain.

Substituting δ := orthonormalizationError ζ = 100·ζ^{1/4} into the closeness conclusion of prop:completing-to-measurement (2·δ + 4·√δ + 2·ζ) gives

`2 · (100·ζ^{1/4}) + 4 · √(100·ζ^{1/4}) + 2·ζ
   = 200·ζ^{1/4} + 40·ζ^{1/8} + 2·ζ`.

This is the literal error returned by composing the two existing lemmas. The paper's printed ζ₂ = 200·ζ^{1/4} + 40·ζ^{1/8} (inductive_step.tex, line 149) drops the residual 2·ζ term; the formal cascade absorbs it into the widened scalar 200·ζ^{1/4} + 42·ζ^{1/8}.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPStarRE.LDT.MakingMeasurementsProjective.sqrt_orthonormalizationError_eq {ζ : Error} (hζ0 : 0 ≤ ζ) :
    √(orthonormalizationError ζ) = 10 * Real.rpow ζ (1 / 8)

    Square-root simplification for the orthonormalization error.

    source
    theorem MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizeAndCompleteError_le_absorbedZeta2 {ζ : Error} (hζ0 : 0 ≤ ζ) (hζ1 : ζ ≤ 1) :
    orthonormalizeAndCompleteError ζ ≤ 200 * Real.rpow ζ (1 / 4) + 42 * Real.rpow ζ (1 / 8)

    The formal cascade scalar with coefficient 42 absorbs the literal orthonormalize-and-complete error in the non-vacuous unit regime.

    Permutation-invariant right-register transport #

    source
    theorem MIPStarRE.LDT.MakingMeasurementsProjective.qSDD_liftRight_eq_liftLeft_of_permInv {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] {ψ : QuantumState (ι × ι)} (hperm : PermInvState ψ) (A B : SubMeas Outcome ι) :
    qSDD ψ A.liftRight B.liftRight = qSDD ψ A.liftLeft B.liftLeft

    On a permutation-invariant bipartite state, the state-dependent distance between right-lifted local submeasurements equals the distance between their left lifts.

    This is the bookkeeping needed for the Bob-side completion estimate in inductive_step.tex lines 140--147: orthonormalizeAndComplete naturally returns a left-register bound, and the paper also uses the corresponding right-register bound for $I \otimes G^{\mathrm B}$ and $I \otimes Q^{\mathrm B}$. This is the submeasurement specialization of Preliminaries.qSDDCore_rightTensor_eq_leftTensor_of_permInv.

    source
    theorem MIPStarRE.LDT.MakingMeasurementsProjective.sddRel_liftRight_of_liftLeft_permInv {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] {ψ : QuantumState (ι × ι)} (hperm : PermInvState ψ) (𝒟 : Distribution Question) (A B : IdxSubMeas Question Outcome ι) (δ : Error) :
    SDDRel ψ 𝒟 A.liftLeft B.liftLeft δ → SDDRel ψ 𝒟 A.liftRight B.liftRight δ

    Transport an SDDRel bound from left lifts to right lifts on a permutation-invariant bipartite state.

    Projective self-consistency handoff #

    source
    structure MIPStarRE.LDT.MakingMeasurementsProjective.ProjectivizationSelfConsistencyHandoff {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (G_A G_B : Measurement Outcome ι) (Q_A Q_B : ProjMeas Outcome ι) (ζ₁ ζ₂ : Error) :
    Prop

    Handoff data for the projective-measurement part of the orthonormalization proof.

    Faithful encoding: The three fields record the paper's pre-projective consistency and the two completion-closeness estimates from references/ldt-paper/inductive_step.tex:130-149. This is not a bridge or residual assumption on a source theorem: ProjectivizationChain.Output constructs the record from the orthonormalization and completion outputs before ProjectivizationChain.Handoff uses it.

    The fields are exactly the hypotheses needed after the orthonormalization and completion constructions have produced projective measurements Q_A,Q_B close to the pre-projective measurements G_A,G_B. The theorem ProjectivizationSelfConsistencyHandoff.fullPolynomialConsistency in ProjectivizationChain.Handoff turns this data into the paper's projective-measurement consistency estimate.

    Instances For