NavierStokesEnergyCert
plain-language theorem explainer
Enumerates the three finite certificate kinds used to audit Navier–Stokes energy transfer in the Recognition calculus: finite cell decomposition, an energy-transfer ledger, and a blow-up obstruction witness. Anyone wiring a ProblemAudit or display bridge for the NS energy problem cites this inventory. It is a plain inductive definition with DecidableEq and Repr, not a proved statement.
Claim. There is a finite inductive inventory of certificate kinds for the Navier–Stokes energy-transfer audit, with exactly three constructors: a finite cell decomposition, an energy-transfer ledger, and a blow-up obstruction witness. Equality of constructors is decidable.
background
The module HardProblemCertificateAudits packages Millennium-style targets as finite certificate inventories plus audit maps. Each hard problem gets a small inductive type of certificate tags, then identity or display audits that check legitimacy and pathology without claiming a full analytic solution.
For Navier–Stokes, the classical open question is global regularity of smooth solutions to the 3D incompressible equations and control of energy cascade versus finite-time blow-up. In this framework the audit is reduced to three named certificate roles: decomposing the domain into finitely many cells, maintaining a ledger of energy transfer between cells, and exhibiting a witness that obstructs blow-up.
Upstream ledger and mass notions (column mass as induction measure, gap factors, finite-dimensional Hamiltonian generators) supply the bookkeeping language; the certificate type itself only names the audit slots.
proof idea
No proof body: the declaration is an inductive type with three nullary constructors and derived DecidableEq and Repr instances. Mathematical content is the enumeration of certificate roles, not a derivation. Downstream audits treat inhabitants as tags in identity or display ProblemAudit records.
why it matters
This inventory is the certificate parameter for every Navier–Stokes audit in the module: the identity energy audit, the certified-display audit, the analytic display structure (cert field), analytic completion, and the full analytic ProblemAudit. It sits beside sibling inventories for the prime critical line, Yang–Mills gap, and Hodge algebraicity, giving a uniform hard-problem certificate surface.
In Recognition Science terms it does not solve the Clay problem; it fixes the finite checklist against which energy-transfer and blow-up-obstruction claims are scored. Parent uses treat it as both the certificate and (in the identity audit) the display type, so the audit is conservative by construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.