HH18 Parameterized: depth Two Child Selected Port Output eq selected Logical Port Transported Accepted Output
ProvedQEC.Distillation.HH18Parameterized.depthTwoChildSelectedPortOutput_eq_selectedLogicalPortTransportedAcceptedOutputlean-qecert-4a64933quantum-computingquantum-error-correction
The actual selected child output is the established one-level selected output at the derived physical input rate.
Preamble
import Definitions.Def_QEC_Distillation_Core_DependentBatch import Definitions.Def_QEC_Distillation_LowOverheadProtocol_Parameterized_ResourceMeasurement import Definitions.Def_QEC_Distillation_LowOverheadProtocol_Parameterized_SelectedPort import Definitions.Def_QEC_Distillation_LowOverheadProtocol_Parameterized_DepthTwoRouting set_option autoImplicit false noncomputable section open QEC open QEC.Distillation open QEC.Distillation.HH18Parameterized open Coding Semantics open Coding.PauliSymplectic open Coding.ReedMuller Coding.PuncturedReedMuller open Semantics.Qubit open scoped BigOperators open Triorthogonal.BH12NoisyInjection open Triorthogonal.BH12NoisyInjection.OneQubit attribute [local instance 100] Fintype.ofFinite
Formal statement
theorem QEC.Distillation.HH18Parameterized.depthTwoChildSelectedPortOutput_eq_selectedLogicalPortTransportedAcceptedOutput
{w r m : Nat} (h : Admissible w r m) (hdegree : 3 * r < m)
(epsilon : HH18NoisyInput.DiagonalErrorRate) (child : LogicalSite m w)
(hhalf : selectedLogicalPortRawError h hdegree epsilon child ≤ 1 / 2)
(port : LogicalSite m w) :
depthTwoChildSelectedPortOutput h hdegree epsilon child hhalf port =
selectedLogicalPortTransportedAcceptedOutput h hdegree
(selectedLogicalPortNextInputRate h hdegree epsilon child hhalf) port := by sorrySource