Exact qubit learning: correctness and physical resources

This is the public combined theorem. The learner returns a finite recorded circuit and one computational-basis string. Its exact correctness probability, copy count, and interpreted elementary gate cost are proved together.

The confidence constants are conservative. Classical machine runtime and lower bounds are not asserted by this theorem.

noncomputable def LeanPool.SingleCopyStabilizer.ExactLearningTheorem.successProbability {ι : Type u_1} [Fintype ι] [DecidableEq ι] (T : ℕ) (S : PureStabilizerState ι) : ℝ

Real probability that the returned description is exactly the input pure state, with global phase ignored.

Equations

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

theorem LeanPool.SingleCopyStabilizer.ExactLearningTheorem.exact_learning {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : PureStabilizerState ι) (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) : have T := SharpExactLearning.roundBudget (Fintype.card ι) δ; 1 - δ ≤ successProbability T S ∧ ∀ d ∈ (OutputCorrectness.descriptionPMF T S).support, d.1.length = T ∧ ExactResources.protocolCopyCount d.1 = 2 * T + 1 ∧ ExactResources.protocolGateCost d.1 ≤ (Fintype.card ι + 1) * T ^ 2 ∧ InstructionSemantics.instructionsEquiv (ExactResources.circuitInstructions d.1) = Circuit.circuitEquiv d.1 ∧ Measurement.IsNormalized (Circuit.decode d.1 d.2)

Exact recovery at the explicit leading-2n round budget. Every possible execution uses 2T+1 copies and at most (n+1)T² elementary gate applications. The counted instructions implement the circuit used by the learned-state decoder; they are not merely a separate numerical cost assignment.

theorem LeanPool.SingleCopyStabilizer.ExactLearningTheorem.exact_learning_copy_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : PureStabilizerState ι) (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) (d : OutputCorrectness.Description ι) (hd : d ∈ (OutputCorrectness.descriptionPMF (SharpExactLearning.roundBudget (Fintype.card ι) δ) S).support) : ↑(ExactResources.protocolCopyCount d.1) < 4 * ↑(Fintype.card ι) + 11 + 16 * √((2 * ↑(Fintype.card ι) + 4) * Real.log (1 / δ)) + 128 * Real.log (1 / δ)

The number of copies at this budget has the explicit leading 4n bound.

theorem LeanPool.SingleCopyStabilizer.ExactLearningTheorem.exact_learning_copy_bound_linear {ι : Type u_1} [Fintype ι] [DecidableEq ι] (hn : 1 ≤ Fintype.card ι) (S : PureStabilizerState ι) (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) (d : OutputCorrectness.Description ι) (hd : d ∈ (OutputCorrectness.descriptionPMF (SharpExactLearning.roundBudget (Fintype.card ι) δ) S).support) : ↑(ExactResources.protocolCopyCount d.1) < 136 * (↑(Fintype.card ι) + Real.log (1 / δ))

Every supported output of the exact learner obeys an explicit O(n + log(1/δ)) copy bound with a universal constant.