Exact label compression with a sharp leading round count #

The numerical budget has leading term 2n rounds and 4n copies. The tail bound is for the explicit uniform-X-label process in ExactLearning; the connection of that process to Born-rule circuit execution is proved separately.

source

def LeanPool.SingleCopyStabilizer.SharpExactLearning.meanBound (n : ℕ) :

ℝ

The reciprocal progress-rate bound for n qubits.

Equations

LeanPool.SingleCopyStabilizer.SharpExactLearning.meanBound n = 2 * ↑n + 4

Instances For

source

noncomputable def LeanPool.SingleCopyStabilizer.SharpExactLearning.roundBudget (n : ℕ) (δ : ℝ) :

ℕ

Explicit round budget preserving the leading coefficient two.

Equations

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

Instances For

source

noncomputable def LeanPool.SingleCopyStabilizer.SharpExactLearning.copyBudget (n : ℕ) (δ : ℝ) :

ℕ

Two fresh copies per round, followed by one final computational readout.

Equations

LeanPool.SingleCopyStabilizer.SharpExactLearning.copyBudget n δ = 2 * LeanPool.SingleCopyStabilizer.SharpExactLearning.roundBudget n δ + 1

Instances For

source

theorem LeanPool.SingleCopyStabilizer.SharpExactLearning.meanBound_pos (n : ℕ) :

0 < meanBound n

source

theorem LeanPool.SingleCopyStabilizer.SharpExactLearning.roundBudget_formula (n : ℕ) (δ : ℝ) :

roundBudget n δ = ⌈2 * ↑n + 4 + 8 * √((2 * ↑n + 4) * Real.log (1 / δ)) + 64 * Real.log (1 / δ)⌉₊

Expanded round budget with no hidden asymptotic constants.

source

theorem LeanPool.SingleCopyStabilizer.SharpExactLearning.confidence_log_nonneg (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) :

0 ≤ Real.log (1 / δ)

The logarithmic confidence parameter is nonnegative on the intended range.

source

theorem LeanPool.SingleCopyStabilizer.SharpExactLearning.roundBudget_upper (n : ℕ) (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) :

↑(roundBudget n δ) < 2 * ↑n + 5 + 8 * √((2 * ↑n + 4) * Real.log (1 / δ)) + 64 * Real.log (1 / δ)

Rounding adds less than one round to the explicit real-valued budget.

source

theorem LeanPool.SingleCopyStabilizer.SharpExactLearning.copyBudget_upper (n : ℕ) (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) :

↑(copyBudget n δ) < 4 * ↑n + 11 + 16 * √((2 * ↑n + 4) * Real.log (1 / δ)) + 128 * Real.log (1 / δ)

The resulting copy budget has leading coefficient four.

source

theorem LeanPool.SingleCopyStabilizer.SharpExactLearning.copyBudget_linear (n : ℕ) (hn : 1 ≤ n) (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) :

↑(copyBudget n δ) < 136 * (↑n + Real.log (1 / δ))

An explicit universal-constant copy bound, valid for at least one qubit. The constant is conservative; copyBudget_upper retains the sharper leading coefficient four and square-root confidence term.

source

theorem LeanPool.SingleCopyStabilizer.SharpExactLearning.rank_le_qubit_count {ι : Type u_1} [Fintype ι] (s : ExactLearning.State ι) :

ExactLearning.rank s ≤ Fintype.card ι

The exact process's rank is bounded by the number of qubits.

source

theorem LeanPool.SingleCopyStabilizer.SharpExactLearning.exact_progress_parameter {ι : Type u_1} [Fintype ι] [DecidableEq ι] (s : ExactLearning.State ι) :

FiniteProbability.progressProbability (ExactLearning.rank s) ≤ ExactLearning.process.progressMass s

Every needed progress-rate estimate is proved for the exact process.

source

theorem LeanPool.SingleCopyStabilizer.SharpExactLearning.exact_process_mean_bound {ι : Type u_1} [Fintype ι] (s : ExactLearning.State ι) :

∑ j ∈ Finset.range (ExactLearning.rank s), 1 / FiniteProbability.progressProbability (j + 1) ≤ meanBound (Fintype.card ι)

The reciprocal-sum hypothesis is discharged for every exact-process state.

source

theorem LeanPool.SingleCopyStabilizer.SharpExactLearning.compression_failure_probability_after_budget {ι : Type u_1} [Fintype ι] [DecidableEq ι] (s : ExactLearning.State ι) (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) (T : ℕ) (hT : roundBudget (Fintype.card ι) δ ≤ T) :

ExactLearning.process.failureProbability T s ≤ δ

The explicit exact-learning label process succeeds with confidence 1-δ at every round count at least the sharp-leading-term budget. All progress-rate and reciprocal-sum hypotheses are proved, not assumed.

source

theorem LeanPool.SingleCopyStabilizer.SharpExactLearning.compression_failure_probability {ι : Type u_1} [Fintype ι] [DecidableEq ι] (s : ExactLearning.State ι) (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) :

ExactLearning.process.failureProbability (roundBudget (Fintype.card ι) δ) s ≤ δ

Exact label compression in ceil(2n+4+8√((2n+4)log(1/δ))+64log(1/δ)) rounds, with failure probability at most δ.