KernelHasMatrixView
plain-language theorem explainer
KernelHasMatrixView defines a predicate on a finite index set ι asserting that a transfer kernel possesses a matrix representation exactly when a nonempty matrix bridge exists between its continuous linear operator and the supplied matrix view. Workers on recognition-theoretic Yang-Mills kernels would cite it to enforce the operator-to-matrix link inside kernel constructions. The definition is a direct one-line wrapper that reduces the property to nonemptiness of the bridge type.
Claim. Let ι be a finite type. For a transfer kernel K consisting of a continuous linear map T from (ι → ℂ) to itself and a matrix view V supplying an explicit matrix A over ι, the predicate holds precisely when the type of matrix bridges between K and V is nonempty.
background
In the YM.Kernel module a TransferKernel over ι is the structure containing a continuous linear operator T : (ι → ℂ) →L[ℂ] (ι → ℂ). A MatrixView over the same ι (assumed Fintype and DecidableEq) is the structure carrying an explicit matrix A : Matrix ι ι ℂ. The local setting therefore supplies the minimal data needed to ask whether an abstract operator kernel admits a concrete matrix presentation. Upstream results supply the dimensionless ratio K = ϕ^{1/2} from Constants and the J-cost potential V(φ_inf) = J(1 + φ_inf) from Cosmology, both of which sit in the same recognition manifold but are not invoked inside this declaration.
proof idea
The definition is a one-line wrapper that applies the Nonempty predicate directly to the type MatrixBridge ι K V. No lemmas are called and no tactics are used; the body simply declares the existence condition via the bridge structure.
why it matters
This definition supplies the interface that lets transfer kernels be viewed as matrices inside the YM kernel layer, preparing the ground for sibling constructions such as buildKernelFromMatrix. It therefore participates in the recognition composition law by furnishing the matrix data that later steps can feed into the phi-ladder and the eight-tick octave. No downstream uses are recorded yet, so its precise role in deriving D = 3 or the alpha band remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.