NavierStokesAnalyticLegitimate
plain-language theorem explainer
The legitimacy predicate on Navier-Stokes analytic display records is the constantly-true proposition: every such display is legitimate by definition. Auditors of the Navier-Stokes energy bridge cite it when filling the generic ProblemAudit interface. The body is a one-line constant Prop, so no side conditions are imposed on the display fields.
Claim. For every Navier-Stokes analytic display record $d$ (energy certificate, cell resolution, energy depth, and display payload), the legitimacy predicate holds identically: $\mathrm{Legitimate}(d) \equiv \top$.
background
This module audits hard-problem certificates by packaging each bridge as a ProblemAudit: a completion map plus legitimacy and pathology predicates, with a conservatism check that the predicates only inspect the underlying certificate.
A Navier-Stokes analytic display is a domain-specific record bundling an energy certificate, a natural cell resolution, an energy depth, and a display payload. The legitimacy slot in the audit is a Prop-valued predicate on that record. Here the predicate is defined to be True for every input, so the analytic display path carries no extra legitimacy filter beyond the certificate itself.
Upstream, the display structure only records those four fields; it does not encode a separate analytic obstruction. Downstream conservatism then recovers the certificate by projection, matching the trivial legitimacy choice.
proof idea
There is no proof obligation. The definition is a one-argument Prop equal to True, ignoring its Navier-Stokes analytic display argument. No lemmas are applied; the body is the constant true proposition.
why it matters
The declaration fills the legitimate field of navierStokesAnalyticAudit, the ProblemAudit instance for the Navier-Stokes energy bridge. The companion theorem navierStokesAnalytic_conservative uses it to show Conservatism: legitimacy (and pathology) depend only on the embedded energy certificate, recovered as d.cert.
In the Recognition certificate-audit layer this is the deliberate choice that the analytic display path is always legitimate. Pathology, if any, is handled by the separate pathology predicate. It does not touch the forcing chain (T0-T8), RCL, or mass ladder; it is scaffolding for hard-problem certificate hygiene around the Navier-Stokes energy certificate siblings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.