PrimeDisplayPayload
plain-language theorem explainer
Three-tag enumeration labeling what a prime-critical-line audit display is showing: the zeta function itself, the critical strip, or an off-line zero witness. Downstream analytic-display records and certified-display audits index on this tag. It is a plain inductive definition with decidable equality and a default inhabited instance (zeta display).
Claim. An inductive type of display-payload tags for the prime-critical-line certificate audit, with three constructors: zeta-function display, critical-strip display, and off-critical-line zero display. Equality is decidable, and the default inhabited value is the zeta-function tag.
background
The module HardProblemCertificateAudits packages audit scaffolding for several classical hard problems (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge algebraicity). Each problem gets a certificate type, optional pathology tags, and a display layer that records what analytic object is being exhibited.
For the prime-critical-line bridge, the certificate type is PrimeCriticalLineCert. The companion structure PrimeAnalyticDisplay packages that certificate together with a prime-window radius, a balance depth, and a displayKind field. The present declaration supplies the finite set of allowed values for that field.
The surrounding audit API is generic: certifiedDisplayAudit and Completion records wire a certificate type to a payload tag type so that displays can be checked for legitimacy without baking analytic content into the tag layer.
proof idea
No proof content. The declaration is a three-constructor inductive type with DecidableEq and Repr derived automatically, plus a one-line Inhabited instance whose default is the zeta-display constructor. There are no lemmas, tactics, or reductions.
why it matters
This tag type is the payload parameter for the prime-critical-line certified-display audit and for the analytic-display record used by the prime analytic completion. Downstream, PrimeAnalyticDisplay stores a displayKind of this type; primeCertifiedDisplayAudit instantiates the generic certified-display audit at (PrimeCriticalLineCert, PrimeDisplayPayload); and primeAnalyticCompletion hard-wires the zeta-display constructor when completing a certificate into a display.
In the Recognition Science foundation layer this is bookkeeping, not physics: it keeps the prime-critical-line hard-problem certificate path typed and auditable. It does not itself encode the eight-tick register, J-cost uniqueness, or any forcing-chain step (T0–T8). Its role is to make the display side of the prime audit mechanically distinguishable from sibling audits (Navier–Stokes, Yang–Mills, Hodge).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.