MatrixBridge
plain-language theorem explainer
MatrixBridge defines a structure requiring that the continuous linear operator T of a TransferKernel equals the continuous linear map induced by the matrix A of a MatrixView. Researchers constructing Yang-Mills kernels from matrix representations cite it to enforce operator-matrix consistency in the Recognition framework. The definition is a direct structural encoding with a single equality field and no proof steps.
Claim. A structure MatrixBridge(ι, K, V) for finite type ι, where K is a transfer kernel with continuous linear operator T : (ι → ℂ) →_L (ι → ℂ) and V is a matrix view with matrix A ∈ M_{ι×ι}(ℂ), satisfying T = CLM.ofLM(Matrix.toLin' A).
background
TransferKernel packages a single continuous linear operator T on the space of functions from ι to ℂ. MatrixView packages a matrix A over ι × ι with complex entries and supplies the auxiliary CLM.ofLM that converts any linear map into its continuous counterpart. The local setting is the YM.Kernel module, which supplies the basic objects for building transfer kernels that later appear in matrix representations of Yang-Mills operators.
proof idea
The declaration is a structure definition whose single field directly records the required equality K.T = CLM.ofLM(Matrix.toLin' V.A); no lemmas or tactics are invoked.
why it matters
MatrixBridge is the type used by buildKernelFromMatrix to return a concrete kernel together with its matrix witness, and by KernelHasMatrixView to assert non-emptiness of the bridge. It therefore supplies the interface that lets downstream geometry and kernel constructions (including the 3 × 3 stochastic example) treat operator and matrix views interchangeably inside the Recognition Science pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.