structure definition def or abbrev

`PvsNPMasterCert`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

pvsNPMasterCert in IndisputableMonolith.Complexity.PvsNPAssembly decl_use

depends on (8)

Lean names referenced from this declaration's body.

CircuitSeparation in IndisputableMonolith.Complexity.CircuitLedger decl_use
CircuitLowerBoundCert in IndisputableMonolith.Complexity.CircuitLowerBound decl_use
JCostLaplacianCert in IndisputableMonolith.Complexity.JCostLaplacian decl_use
JFrustrationCert in IndisputableMonolith.Complexity.JFrustration decl_use
NonNaturalnessCert in IndisputableMonolith.Complexity.NonNaturalness decl_use
PvsNPDissolution in IndisputableMonolith.Complexity.PvsNPAssembly decl_use
SpectralGapCert in IndisputableMonolith.Complexity.SpectralGap decl_use
laplacian in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use