primeAnalyticCompletion
plain-language theorem explainer
Embeds each finite prime-critical-line certificate into an analytic display record tagged as a zeta display with zero window radius and balance depth. The certification relation is equality of the certificate field. Downstream audits and conservativity proofs cite this completion as the native-to-display bridge for the prime-critical-line hard-problem certificate. The body is a two-field structure instance, not a derived argument.
Claim. The prime-analytic completion is the pair consisting of the display map $c \mapsto (c,\,0,\,0,\,\zeta\text{-display})$ from finite prime-critical-line certificates into analytic display records, and the certification predicate holding precisely when the certificate equals the certificate field of the display.
background
In the Primitive Recognition Calculus, a completion is an interface from native data $N$ to display data $D$ together with certificates $Cert$ for display predicates: it supplies a map $\mathrm{display}: N \to D$ and a relation $\mathrm{certifies}: Cert \to D \to \mathrm{Prop}$. The upstream doc states this cleanly: "A completion interface from native data $N$ to display data $D$, with certificates $Cert$ for display predicates $P$."
Here $N$ and $Cert$ are both the finite inventory PrimeCriticalLineCert (constructors: finite prime window, Euler-product balance ledger, zero-obstruction witness). Display data are PrimeAnalyticDisplay records: a certificate, a natural prime-window radius, a balance depth, and a payload tag from PrimeDisplayPayload (zeta display, critical-strip display, or off-line zero display).
The module packages hard-problem certificate audits (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge algebraic). This definition is the prime-analytic bridge inside that audit layer, not a statement about the Riemann hypothesis itself.
proof idea
Definitional structure instance for Completion. The display field packs the input certificate $c$ with defaults $\mathrm{primeWindowRadius}=0$, $\mathrm{balanceDepth}=0$, and payload zetaDisplay. The certifies field is propositional equality of $c$ with the display's certificate component. No lemmas are invoked; the body is pure field assignment.
why it matters
This completion is the native-to-display hinge for the prime-critical-line audit path. It is plugged directly into primeAnalyticAudit as the completion field of the problem-audit record (alongside legitimacy, pathology, and the two conservativity witnesses). The companion theorem primeAnalytic_conservative proves both legitimate and pathology predicates are conservative for this completion by recovering d.cert and reflexivity.
In the broader Recognition foundation, hard-problem audits separate finite native certificates from analytic display layers so that conservativity can be checked without smuggling infinitary analytic content into the certificate inventory. The zeta-display default marks the intended analytic face (Riemann zeta / critical-line language) while keeping window and depth at zero until a later refinement widens them. It does not close any Millennium problem; it only standardizes the certificate–display interface those audits consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.