NavierStokesDisplayPayload
plain-language theorem explainer
Three-valued tag type for how a Navier–Stokes energy certificate is displayed in the hard-problem audit layer: smooth flow, energy cascade, or blowup. Downstream analytic-display records and certified-display audits index on this tag. The definition is a plain inductive enumeration with decidable equality and default inhabitant smooth flow.
Claim. A finite enumeration of display kinds for Navier–Stokes certificate audits, with three constructors: smooth-flow display, energy-cascade display, and blowup display. The type carries decidable equality and a canonical default (smooth flow).
background
The module HardProblemCertificateAudits packages audit scaffolding for several Millennium-style hard problems (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge algebraicity). Each problem has a certificate type and a display layer that records how the certificate is presented for inspection.
For Navier–Stokes the certificate side is the energy certificate; the display side needs a small discrete label for the qualitative regime being shown. That label is this payload type. Sibling audits use analogous tag types (e.g. for Yang–Mills). Upstream imports supply the quantized proof-method infrastructure that turns certificates plus displays into ProblemAudit and Completion objects.
The three tags match the classical trichotomy in the Clay NS problem: global smooth solutions, cascade/turbulent energy transfer, and possible finite-time singularity.
proof idea
Definitional, not a proof. An inductive type with three nullary constructors, deriving DecidableEq and Repr. An Inhabited instance picks the smooth-flow constructor as the default value used when a completion or audit needs a canonical payload.
why it matters
Gives the display field of NavierStokesAnalyticDisplay (cert, cell resolution, energy depth, plus this kind tag) a closed finite type. navierStokesAnalyticCompletion hard-wires the smooth-flow tag when lifting an energy certificate into an analytic display. navierStokesCertifiedDisplayAudit builds a ProblemAudit over CertifiedDisplay parameterized by this payload, so every certified NS display is forced to declare one of the three regimes.
In the Recognition Science stack this sits in the foundation audit layer that bridges discrete recognition calculus to classical hard-problem statements. It does not itself invoke the forcing chain (T0–T8), RCL, or the mass ladder; it only classifies presentation modes for the NS energy certificate path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.