`pvsNPMasterCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Complexity.PvsNPAssembly
domain: Complexity
line: 109 · 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 109.

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

formal source

 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.