module module

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.HardProblemCertificateAudits`

show as: view Lean formalization →

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

generate prose now

used by (2)

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

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaNativeAnalysis module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaNativeStrongClosure module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.QuantizedProofMethod module_import

declarations in this module (56)

inductive PrimeCriticalLineCert L34
inductive NavierStokesEnergyCert L41
inductive YangMillsGapCert L48
inductive HodgeAlgebraicCert L55
def CertificateLegitimate L63
def CertificatePathology L68
def identityCertificateAudit L71
def primeCriticalLineAudit L78
def navierStokesEnergyAudit L81
def yangMillsGapAudit L85
def hodgeAlgebraicAudit L88
theorem primeCriticalLine_finiteReduction L91
theorem navierStokesEnergy_finiteReduction L94
theorem yangMillsGap_finiteReduction L97
theorem hodgeAlgebraic_finiteReduction L100
theorem hard_problem_certificate_audits_headline L106
structure CertifiedDisplay L119
def certifiedDisplayCompletion L127
def CertifiedDisplayLegitimate L132
def CertifiedDisplayPathology L133
theorem certifiedDisplay_conservative L135
inductive PrimeDisplayPayload L146
inductive NavierStokesDisplayPayload L155
inductive YangMillsDisplayPayload L164
inductive HodgeDisplayPayload L173
def certifiedDisplayAudit L181
def primeCertifiedDisplayAudit L189
def navierStokesCertifiedDisplayAudit L194
def yangMillsCertifiedDisplayAudit L199
def hodgeCertifiedDisplayAudit L204
theorem certified_display_audits_headline L214
structure PrimeAnalyticDisplay L227
structure NavierStokesAnalyticDisplay L235
structure YangMillsAnalyticDisplay L243
structure HodgeAnalyticDisplay L251
def primeAnalyticCompletion L258
def navierStokesAnalyticCompletion L262
def yangMillsAnalyticCompletion L267
def hodgeAnalyticCompletion L271
def PrimeAnalyticLegitimate L275
def PrimeAnalyticPathology L276
def NavierStokesAnalyticLegitimate L277
def NavierStokesAnalyticPathology L278
def YangMillsAnalyticLegitimate L279
def YangMillsAnalyticPathology L280
def HodgeAnalyticLegitimate L281
def HodgeAnalyticPathology L282
theorem primeAnalytic_conservative L284
theorem navierStokesAnalytic_conservative L289
theorem yangMillsAnalytic_conservative L294
theorem hodgeAnalytic_conservative L299
def primeAnalyticAudit L304
def navierStokesAnalyticAudit L311
def yangMillsAnalyticAudit L319
def hodgeAnalyticAudit L326
theorem domain_specific_analytic_audits_headline L337