  72        decoder (BalancedParityHidden.restrict
  73          (BalancedParityHidden.enc b R) M) ≠ b
  74
  75theorem dissolution_holds : PvsNPDissolution where
  76  rhat_polytime := fun n f h =>
  77    let ⟨steps, a, hle, ha⟩ := sat_recognition_time_bound f h
  78    ⟨steps, a, hle, ha⟩
  79  unsat_obstruction := fun _n f h => unsat_cost_lower_bound f h
  80  local_blindness := fun _n M _hM decoder =>
  81    BalancedParityHidden.adversarial_failure M decoder
  82
  83/-! ## Status -/
  84
  85structure PvsNPResolutionStatus where
  86  conditional_proof_available : Bool
  87  dissolution_proved : Bool
  88  open_gap : String
  89  sorry_count_in_chain : ℕ
  90
  91def currentStatus : PvsNPResolutionStatus where
  92  conditional_proof_available := false
  93  dissolution_proved := true
  94  open_gap := "UniformTopologicalObstructionHyp: prove that for some fixed k, " ++
  95              "every UNSAT formula on n variables requires circuits of size >= 2^(n/k)."
  96  sorry_count_in_chain := 1
  97
  98/-! ## Master Certificate -/
  99
 100structure PvsNPMasterCert where
 101  laplacian : JCostLaplacianCert
 102  spectral : SpectralGapCert
 103  frustration : JFrustrationCert
 104  non_natural : NonNaturalnessCert
 105  lower_bound : CircuitLowerBoundCert

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.