structure
definition
PvsNPResolutionStatus
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Complexity.PvsNPAssembly on GitHub at line 85.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
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
106 dissolution : PvsNPDissolution
107 circuit_sep : CircuitSeparation
108
109def pvsNPMasterCert : PvsNPMasterCert where
110 laplacian := jcostLaplacianCert
111 spectral := spectralGapCert
112 frustration := jfrustrationCert
113 non_natural := nonNaturalnessCert
114 lower_bound := circuitLowerBoundCert
115 dissolution := dissolution_holds