certificateMap_legitimate
plain-language theorem explainer
A certificate map for a display predicate yields continuum-statement legitimacy: every witness of P carries a finite typed distinction. Cite this when wiring finite certificates into continuum displays or conservative completions. The proof packages the map's cert field as a Nonempty witness in two tactics.
Claim. Let $P : D \to \mathrm{Prop}$ be a display predicate and $M$ a certificate map for $P$ (a function sending each $d \in D$ to a typed finite distinction, with a vacuous soundness side-condition). Then the continuum statement for $P$ is legitimate: for every $d$ with $P(d)$, the type of typed finite distinctions is nonempty.
background
In the Primitive Recognition Calculus, continuum claims about displays are admissible only when every witness is backed by a finite certificate. A typed finite distinction is a finite, tag-indexed certificate of distinction; the module treats these as the only legitimate witnesses that may lift to continuum language.
A certificate map assigns to each display point $d$ such a typed finite distinction, together with a soundness field that is presently the trivial proposition $\mathrm{True}$. Continuum-statement legitimacy is the Prop that every $d$ satisfying the display predicate $P$ yields a nonempty type of typed finite distinctions.
The surrounding module FiniteCertificateTransfer sits on CompletionConservativity and develops transfer of finite certificates under conservative completions of Hilbert displays. Spatial dimension $D=3$ appears in related foundation modules via the forcing chain (T8), but is not used in this declaration.
proof idea
Two-tactic term proof. Introduce a display witness $d$ and the hypothesis $P(d)$. Apply the certificate map's cert field at $d$ and wrap the resulting typed finite distinction in a Nonempty constructor. The soundness field of the map is unused because legitimacy only demands existence of a certificate, not a nontrivial soundness proof.
why it matters
This is the elementary bridge from the CertificateMap structure to LegitimateContinuumStatement inside FiniteCertificateTransfer. Sibling results (conservative_completion_transfers, obstruction_descends, finite_certificate_transfer) build the actual transfer theorems; this lemma is the definitional hinge they rely on when a map is already in hand.
In the Recognition framework it enforces the finite-certificate discipline on continuum language: continuum displays (Hilbert displays of F_RS amplitudes, eight-tick registers) may speak only through finite typed distinctions. That discipline is what keeps continuum statements from smuggling uncountable or non-constructive content past the forcing chain. No downstream used_by edges are recorded yet; the declaration is infrastructure for the transfer lemmas in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.