ProblemAudit
plain-language theorem explainer
A Delta audit packages a continuum problem as native data, display data, and certificates, plus two display predicates (legitimate objects and pathologies) that both conserve under the completion. Anyone wiring finite-certificate reductions of hard continuum problems (Hodge, Navier–Stokes, certified displays) cites this interface. Pure structure definition: five fields, no proof obligations beyond the two conservativity witnesses.
Claim. A problem audit over native type $N$, display type $D$, and certificate type $\mathrm{Cert}$ is a completion (display map $N\to D$ with a certification relation $\mathrm{Cert}\to D\to\mathrm{Prop}$) together with two predicates on display data, legitimacy and pathology, each required to be conservative for that completion: every display point satisfying the predicate carries a finite/native certificate.
background
In the Primitive Recognition Calculus, continuum statements are not proved directly in the display language. They are audited through a completion interface: native data $N$ map to display data $D$, and certificates $\mathrm{Cert}$ witness display predicates. Upstream, Completion is exactly that pair (display map, certifies relation). A predicate on $D$ is conservative for the completion when every display datum that satisfies it is covered by some certificate—the finite-certificate transfer principle used throughout this module family.
The local setting is quantized proof method: hard continuum problems are reduced by showing that both the good objects and the pathologies descend to finite certificates. The sibling notion of finite reduction is the claim that legitimate objects and pathologies both so descend. Spatial dimension $D=3$ and related RS constants appear in the import graph but are not parameters of this structure; the audit is type-parametric.
Conservativity is the hinge. Without it, a display predicate could hold for continuum junk that never touches native certificates, and the audit would not transfer.
proof idea
No proof body: this is a structure definition. The five fields are the data of an audit. The two Prop fields legitimate_conservative and pathology_conservative are not derived here; each concrete audit (identity certificate audit, Hodge analytic audit, certified display audit, Navier–Stokes audits) supplies those witnesses by applying the corresponding conservativity lemmas for its chosen completion and predicates.
why it matters
This is the common carrier type for hard-problem certificate audits in the PRC stack. Downstream, identity certificate audit, certified display audit, Hodge algebraic/analytic/certified-display audits, and Navier–Stokes analytic/certified-display audits are all values of this structure. Strong closure certificates in the Delta-native strong closure module consume the same audit pattern when packaging closure entries.
In Recognition Science terms, the point is methodological rather than a T0–T8 forcing step: continuum claims (display side) are only admitted when both success and failure modes are certificate-covered on the native side. That is the finite-certificate reduction slogan attached to the structure. It does not itself solve Hodge or Navier–Stokes; it standardizes what a solved audit must look like so later closure registries can cite uniform heads.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.