Finite classical exact-learning transcripts

Every possible returned description contains exactly the prescribed number of round records. The copy and gate bounds therefore apply to the actual classical output distribution, rather than an unrelated arbitrary list.

@[reducible, inline]

noncomputable abbrev LeanPool.SingleCopyStabilizer.Transcript.transcriptPMF {ι : Type u_1} [Fintype ι] [DecidableEq ι] (T : ℕ) (S : PureStabilizerState ι) : PMF (OutputCorrectness.Description ι)

The physical experiment retaining its circuit record and final readout.

Equations

• LeanPool.SingleCopyStabilizer.Transcript.transcriptPMF T S = LeanPool.SingleCopyStabilizer.OutputCorrectness.descriptionPMF T S

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

Its decoded interpretation is exactly the proved output-state law.

theorem LeanPool.SingleCopyStabilizer.Transcript.supported_length {ι : Type u_1} [Fintype ι] [DecidableEq ι] (T : ℕ) (S : PureStabilizerState ι) (d : OutputCorrectness.Description ι) (hd : d ∈ (transcriptPMF T S).support) : d.1.length = T

Every possible transcript records exactly one outcome per scheduled round, including zero differences that append no quantum gates.

theorem LeanPool.SingleCopyStabilizer.Transcript.zero_of_length_ne {ι : Type u_1} [Fintype ι] [DecidableEq ι] (T : ℕ) (S : PureStabilizerState ι) (d : OutputCorrectness.Description ι) (hlen : d.1.length ≠ T) : (transcriptPMF T S) d = 0

Histories of the wrong length have exactly zero output probability.

theorem LeanPool.SingleCopyStabilizer.Transcript.supported_copy_count {ι : Type u_1} [Fintype ι] [DecidableEq ι] (T : ℕ) (S : PureStabilizerState ι) (d : OutputCorrectness.Description ι) (hd : d ∈ (transcriptPMF T S).support) : ExactResources.protocolCopyCount d.1 = 2 * T + 1

The returned finite description corresponds to exactly 2T+1 consumed input copies, for every possible run and independently of success.

theorem LeanPool.SingleCopyStabilizer.Transcript.supported_circuit_gate_count {ι : Type u_1} [Fintype ι] [DecidableEq ι] (T : ℕ) (S : PureStabilizerState ι) (d : OutputCorrectness.Description ι) (hd : d ∈ (transcriptPMF T S).support) : ExactResources.listCircuitGateCount d.1 ≤ (Fintype.card ι + 1) * T

At most (n+1)T elementary instructions describe the final circuit.

theorem LeanPool.SingleCopyStabilizer.Transcript.supported_protocol_gate_cost {ι : Type u_1} [Fintype ι] [DecidableEq ι] (T : ℕ) (S : PureStabilizerState ι) (d : OutputCorrectness.Description ι) (hd : d ∈ (transcriptPMF T S).support) : ExactResources.protocolGateCost d.1 ≤ (Fintype.card ι + 1) * T ^ 2

All gates used on the fresh copies and final readout total at most (n+1)T², for every supported classical output description.

theorem LeanPool.SingleCopyStabilizer.Transcript.supported_protocol_gate_cost_two_n {ι : Type u_1} [Fintype ι] [DecidableEq ι] (T : ℕ) (S : PureStabilizerState ι) (d : OutputCorrectness.Description ι) (hd : d ∈ (transcriptPMF T S).support) (hn : 1 ≤ Fintype.card ι) : ExactResources.protocolGateCost d.1 ≤ 2 * Fintype.card ι * T ^ 2

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

Correctness stated directly on the recorded finite output, with any round count at least the proved confidence budget.