navierStokesEnergyAudit
plain-language theorem explainer
Packages the Navier-Stokes energy-transfer problem as a Delta audit whose node, data, and certificate types are the same finite three-element inventory (cell decomposition, energy ledger, blowup obstruction). Cited by the hard-problem audit headline and by the NS energy finite-reduction theorem. One-line application of the identity certificate-audit constructor.
Claim. The Navier-Stokes energy audit is the identity $\Delta$-audit on the finite certificate type $\{$finite cell decomposition, energy-transfer ledger, blowup-obstruction witness$\}$, with node, data, and certificate sorts all equal to that type.
background
In the quantized-proof layer, a ProblemAudit is the Delta audit of a continuum problem: a completion map from a node type $N$ through data $D$ to certificates $Cert$, plus two predicates on $D$ (legitimate vs pathology) that are conservative for that completion. Conservativity means the predicates respect the discrete completion, so continuum claims reduce to finite certificate checks.
NavierStokesEnergyCert is the finite inventory for the NS energy-transfer audit: three constructors (finite cell decomposition, energy-transfer ledger, blowup-obstruction witness). The identity audit constructor builds a ProblemAudit $C,C,C$ whose completion is the identity completion on $C$, with the module-wide legitimate and pathology predicates, each proved conservative by the shared identity-conservative lemma.
This module supplies audit schemas for several hard problems (prime critical line, NS energy, Yang-Mills gap, Hodge algebraic), not continuum solutions.
proof idea
One-line wrapper: instantiate the identity certificate audit at the Navier-Stokes energy certificate type. That constructor fills completion with the identity completion, legitimate and pathology with the shared CertificateLegitimate and CertificatePathology predicates, and both conservativity fields with identity_conservative on those predicates.
why it matters
Gives the NS energy-transfer problem a concrete finite certificate inventory inside the Primitive Recognition Calculus audit layer. Downstream, navierStokesEnergy_finiteReduction applies problemAudit_finiteReduction to this audit to obtain HasFiniteReduction. The headline theorem hard_problem_certificate_audits_headline conjoins that fact with the parallel audits for the prime critical line, Yang-Mills gap, and Hodge algebraic problems, stating explicitly that these are audit schemas, not solutions of the underlying continuum problems. In the Recognition framework this is scaffolding for discrete energy-transfer bookkeeping (cell decomposition, ledger, blowup obstruction), aligned with the finite-reduction method rather than a claim to resolve the Clay NS regularity problem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.