primeCertifiedDisplayAudit
plain-language theorem explainer
Specializes the certified-display Δ-audit to the prime-critical-line problem: native certificates are the finite inventory (prime window, Euler-product ledger, zero-obstruction witness), and displays are continuum-facing objects tagged by zeta, critical-strip, or off-line payloads. Anyone wiring the RH-side Delta bridge or the four-problem headline cites this. Proof is a one-line specialization of the generic certified-display audit.
Claim. The prime-critical-line certified-display audit is the $\Delta$-audit whose native certificate type is the finite prime-critical-line inventory, whose display type is the certified display of that inventory with prime display payloads (zeta, critical strip, off-line zero), and whose certificate parameter is again that finite inventory.
background
In the quantized-proof method, a ProblemAudit is the $\Delta$-audit of a continuum problem: a completion map from native certificates through displays, plus legitimacy and pathology predicates that are conservative for that completion.
Here the native side is the finite prime-critical-line certificate inventory (finite prime window, Euler-product balance ledger, zero-obstruction witness). The display side is a certified display: a continuum-facing object that pairs such a certificate with a payload tag (zeta display, critical-strip display, or off-line zero display). The certificate gives the display its authority.
The generic certified-display audit already packages completion, legitimacy, pathology, and the two conservativity proofs for any certificate/payload pair with an inhabited payload. This declaration simply instantiates that package on the prime-critical-line types.
proof idea
One-line wrapper: apply the generic certified-display audit at the prime-critical-line certificate type and the prime display-payload type. No extra obligations; the inhabited-payload instance is the default zeta tag, and conservativity is inherited from the generic certified-display lemmas.
why it matters
Feeds the certified-display audits headline, which asserts finite reduction for all four hard-problem display audits (prime-critical-line, Navier–Stokes energy, Yang–Mills gap, Hodge algebraic). Downstream doc: "the hard-problem stubs now have a non-identity display interface: every admissible display object carries an explicit finite certificate... This is still not a solution of the four problems; it is the correct Delta bridge shape for later analytic interfaces."
In the Recognition foundation layer this is the RH-facing leg of that bridge: continuum zeta/critical-strip language is forced to carry a finite native witness before any legitimacy claim is admitted. It does not touch T5–T8 or the mass ladder; it only fixes the audit shape for later analytic interfaces on the prime-critical-line side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.