Documentation

LeanPool.SingleCopyStabilizer.ExactLearning

Stochastic compression of unsigned binary stabilizer labels #

This module instantiates the finite adaptive-process theorem with the actual binary label-space update. At every round, it samples an X label uniformly from the current X projection and an independent uniform binary correction. The progress lower bound is proved from the one-round symplectic results.

This is a theorem about unsigned label spaces. It does not assert that a quantum measurement supplies the stated distribution or reconstruct phases.

source
@[reducible, inline]
abbrev LeanPool.SingleCopyStabilizer.ExactLearning.State (ι : Type u_2) [Fintype ι] :
Type u_2

An unsigned binary Lagrangian label space.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[reducible, inline]
    abbrev LeanPool.SingleCopyStabilizer.ExactLearning.Outcome (ι : Type u_2) :
    Type u_2

    An observed X label together with its independent correction bit.

    Equations
    Instances For
      source
      noncomputable def LeanPool.SingleCopyStabilizer.ExactLearning.rank {ι : Type u_1} [Fintype ι] (s : State ι) :
      ℕ

      The number of diagonal generators still missing.

      Equations
      Instances For
        source
        noncomputable def LeanPool.SingleCopyStabilizer.ExactLearning.next {ι : Type u_1} [Fintype ι] [DecidableEq ι] (s : State ι) (o : Outcome ι) :
        State ι

        Totalized round update, with the Lagrangian invariants preserved.

        Equations
        Instances For
          source
          noncomputable def LeanPool.SingleCopyStabilizer.ExactLearning.weight {ι : Type u_1} [Fintype ι] (s : State ι) (o : Outcome ι) :
          ℝ

          Uniform sampling on the current X projection, independently of a uniform correction bit. Impossible X labels have weight zero.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem LeanPool.SingleCopyStabilizer.ExactLearning.projection_card_pos {ι : Type u_1} [Fintype ι] (s : State ι) :
            0 < Nat.card ↥(xProjection ↑s)
            source
            theorem LeanPool.SingleCopyStabilizer.ExactLearning.weight_nonneg {ι : Type u_1} [Fintype ι] (s : State ι) (o : Outcome ι) :
            0 ≤ weight s o
            source
            theorem LeanPool.SingleCopyStabilizer.ExactLearning.weight_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (s : State ι) :
            ∑ o : Outcome ι, weight s o = 1
            source
            theorem LeanPool.SingleCopyStabilizer.ExactLearning.diagonal_finrank_le {ι : Type u_1} [Fintype ι] (s : State ι) :
            Module.finrank (ZMod 2) ↥(diagonalSpace ↑s) ≤ Fintype.card ι
            source
            theorem LeanPool.SingleCopyStabilizer.ExactLearning.rank_eq_projection_finrank {ι : Type u_1} [Fintype ι] (s : State ι) :
            rank s = Module.finrank (ZMod 2) ↥(xProjection ↑s)
            source
            theorem LeanPool.SingleCopyStabilizer.ExactLearning.projection_card_eq_pow_rank {ι : Type u_1} [Fintype ι] (s : State ι) :
            Nat.card ↥(xProjection ↑s) = 2 ^ rank s

            The current X projection contains exactly 2^rank labels.

            source
            theorem LeanPool.SingleCopyStabilizer.ExactLearning.rank_mono {ι : Type u_1} [Fintype ι] [DecidableEq ι] (s : State ι) (o : Outcome ι) :
            rank (next s o) ≤ rank s
            source
            noncomputable def LeanPool.SingleCopyStabilizer.ExactLearning.process {ι : Type u_1} [Fintype ι] [DecidableEq ι] :
            AdaptiveProcess.RankedProcess (State ι) (Outcome ι)

            The finite probability process whose random outcomes are projection labels and correction bits, and whose state is the evolving label space.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem LeanPool.SingleCopyStabilizer.ExactLearning.exists_rank_progress {ι : Type u_1} [Fintype ι] [DecidableEq ι] (s : State ι) (u : BinaryVec ι) (hu : u ∈ xProjection ↑s) (hzero : u ≠ 0) :
              ∃ (b : ZMod 2), rank (next s (u, b)) < rank s

              Any nonzero allowed X label admits at least one correction that strictly reduces the number of missing diagonal generators.

              source
              theorem LeanPool.SingleCopyStabilizer.ExactLearning.two_le_projection_card {ι : Type u_1} [Fintype ι] (s : State ι) (hrank : 0 < rank s) :
              2 ≤ Nat.card ↥(xProjection ↑s)

              Positive rank guarantees at least two possible X labels.

              source
              theorem LeanPool.SingleCopyStabilizer.ExactLearning.nonzero_projection_card {ι : Type u_1} [Fintype ι] [DecidableEq ι] (s : State ι) :
              {u : BinaryVec ι | u ∈ xProjection ↑s ∧ u ≠ 0}.card = Nat.card ↥(xProjection ↑s) - 1

              Cardinality of the nonzero part of the X projection.

              source
              theorem LeanPool.SingleCopyStabilizer.ExactLearning.progress_mass_lower_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (s : State ι) :
              (↑(Nat.card ↥(xProjection ↑s)) - 1) / (↑(Nat.card ↥(xProjection ↑s)) * 2) ≤ process.progressMass s

              Counting one successful correction for every nonzero X label gives an unconditional progress mass of at least (#X-1)/(2#X).

              source
              theorem LeanPool.SingleCopyStabilizer.ExactLearning.progress_mass_ge_rank_parameter {ι : Type u_1} [Fintype ι] [DecidableEq ι] (s : State ι) :
              (1 - (1 / 2) ^ rank s) / 2 ≤ process.progressMass s

              The exact rank-dependent progress parameter used in the paper is also proved for this label process.

              source
              theorem LeanPool.SingleCopyStabilizer.ExactLearning.progress_mass_ge_quarter {ι : Type u_1} [Fintype ι] [DecidableEq ι] (s : State ι) (hrank : 0 < rank s) :
              1 / 4 ≤ process.progressMass s

              The quarter-progress assumption is derived from the label-space update, not left as a hypothesis of the compression theorem.

              source
              theorem LeanPool.SingleCopyStabilizer.ExactLearning.compression_failure_probability {ι : Type u_1} [Fintype ι] [DecidableEq ι] (s : State ι) (k : ℕ) :
              process.failureProbability (8 * (Fintype.card ι + k)) s ≤ (1 / 2) ^ k

              After 8(n+k) uniform-X-label rounds, the probability that the label space is not fully diagonal is at most 2^(-k). Here n = #ι, and all the per-round progress hypotheses have been discharged.

              source
              theorem LeanPool.SingleCopyStabilizer.ExactLearning.rank_zero_iff_full_diagonal {ι : Type u_1} [Fintype ι] (s : State ι) :
              rank s = 0 ↔ Module.finrank (ZMod 2) ↥(diagonalSpace ↑s) = Fintype.card ι

              The terminal event has exactly the expected algebraic meaning.

              source
              theorem LeanPool.SingleCopyStabilizer.ExactLearning.rank_zero_iff_diagonal_eq_top {ι : Type u_1} [Fintype ι] (s : State ι) :
              rank s = 0 ↔ diagonalSpace ↑s = ⊤

              Equivalently, at termination every binary vector is a diagonal label.