Rational-Dilation Yoneda Externalization

We discharge the externalization component of Target 2 of the No-Phantom Language program by exhibiting, for any finite-rank reproducing-kernel-Hilbert-space (RKHS) detector on the Burnol/Blaschke defect object, a corresponding family of rational-dilation Yoneda representables in the presheaf category $\mathsf{PSh}(\mathbf{D}_\mathbb{Q})$. The key identification, available from Vol5's $\texttt{NoPhantomConcreteAtoms}$ surface, is the definitional identity $\mathbf{D}_\mathbb{Q}\text{-objects} \equiv \mathcal{N}_K$ (Nyman kernels), which makes every rational-dilation generator already a Nyman representable.

We prove, in the Lean 4 formalization, the principal theorem $\texttt{burnol\_blaschke\_detector\_externalization}: \texttt{RKHSDetectorExternalizationToRationalRepresentables}\;K_B, S, R$ relative to a vol5-exposed introduction rule for the opaque predicate $\texttt{DefectDetectedByRationalDilationRepresentable}$, and we characterize precisely the missing introduction rule in an obstruction module when the rule is not exposed. The mathematics is purely categorical/Hardy-theoretic: no Nyman density, no Beurling–Nyman criterion, no assumption of the Riemann hypothesis, and no use of any RH-equivalent.