Exact state reconstruction from the adaptive experiment's actual output. Correctness identifies amplitudes up to a unit-modulus global scalar.

def LeanPool.SingleCopyStabilizer.OutputCorrectness.SameRay {ι : Type u_1} (ψ φ : Measurement.Amplitude ι) : Prop

Equality of pure states up to a physically irrelevant global phase.

Equations

• LeanPool.SingleCopyStabilizer.OutputCorrectness.SameRay ψ φ = ∃ (c : ℂ), Complex.normSq c = 1 ∧ ψ = c • φ

theorem LeanPool.SingleCopyStabilizer.OutputCorrectness.sameRay_refl {ι : Type u_1} (ψ : Measurement.Amplitude ι) : SameRay ψ ψ

theorem LeanPool.SingleCopyStabilizer.OutputCorrectness.sameRay_inverse_iff {ι : Type u_1} (U : Measurement.Amplitude ι ≃ₗ[ℂ] Measurement.Amplitude ι) (ψ φ : Measurement.Amplitude ι) : SameRay ψ (U.symm φ) ↔ SameRay (U ψ) φ

Reversing a linear gate transports exactly the same global phase.

theorem LeanPool.SingleCopyStabilizer.OutputCorrectness.roundEquiv_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : Measurement.Bits ι) (b : ZMod 2) (ψ : Measurement.Amplitude ι) : (Circuit.roundEquiv u b) ψ = QuantumRound.applyRoundAmplitude u b ψ

def LeanPool.SingleCopyStabilizer.OutputCorrectness.outputPMF {ι : Type u_1} [Fintype ι] [DecidableEq ι] : ℕ → PureStabilizerState ι → PMF (Measurement.Amplitude ι)

The actual adaptive learner's returned amplitude. The terminal experiment reads one computational outcome. Each recursive step performs two fresh-copy Born measurements and the correction coin, then reverses the recorded round on the recursively decoded result.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.SingleCopyStabilizer.OutputCorrectness.outputPMF 0 x✝ = PMF.map LeanPool.SingleCopyStabilizer.Circuit.basis (LeanPool.SingleCopyStabilizer.Measurement.bornPMF x✝.amplitude ⋯)

@[reducible, inline]

abbrev LeanPool.SingleCopyStabilizer.OutputCorrectness.Description (ι : Type u_2) : Type u_2

Finite classical output: the chronological round records and one final computational-basis string. No unknown amplitudes are included in the output.

Equations

• LeanPool.SingleCopyStabilizer.OutputCorrectness.Description ι = (List (LeanPool.SingleCopyStabilizer.Circuit.Outcome ι) × LeanPool.SingleCopyStabilizer.Measurement.Bits ι)

def LeanPool.SingleCopyStabilizer.OutputCorrectness.descriptionPMF {ι : Type u_1} [Fintype ι] [DecidableEq ι] : ℕ → PureStabilizerState ι → PMF (Description ι)

The same physical experiment retaining its classical circuit description.

Equations

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

theorem LeanPool.SingleCopyStabilizer.OutputCorrectness.descriptionPMF_decode {ι : Type u_1} [Fintype ι] [DecidableEq ι] (t : ℕ) (S : PureStabilizerState ι) : PMF.map (fun (d : Description ι) => Circuit.decode d.1 d.2) (descriptionPMF t S) = outputPMF t S

Interpreting the returned finite description gives exactly the amplitude distribution in outputPMF.

theorem LeanPool.SingleCopyStabilizer.OutputCorrectness.description_normalized {ι : Type u_1} [Fintype ι] [DecidableEq ι] (d : Description ι) : Measurement.IsNormalized (Circuit.decode d.1 d.2)

Every classical description denotes a normalized pure state.

theorem LeanPool.SingleCopyStabilizer.OutputCorrectness.outputPMF_normalized {ι : Type u_1} [Fintype ι] [DecidableEq ι] (t : ℕ) (S : PureStabilizerState ι) (ψ : Measurement.Amplitude ι) (hψ : ψ ∈ (outputPMF t S).support) : Measurement.IsNormalized ψ

