pith. machine review for the scientific record. sign in
structure

PvsNPMasterCert

definition
show as:
view math explainer →
module
IndisputableMonolith.Complexity.PvsNPAssembly
domain
Complexity
line
100 · github
papers citing
none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Complexity.PvsNPAssembly on GitHub at line 100.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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
 116  circuit_sep := circuitSeparation
 117
 118end -- noncomputable section
 119
 120end PvsNPAssembly
 121end Complexity
 122end IndisputableMonolith

papers checked against this theorem

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