kernel3x3_with_bridge
plain-language theorem explainer
kernel3x3_with_bridge supplies the explicit 3x3 transfer kernel whose operator is induced by the constant matrix of all entries 1/3, paired with the matrix bridge that witnesses the equality. Workers on discrete Yang-Mills models in the Recognition framework cite it for the uniform stochastic case over Fin 3. Construction is a direct one-line application of buildKernelFromMatrix to the constantStochastic3x3 view.
Claim. Let $V$ be the matrix view over $Fin 3$ whose entries are all equal to $1/3$. Define the dependent pair $(K, B)$ where $K$ is the transfer kernel whose continuous linear operator $T$ satisfies $Tf = (1/3) sum_j f(j)$ for functions $f$ on $Fin 3$, and $B$ is the matrix bridge asserting that $T$ equals the linear map induced by the matrix of $V$.
background
In the YM.Kernel module the structure TransferKernel ι packages a continuous linear map $T : (ι → ℂ) →L[ℂ] (ι → ℂ)$. The companion structure MatrixBridge ι K V records the single field intertwine : K.T = CLM.ofLM (Matrix.toLin' V.A), which asserts that the kernel operator is exactly the linearization of the supplied matrix view V. constantStochastic3x3 is the concrete MatrixView (Fin 3) whose matrix A has every entry equal to 1/3. The upstream definition buildKernelFromMatrix takes any such V and returns the pair consisting of the kernel built from Matrix.toLin' V.A together with the reflexivity proof of the intertwining equation.
proof idea
One-line wrapper that applies buildKernelFromMatrix (ι := Fin 3) to constantStochastic3x3, which internally constructs the TransferKernel whose T is CLM.ofLM (Matrix.toLin' V.A) and supplies the bridge with intertwine := rfl.
why it matters
Supplies a concrete 3x3 stochastic kernel instance inside the Yang-Mills kernel infrastructure. It instantiates the matrix-bridge construction for the uniform case, consistent with the three spatial dimensions forced by the eight-tick octave in the unified forcing chain. No downstream uses are recorded yet, so its role in larger YM proofs or curvature functionals remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.