CertifiedDisplayLegitimate
plain-language theorem explainer
Every certified display is declared legitimate by definition: the predicate on continuum-facing objects that carry a finite certificate is the constant true proposition. Auditors of hard-problem certificate pipelines cite it as the legitimacy slot in the display audit record. The body is the trivial constant True, not a derived argument.
Claim. For any types $\mathrm{Cert}$ and $\mathrm{Payload}$, and any continuum-facing display object that pairs a finite certificate with a payload tag, the legitimacy predicate on that display holds (it is the constant true proposition).
background
This module audits hard-problem certificates by separating finite native witnesses from continuum-facing display objects. A certified display is a pair: a certificate (the finite witness that grants authority) and a payload (an analytic or display-side tag). The structure is the completion interface from finite certificates to objects that can be shown on the continuum side.
Legitimacy and pathology are the two boolean-facing slots in a problem audit. Sibling audits (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge algebraic) use the same pattern: a completion map, a legitimacy predicate, a pathology predicate, and conservativity theorems tying them to the certificate layer. The CKM-style Cert structure upstream is the model of a finite witness with geometric and numerical match fields.
Locally, legitimacy for certified displays is intentionally vacuous: carrying a certificate is enough for the display to count as legitimate in this audit layer.
proof idea
Definitional, not proved. The predicate ignores its certified-display argument and reduces to the constant proposition True. No lemmas are applied; there is no tactic script. Downstream conservativity only needs that every completed display satisfies the predicate, which holds immediately.
why it matters
Fills the legitimacy field of the certified-display problem audit. The audit record wires completion, legitimacy, pathology, and the conservativity pair; this definition is the legitimacy component. The companion theorem certifiedDisplay_conservative shows both legitimacy and pathology are conservative for the display completion map, and the first conjunct is immediate from this constant-true predicate.
In the Recognition foundation layer this is scaffolding hygiene, not a physics claim: it standardizes how finite certificates (eight-tick, phi-ladder, forcing-chain style witnesses) are allowed to authorize continuum displays without smuggling extra analytic hypotheses into the legitimacy slot. It does not touch T5–T8 or the mass ladder directly; it only keeps the hard-problem audit API uniform.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.