certifiedDisplay_conservative
plain-language theorem explainer
The certified-display completion is conservative for both the legitimate and pathology predicates on certified displays: every display satisfying either predicate is certificate-covered. Audit authors cite this when packaging a ProblemAudit for hard-problem certificates. The proof is a two-branch constructor that recovers the carried certificate and closes by reflexivity.
Claim. For any types $\mathrm{Cert}$ and $\mathrm{Payload}$ with $\mathrm{Payload}$ inhabited, the certified-display completion is conservative for the legitimate predicate and conservative for the pathology predicate: every certified display satisfying either predicate is covered by the certificate it carries.
background
In the Primitive Recognition Calculus, a completion $C$ maps native certificates to display data and records when a certificate certifies a display. Conservativity for a predicate $P$ on displays means $P$ is certificate-covered: every display satisfying $P$ comes from some certificate under the completion's certifies relation. The doc states: "A completion is conservative for a predicate when the predicate is certificate-covered."
The certified-display completion sends each certificate $c$ to the display $\langle c, \mathrm{default}\rangle$ and certifies $d$ exactly when $c = d.\mathrm{cert}$. The two predicates used here, legitimate and pathology on certified displays, are both the constant-true proposition, so the conservativity claim is purely structural: every display is covered by its own certificate field.
This module sits in the hard-problem certificate audit layer, which packages finite certificates (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge algebraic) into a uniform ProblemAudit interface.
proof idea
Term-mode proof by constructor on the conjunction. Each conjunct is ConservativeFor, i.e. certificate-covered. For a display $d$ (the predicate hypothesis is discarded as True), return the pair $\langle d.\mathrm{cert}, \mathrm{rfl}\rangle$: the certificate is the display's own cert field, and the certifies equality holds by reflexivity. The two branches are identical.
why it matters
Feeds certifiedDisplayAudit, which builds a ProblemAudit whose legitimate_conservative field is the first conjunct of this theorem (and whose pathology side is the second). That audit is the uniform packaging layer for hard-problem certificates in the Primitive Recognition Calculus: finite certificates display as certified displays without introducing non-native artifacts.
Conservativity is the audit's guarantee that the legitimate and pathology sides introduce no certificate-free displays. In the Recognition framework this is bookkeeping for the foundation layer rather than a forcing-chain step (T0–T8); it keeps hard-problem certificate claims inside the certificate-covered fragment so later verification modules can treat displays as faithful projections of finite certs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.