navierStokesAnalyticAudit
plain-language theorem explainer
Packages the Navier–Stokes energy-transfer audit as a single problem-audit record: finite certificate inventory, analytic display type, trivial legitimate and pathology predicates, and a completion map proved conservative for both. Downstream headline theorems cite it to assert a finite-reduction interface for the NS stub. The body is pure field assembly from the completion def and the two projections of the conservativity theorem.
Claim. The Navier–Stokes analytic audit is the problem-audit package with certificate type the finite inventory $\{\text{finite cell decomposition},\ \text{energy-transfer ledger},\ \text{blow-up obstruction witness}\}$, display type carrying a certificate together with cell resolution, energy depth, and a display payload, completion sending each certificate $c$ to the smooth-flow display of $c$, and legitimate and pathology predicates both identically $\top$, each conservative for that completion.
background
The module builds domain-specific analytic audits for hard-problem stubs (primes, Navier–Stokes, Yang–Mills, Hodge). Each audit is a ProblemAudit record: a finite certificate type, a display type, a completion map from certificates to displays, and legitimate/pathology predicates on displays, together with proofs that both predicates are conservative for the completion.
For Navier–Stokes the certificate inventory is three tokens: finite cell decomposition, energy-transfer ledger, and blow-up obstruction witness. The analytic display records a certificate, a cell resolution, an energy depth, and a display payload. The completion used here always emits a smooth-flow payload with zero resolution and depth, and certifies by equality of the embedded certificate.
Legitimate and pathology predicates on these displays are both defined as the constant true proposition. Conservativity then reduces to recovering the display's own certificate, which the upstream conservativity theorem records as a pair of one-line witnesses.
proof idea
Definitional field fill-in, not a tactic proof. The completion field is the already-defined Navier–Stokes analytic completion (display of $c$ is the smooth-flow record with cert $c$; certifies is certificate equality). Legitimate and pathology are the constant-true predicates. The two conservativity fields are the left and right projections of the upstream theorem that both predicates are conservative for that completion (each proof is intro d _; exact ⟨d.cert, rfl⟩).
why it matters
Feeds the domain-specific analytic audits headline, which asserts finite reduction for the four hard-problem analytic audits (primes, Navier–Stokes, Yang–Mills, Hodge). That headline's doc-comment is explicit: the reductions still do not solve the problems; they fix the exact display interface that future analytic proofs must refine.
In the Recognition Science foundation layer this is scaffolding hygiene, not a PDE theorem. It places the classical Navier–Stokes regularity/energy question into the same quantized certificate-and-display shape used for the other stubs, so later work can attach real energy-transfer or blow-up-obstruction content without changing the audit API. No forcing-chain landmark (T5–T8, RCL, $\varphi$) is invoked here; the link is organizational.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.