HH18 Parameterized: syndrome Outcome accepted iff

import Definitions.Def_QEC_Distillation_LowOverheadProtocol_Parameterized_Syndrome
import Definitions.Def_QEC_Distillation_LowOverheadProtocol_Parameterized_Postselection
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
attribute [local instance 100] Fintype.ofFinite
universe u

theorem QEC.Distillation.HH18Parameterized.syndromeOutcome_accepted_iff (w r m : Nat) (syndrome : Syndrome w r m) :
    syndromeOutcome w r m syndrome = .accepted ↔
      syndrome = HH18PuncturedReedMuller.allPositiveSyndrome w r m := by sorry