TypedFiniteDistinction
plain-language theorem explainer
A typed finite distinction certificate is a pair of a natural-number size and a tag naming the distinction regime that produced the finite data. It is the carrier type for continuum-legitimacy and certificate-transfer arguments in the Primitive Recognition Calculus. Anyone citing finite certificates for display predicates uses this structure. As a pure data definition there is no proof body.
Claim. Fix a tag type $T$. A typed finite distinction certificate over $T$ is a pair $(n,t)$ with $n\in\mathbb{N}$ and $t\in T$: finite size data together with a tag recording which distinction regime produced it.
background
The Primitive Recognition Calculus works with finite Hilbert displays of $F_{RS}$ amplitudes rather than raw continuum objects. A display turns an $F_{RS}[i]$ amplitude into a finite Hilbert vector; continuum claims about such displays are only admitted when every witness carries a finite certificate.
This module sits on completion conservativity: legitimate continuum statements must transfer along conservative completions, and obstructions must descend. The certificate is deliberately thin: a size in $\mathbb{N}$ plus an arbitrary tag type that labels the distinction regime (which forcing or recognition step produced the finite data).
Upstream active-edge and anchor constants ($A=1$ per tick) and the finite-dimensional recognition register set the scale at which "finite" is meaningful; the certificate itself does not encode those constants, only the size-and-tag pair.
proof idea
Pure structure definition: two fields, size : ℕ and tag : Tag, with no constructors beyond the default, no proofs, and no axioms. Downstream definitions pattern-match on this carrier.
why it matters
This is the atomic certificate type for FiniteCertificateTransfer. CertificateMap sends each display witness of a predicate $P$ to a typed finite distinction; LegitimateContinuumStatement asserts that every $d$ with $P,d$ yields a nonempty such certificate.
In the Recognition framework, continuum language is allowed only when it is backed by finite distinction data (aligned with the finite 8-tick register and conservative completion). Without this carrier, soundness and faithfulness of covers, obstruction descent, and the finite-certificate transfer theorem have nothing to map into. It does not itself close a T0–T8 forcing step; it supplies the data shape those transfer lemmas quantify over.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.