certifiedDisplayAudit
plain-language theorem explainer
Packages a finite certificate type and an inhabited display payload into a full ProblemAudit whose continuum objects are certified displays. Anyone wiring a hard-problem stub (prime zeros, Navier–Stokes energy, Yang–Mills gap, Hodge) through the quantized-proof audit interface cites this. The body is a pure structure assembly: completion map plus the two trivial legitimacy/pathology predicates and their conservativeness halves.
Claim. For certificate type $C$ and inhabited payload type $P$, there is a problem audit whose native side is $C$, whose display side is the type of certified displays $\mathrm{CertifiedDisplay}(C,P)$ (pairs $(c,p)$ with $c\in C$ and $p\in P$), and whose certificate side is again $C$. Completion sends $c$ to the default-payload display $\langle c,\mathrm{default}\rangle$ and certifies a display by equality of certificates. Both the legitimate and pathology predicates on displays are the constantly-true proposition, and both are conservative for that completion.
background
In the quantized-proof method, a continuum hard problem is audited by a ProblemAudit: a completion interface from a native finite type $N$ to a display type $D$ with certificates $C$, together with two predicates on $D$ (legitimate vs pathology) that are required to be conservative for the completion. Conservativeness means the predicate on a display is decided entirely by the certificate it carries, so the continuum side cannot smuggle extra content past the finite witness.
A certified display is the minimal continuum-facing object that still carries authority: a pair of a finite certificate and an analytic/display-side payload tag. The completion map builds the default-payload display from a certificate and certifies any display by certificate equality. The legitimate and pathology predicates on certified displays are both defined as the constantly-true proposition True, so the audit is deliberately non-discriminating on the display side; discrimination lives in the certificate type itself.
The local module collects hard-problem certificate audits (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge algebraic cycles) under one display pattern. This definition is the shared audit skeleton those four specializations instantiate.
proof idea
Pure structure fill-in, not a tactic proof. The five fields of ProblemAudit are assigned directly: completion is certifiedDisplayCompletion (display $c\mapsto\langle c,\mathrm{default}\rangle$, certifies by $c=d.\mathrm{cert}$); legitimate and pathology are the constantly-true predicates CertifiedDisplayLegitimate and CertifiedDisplayPathology; the two conservativeness obligations are the left and right projections of the already-proved conjunction certifiedDisplay_conservative. No further rewriting or case analysis is required.
why it matters
This is the reusable audit constructor that turns any finite hard-problem certificate type into a continuum-facing ProblemAudit without inventing new analytic content. Downstream it is applied verbatim as primeCertifiedDisplayAudit, navierStokesCertifiedDisplayAudit, yangMillsCertifiedDisplayAudit, and hodgeCertifiedDisplayAudit, each specializing Cert and Payload to the corresponding certificate and display-payload types.
In the Recognition Science foundation layer this sits inside the Primitive Recognition Calculus: hard continuum claims are admitted only through a Delta audit whose continuum side is conservative for a finite certificate. The construction deliberately makes legitimacy and pathology trivial on the display, so all real content (and all future falsification) lives in the certificate type and its own audit path. It does not itself resolve any Millennium problem; it standardizes the display wrapper those certificate audits share, matching the module headline that the hard-problem stubs now have a certified-display audit interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.