The learner's output distribution is supported on normalized amplitudes.

noncomputable def LeanPool.SingleCopyStabilizer.OutputCorrectness.outputFailure {ι : Type u_1} [Fintype ι] [DecidableEq ι] (t : ℕ) (S : PureStabilizerState ι) : ENNReal

Actual probability that the output fails to represent the input state. The Boolean pushforward avoids introducing a measure on amplitude space.

Equations

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

theorem LeanPool.SingleCopyStabilizer.OutputCorrectness.outputFailure_zero_of_rank_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : PureStabilizerState ι) (hrank : ExactLearning.rank (PhysicalSampling.labels S) = 0) : outputFailure 0 S = 0

At full diagonal rank the single final Born readout reconstructs the current input amplitude up to global phase with probability one.

theorem LeanPool.SingleCopyStabilizer.OutputCorrectness.outputFailure_succ {ι : Type u_1} [Fintype ι] [DecidableEq ι] (t : ℕ) (S : PureStabilizerState ι) : outputFailure (t + 1) S = ∑ o : ExactLearning.Outcome ι, (PhysicalSampling.outcomePMF S) o * outputFailure t (QuantumRound.quantumRound S o)

The output error is the Born-weighted mean of the errors of later rounds. Reversing a recorded Clifford cannot create a reconstruction error.

theorem LeanPool.SingleCopyStabilizer.OutputCorrectness.outputFailure_le_compression {ι : Type u_1} [Fintype ι] [DecidableEq ι] (t : ℕ) (S : PureStabilizerState ι) : outputFailure t S ≤ ENNReal.ofReal (PhysicalExactLearning.failureProbability t S)

The probability of returning the wrong state is at most the probability of incomplete diagonal compression in the actual physical experiment.

theorem LeanPool.SingleCopyStabilizer.OutputCorrectness.exact_learning_failure_probability {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : PureStabilizerState ι) (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) : outputFailure (SharpExactLearning.roundBudget (Fintype.card ι) δ) S ≤ ENNReal.ofReal δ

The actual learner returns the exact input pure state up to global phase, except with probability at most δ, at the proved leading-2n round budget.

theorem LeanPool.SingleCopyStabilizer.OutputCorrectness.exact_learning_failure_probability_after_budget {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : PureStabilizerState ι) (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) (T : ℕ) (hT : SharpExactLearning.roundBudget (Fintype.card ι) δ ≤ T) : outputFailure T S ≤ ENNReal.ofReal δ

theorem LeanPool.SingleCopyStabilizer.OutputCorrectness.description_failure_probability {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : PureStabilizerState ι) (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) : (PMF.map (fun (d : Description ι) => decide (SameRay S.amplitude (Circuit.decode d.1 d.2))) (descriptionPMF (SharpExactLearning.roundBudget (Fintype.card ι) δ) S)) false ≤ ENNReal.ofReal δ

The same correctness guarantee stated directly for the finite classical description that the learner returns.

theorem LeanPool.SingleCopyStabilizer.OutputCorrectness.bool_success_probability_ge (p : PMF Bool) (δ : ℝ) (hδ : 0 ≤ δ) (hfailure : p false ≤ ENNReal.ofReal δ) : 1 - δ ≤ (p true).toReal

For a Boolean correctness experiment, the success and failure probabilities sum to one.

theorem LeanPool.SingleCopyStabilizer.OutputCorrectness.description_success_probability {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : PureStabilizerState ι) (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) : 1 - δ ≤ ((PMF.map (fun (d : Description ι) => decide (SameRay S.amplitude (Circuit.decode d.1 d.2))) (descriptionPMF (SharpExactLearning.roundBudget (Fintype.card ι) δ) S)) true).toReal

Direct real-valued success guarantee for the returned classical circuit description: it exactly represents the input pure state with probability at least 1-δ.