PrimeAnalyticDisplay
plain-language theorem explainer
Bundles a prime-critical-line certificate with a finite prime window radius, an Euler-product balance depth, and a display payload tag (zeta, critical strip, or off-line zero). Downstream audit and completion maps cite it as the analytic display type for the RH-style bridge. It is a plain record structure with no proof obligations.
Claim. A prime-analytic display is a record $(c, R, d, \tau)$ where $c$ is a finite prime-critical-line certificate (finite prime window, Euler-product balance ledger, or zero-obstruction witness), $R \in \mathbb{N}$ is a prime-window radius, $d \in \mathbb{N}$ is a balance depth, and $\tau$ is a display payload tag among zeta display, critical-strip display, and off-line-zero display.
background
The module HardProblemCertificateAudits packages finite certificate inventories and display records for several hard-problem bridges (primes/RH, Navier–Stokes energy, Yang–Mills gap, Hodge). Each bridge pairs a certificate enum with a domain-specific analytic display so that completion, legitimacy, and pathology predicates can be stated uniformly.
For the prime-critical-line bridge the certificate inventory is three tags: a finite prime window, an Euler-product balance ledger, and a zero-obstruction witness. The display payload tags mark which analytic face is being shown: the zeta function, the critical strip, or an off-line zero. The Hilbert-display layer upstream turns $F_{RS}$ amplitudes into finite Hilbert vectors; this structure is the corresponding bookkeeping record on the prime side, not an operator construction.
Local convention: displays carry explicit finite parameters (window radius, balance depth) so audits stay finitary rather than quantifying over infinite zero sets.
proof idea
No proof. The declaration is a structure (record type) with four fields and a derived Repr instance. Field types are the in-module certificate inductive, two natural-number parameters, and the prime display-payload inductive.
why it matters
This record is the display type in the prime analytic completion and the full prime analytic audit. Completion builds a default display from a certificate by fixing radius and depth to zero and tagging zeta display, then certifies by matching the embedded certificate. Legitimacy and pathology predicates are currently trivial (True) on every such display, so the structure mainly fixes the interface that a later non-trivial audit must inhabit.
In the Recognition stack this sits with other hard-problem certificate audits that keep bridges finitary: finite windows and balance ledgers rather than classical infinite analytic continuation. It does not itself force the critical line or invoke T0–T8; it only supplies the typed carrier those audits consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.