navierStokesCertifiedDisplayAudit
plain-language theorem explainer
Specializes the certified-display audit interface to the Navier-Stokes energy-transfer problem: finite certificates (cell decomposition, energy ledger, blowup obstruction) paired with continuum display tags (smooth flow, cascade, blowup). Anyone citing the hard-problem display headline or the NS finite-reduction bridge uses this. One-line specialization of the generic certified-display audit constructor.
Claim. The Navier-Stokes energy-transfer problem admits a $\Delta$-audit whose native certificate type is the finite inventory $\{\text{cell decomposition},\ \text{energy ledger},\ \text{blowup obstruction}\}$, whose display type is a certified display carrying one of those certificates together with a payload tag in $\{\text{smooth flow},\ \text{energy cascade},\ \text{blowup}\}$, and whose certificate type on the completion side is again that same finite inventory.
background
In the Primitive Recognition Calculus, a continuum hard problem is not attacked by writing PDE estimates directly. Instead one builds a $\Delta$-audit: a ProblemAudit package with a completion map from a native finite certificate type $N$ into a display type $D$, plus two conservative predicates (legitimate vs pathological displays). Conservativity means the predicates depend only on the certificate the display carries.
For Navier-Stokes the native inventory is three finite tags: a cell decomposition of the domain, an energy-transfer ledger, and a blowup-obstruction witness. The display side is a CertifiedDisplay: a pair (certificate, payload) where the payload is one of smooth-flow, energy-cascade, or blowup. The generic constructor certifiedDisplayAudit wires the default completion, the legitimate/pathology predicates, and the conservativity proofs for any inhabited payload type.
This module sits downstream of QuantizedProofMethod, which defines the audit structure and the finite-reduction criterion used by the headline theorem.
proof idea
One-line wrapper. Instantiate the generic certified-display audit at certificate type NavierStokesEnergyCert and payload type NavierStokesDisplayPayload. The generic constructor already supplies completion, legitimate/pathology predicates, and both conservativity proofs; no extra obligations are discharged here.
why it matters
Feeds the conjunction in certified_display_audits_headline, which asserts that the four hard-problem display audits (prime critical line, Navier-Stokes, Yang-Mills, Hodge) each satisfy HasFiniteReduction. The headline doc-comment is explicit: this is still not a solution of the four problems; it is the correct $\Delta$ bridge shape for later analytic interfaces.
In the Recognition framework the point is architectural. Continuum claims about smooth NS flow or finite-time blowup are forced to route through a finite certificate inventory before they count as audited displays. That matches the quantized-proof method's demand that legitimate and pathological judgments be conservative under completion. The declaration closes the NS slot in that four-problem bridge; analytic content (energy inequalities, Beale-Kato-Majda-type controls) remains future work on the payload side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.