yangMillsAnalytic_conservative
plain-language theorem explainer
The Yang–Mills analytic completion is conservative for both the legitimate and pathology predicates: every display satisfying either predicate carries a certificate. Certificate auditors cite this when assembling the Yang–Mills analytic problem audit. The proof is a one-line constructor that recovers the embedded certificate by reflexivity.
Claim. The Yang–Mills analytic completion is conservative for the legitimate predicate and for the pathology predicate: each is certificate-covered, so any display datum satisfying either predicate is witnessed by a certificate equal to the display's own certificate field.
background
In the Primitive Recognition Calculus, a completion $C$ packages native certificates into display data together with a certifies relation. Conservativity for a predicate $P$ on displays means $P$ is certificate-covered: whenever $P(d)$ holds, some certificate $c$ satisfies $\mathrm{certifies}(c,d)$. Equivalently, there are no non-native artifacts for $P$.
Here the completion maps a Yang–Mills gap certificate $c$ to an analytic display $\langle c, 0, 0, \mathrm{connectionDisplay}\rangle$, and certifies by equality of the certificate field. Both the legitimate and pathology predicates on analytic displays are the constantly-true proposition, so every display is in scope; conservativity then reduces to exhibiting the embedded certificate.
This sits in the hard-problem certificate audit layer, which records finite, certificate-level reductions for several classical open problems (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge) without claiming analytic resolution of those problems.
proof idea
One-line wrapper. Split the conjunction with constructor. On each conjunct, introduce a display $d$ and the (vacuous) predicate hypothesis, then return $\langle d.\mathrm{cert}, \mathrm{rfl}\rangle$: the certificate is the display's own cert field, and certifies holds by reflexivity of equality. No external lemmas are needed beyond the definitions of ConservativeFor and the completion.
why it matters
Feeds directly into yangMillsAnalyticAudit, which packages the completion, the two predicates, and the two conservativity halves into a single ProblemAudit record. That audit is the certificate-level bookkeeping entry for the Yang–Mills analytic display path alongside sibling audits (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge algebraic).
Within Recognition Science this is scaffolding hygiene, not a mass or forcing-chain result: it guarantees the analytic display layer introduces no uncertified legitimate or pathological claims. It does not touch T5–T8, the RCL, or the mass ladder; it only certifies that the audit interface for this hard-problem display is conservative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.