LegitimateContinuumStatement
plain-language theorem explainer
A continuum display predicate is legitimate precisely when every witness admits a finite typed distinction certificate. Foundation workers cite this when stating what a certificate map must deliver before conservative completion can transfer finite data. The body is a one-line universal quantification over display witnesses.
Claim. For types $\mathrm{Tag}$ and $D$ and a predicate $P:D\to\mathrm{Prop}$, the continuum statement $P$ is legitimate when $\forall d\in D$, if $P(d)$ holds then there exists a typed finite distinction certificate with tag type $\mathrm{Tag}$ (finite size together with a regime tag).
background
In the Primitive Recognition Calculus, continuum-level display predicates on a type $D$ are not trusted on their own. A typed finite distinction certificate packages a natural-number size with a tag naming the distinction regime that produced it. That structure is the finite witness the rest of the module moves around.
The local setting is finite-certificate transfer under conservative completion: continuum statements about displays must be backed by finite certificates before one may push them through a completion and still retain a finite obstruction or certificate on the discrete side. Spatial dimension $D=3$ appears among imports as the forced T8 value, but this definition itself is dimension-agnostic.
Legitimacy is the Prop-level gate: every display witness of $P$ must yield a nonempty finite certificate of the given tag type.
proof idea
Pure definition. The body is the universal claim that every $d:D$ satisfying $P$ produces a nonempty typed finite distinction (finite size plus tag). No lemmas are applied; downstream theorems discharge the definition by exhibiting an explicit certificate map.
why it matters
This is the gate predicate for the finite-certificate transfer layer. The immediate consumer is the theorem that every certificate map witnesses legitimacy: given a map sending each display witness to a typed finite distinction, the continuum statement is legitimate by construction.
That legitimacy hypothesis then feeds conservative-completion transfer and obstruction-descent results in the same module: only legitimate continuum statements are allowed to move finite certificates across a completion without inventing new continuum data. In the broader Recognition forcing chain this keeps continuum talk tethered to finite typed distinctions, consistent with the discrete eight-tick and $D=3$ scaffolding upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.