navierStokesAnalyticCompletion
plain-language theorem explainer
Packages each Navier–Stokes energy certificate as a trivial analytic display (zero cell resolution, zero energy depth, smooth-flow tag) and certifies by matching the embedded certificate. Downstream audits and conservativity proofs cite it as the completion half of the NS analytic bridge. The body is a two-field structure instance: a constant display map and equality on the cert projection.
Claim. The Navier–Stokes analytic completion is the map sending each energy certificate $c$ to the display record $(c, 0, 0, \mathrm{smoothFlow})$, together with the certification relation that holds precisely when the certificate equals the display's embedded certificate field. It is an instance of the generic completion interface from native certificates to analytic displays.
background
In the Primitive Recognition Calculus, hard-problem audits are factored through a generic Completion interface: a display map from native data $N$ to display data $D$, plus a certification predicate relating certificates to displays. Conservativity then means every display satisfying a legitimacy or pathology predicate carries a finite native certificate.
For Navier–Stokes, the native side is the finite inventory NavierStokesEnergyCert (finite cell decomposition, energy-transfer ledger, blowup-obstruction witness). The display side is NavierStokesAnalyticDisplay, a record holding a certificate, two natural-number resolution parameters, and a payload tag (smoothFlowDisplay, energyCascadeDisplay, or blowupDisplay).
This module builds certificate audits for several Millennium-type problems (primes, NS, Yang–Mills, Hodge) under a common completion-and-conservativity pattern imported from CompletionConservativity and the quantized proof method.
proof idea
Pure structure instance, no tactics. The display field is the constant packaging $c \mapsto \langle c, 0, 0, \mathrm{smoothFlowDisplay}\rangle$. The certifies field is propositional equality of the certificate with the display's cert projection. No upstream lemmas are applied; the definition only assembles the two fields required by Completion.
why it matters
Feeds two immediate parents: navierStokesAnalyticAudit, which wires this completion into a full ProblemAudit with legitimacy and pathology predicates, and navierStokesAnalytic_conservative, which proves both predicates are conservative for this completion by the one-line witness $\langle d.\mathrm{cert}, \mathrm{rfl}\rangle$.
Within Recognition Science this is scaffolding for the NS energy-transfer audit bridge, not a PDE existence theorem. It sits in the foundation layer that packages hard-problem claims as finite certificate inventories with display conservativity, parallel to the prime-critical-line, Yang–Mills gap, and Hodge algebraic audits in the same module. It does not invoke the forcing chain (T0–T8), RCL, or phi-ladder mass formulas; those live elsewhere.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.