buildKernelFromMatrix
plain-language theorem explainer
buildKernelFromMatrix constructs a TransferKernel and its MatrixBridge from any MatrixView on a finite index set by converting the matrix to a continuous linear map. It is invoked when instantiating concrete kernels such as the 3x3 case in the Yang-Mills sector. The definition is realized by a direct let-binding that applies CLM.ofLM to the matrix linearization and closes the bridge by reflexivity.
Claim. Let ι be a finite type equipped with decidable equality. Given a matrix view V whose matrix A maps ι × ι to ℂ, there exists a transfer kernel K whose continuous linear operator T is obtained by applying the continuous-linear-map constructor to the linear map induced by A, together with a matrix bridge witnessing that T equals the linear map induced by A.
background
In the YM.Kernel module a MatrixView ι is a structure containing a single field A : Matrix ι ι ℂ. A TransferKernel ι is a structure containing a single field T : (ι → ℂ) →L[ℂ] (ι → ℂ). A MatrixBridge ι K V is a structure whose single field intertwine asserts the equality K.T = CLM.ofLM (Matrix.toLin' V.A). The construction therefore supplies a canonical way to promote a matrix representation to a continuous linear operator while recording the identification. The surrounding Recognition Science setting draws on upstream definitions such as the dimensionless bridge ratio K = φ^{1/2} and the integration gap A = 1, which fix the scaling conventions for kernels operating on the phi-ladder in D = 3 dimensions.
proof idea
The definition proceeds by a direct let-binding that sets K to the TransferKernel whose T field is CLM.ofLM (Matrix.toLin' V.A). The returned sigma pair is then formed with a MatrixBridge whose intertwine field is instantiated by rfl, which succeeds because the construction matches the bridge condition by definition.
why it matters
This definition supplies the uniform mechanism that kernel3x3_with_bridge invokes to produce a concrete 3x3 transfer kernel from the constant stochastic matrix view. It thereby anchors the Yang-Mills kernel infrastructure to the Recognition framework's linear-algebra primitives, consistent with the eight-tick octave and spectral emergence used elsewhere in the monolith. No open scaffolding questions are discharged here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.