NavierStokesAnalyticDisplay
plain-language theorem explainer
Bundles a Navier–Stokes energy certificate with cell resolution, energy depth, and a display payload tag (smooth flow, cascade, or blowup). Used by the analytic audit and completion maps that package finite certificates for the NS bridge. Pure record type: no proof content.
Claim. A Navier–Stokes analytic display is a 4-tuple $(c, n_{\mathrm{cell}}, d_E, \tau)$ where $c$ is a finite energy-transfer certificate (cell decomposition, transfer ledger, or blowup obstruction), $n_{\mathrm{cell}}, d_E \in \mathbb{N}$ are resolution and energy-depth parameters, and $\tau$ is a display tag among smooth flow, energy cascade, and blowup.
background
The HardProblemCertificateAudits module packages Millennium-style targets as finite certificate inventories plus display records that the Primitive Recognition Calculus can audit. For Navier–Stokes, the certificate side is the inductive type with constructors finite cell decomposition, energy-transfer ledger, and blowup-obstruction witness. The display side tags the intended analytic picture: smooth flow, energy cascade, or blowup.
This structure is the domain-specific analytic display record for the NS bridge: it pairs one certificate with two natural-number bookkeeping fields (cell resolution and energy depth) and one payload tag. Upstream Hilbert-display machinery shows how $F_{RS}$ amplitudes become finite Hilbert vectors; here the analogous role is a finite, inspectable NS audit object rather than a continuum PDE solution.
Sibling audits (prime critical line, Yang–Mills gap, Hodge) use the same pattern: certificate inductive, display payload, then completion/legitimate/pathology hooks.
proof idea
No proof: this is a structure definition with four fields and a derived Repr instance. Inhabitants are built by structure notation, as in the completion map that sends a certificate $c$ to $\langle c, 0, 0, \mathrm{smoothFlowDisplay}\rangle$.
why it matters
Feeds the NS analytic completion, legitimacy, pathology, and the assembled ProblemAudit that ties certificates to displays. Without this record, the audit cannot attach resolution/depth metadata or choose a display tag for the energy-transfer story.
In the broader Recognition stack, hard-problem bridges are reduced to finite certificate audits rather than open continuum analysis. The NS case sits beside Yang–Mills gap and prime-critical-line audits in the same module. Framework landmarks that motivate finiteness (eight-tick register, finite Hilbert display) explain why a discrete cell/energy bookkeeping object is the right carrier, even though this declaration itself does not invoke T0–T8 or the RCL equation.
Legitimacy and pathology are currently trivial (True), so the structure is scaffolding for a later non-vacuous audit rather than a finished regularity theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.