primeAnalytic_conservative
plain-language theorem explainer
The prime-analytic completion is conservative for both the legitimate and pathology predicates: every prime-analytic display is certificate-covered. Auditors of the Riemann / prime-critical-line hard-problem package cite this when assembling the problem audit. The proof is a one-line constructor that exhibits each display's own certificate and closes equality by reflexivity.
Claim. The prime-analytic completion $C$ is conservative for the legitimate predicate $L$ and for the pathology predicate $P$ on prime-analytic displays: both $L$ and $P$ are certificate-covered by $C$. (Here $L$ and $P$ are the constantly-true predicates on the display type.)
background
In the Primitive Recognition Calculus, a completion packages how native certificates are displayed and when a certificate certifies a display. Conservativity for a predicate means the predicate is certificate-covered: every display satisfying the predicate carries some certificate that certifies it. A non-native artifact would be a display satisfying the predicate with no certificate.
The prime-analytic completion maps a prime-critical-line certificate to a display with zeta payload and certifies exactly when the certificate equals the display's stored cert. The legitimate and pathology predicates used here are both the constantly-true proposition on prime-analytic displays, so coverage reduces to "every display has a certifying certificate."
This module audits hard-problem certificates (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge) by packaging completion, legitimate/pathology predicates, and conservativity witnesses into a single problem audit.
proof idea
One-line wrapper. constructor splits the conjunction into two ConservativeFor goals. Each expands to certificate-covered: for an arbitrary display $d$ (the predicate hypothesis is vacuous since both predicates are True), exhibit the witness certificate $d.\mathrm{cert}$ and close the certifies equality by rfl, matching the completion's certifies clause $c = d.\mathrm{cert}$.
why it matters
Supplies both conjuncts required by primeAnalyticAudit, the problem-audit record for the prime-critical-line / zeta-display package: that audit sets legitimate_conservative and pathology_conservative to the two projections of this theorem. Without conservativity, the audit could not claim that legitimate and pathological displays are certificate-covered under the prime-analytic completion.
In the broader hard-problem certificate audit suite (siblings for Navier–Stokes, Yang–Mills, Hodge), this is the prime-analytic instance of the same conservativity pattern: trivial predicates plus a cert-equals-display completion make coverage immediate. It does not resolve the Riemann hypothesis; it only certifies that the audit interface is conservative for its chosen predicates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.