CertificateMap
plain-language theorem explainer
A certificate map assigns to every display element a typed finite distinction certificate for a predicate P. Continuum-legitimacy arguments cite it as the data package that turns “P holds on d” into finite certificate evidence. It is a pure structure definition: one map field plus a vacuous soundness field.
Claim. Fix tag type $\mathrm{Tag}$, display type $D$, and predicate $P:D\to\mathrm{Prop}$. A certificate map consists of a function $c:D\to\mathrm{TypedFiniteDistinction}(\mathrm{Tag})$ together with the (vacuous) soundness condition that $P(d)$ implies $\top$.
background
In the Primitive Recognition Calculus, continuum-level statements about displays must be backed by finite data. A typed finite distinction certificate is a pair $(\mathrm{size}:\mathbb{N},\mathrm{tag}:\mathrm{Tag})$: a finite size together with a tag naming the distinction regime that produced it.
The surrounding module develops finite-certificate transfer: when a completion is conservative for a display predicate, legitimacy and obstruction facts pass between the continuum statement and finite certificates. Display maps (e.g. Hilbert display of $F_{RS}$ amplitudes) supply the concrete $D$ on which $P$ is evaluated.
This structure is the data carrier for that transfer. The soundness field is intentionally trivial ($P(d)\to\top$), so the map itself does not yet enforce semantic correctness of the certificates; legitimacy is recovered by a one-line wrapper downstream.
proof idea
No proof: this is a structure definition. Two fields are declared. cert sends each display element to a TypedFiniteDistinction Tag. sound is the proposition $\forall d,, P(d)\to\top$, which is definitionally inhabited and carries no content. Instantiation is by supplying any such cert map (and the trivial soundness proof).
why it matters
Parent use is certificateMap_legitimate: any certificate map immediately yields a legitimate continuum statement, i.e. every display witness of $P$ has some finite typed distinction certificate. That theorem is the entry point for the module’s transfer lemmas (conservative_completion_transfers, obstruction_descends, finite_certificate_transfer).
In the Recognition framework this is scaffolding for the claim that continuum physics statements (displays, amplitudes, winding data) remain finitely certifiable, consistent with the forcing chain’s finite discrete skeleton (eight-tick octave, $D=3$). It does not itself force $\varphi$ or $J$; it only packages the certificate side of the conservativity story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.