constantStochastic3x3
plain-language theorem explainer
This definition constructs a uniform 3 by 3 matrix over the complex numbers whose every entry equals one third. Researchers building transfer kernels in the YM sector cite it when they need a constant stochastic matrix for bridge constructions. The body is a direct record literal that populates the matrix field of MatrixView.
Claim. Let $M$ be the $3times 3$ matrix over $mathbb{C}$ with every entry equal to $frac13$. The constant stochastic matrix on three indices is the MatrixView structure whose matrix component is exactly $M$.
background
MatrixView is the structure that packages a square matrix $A$ over $mathbb{C}$ indexed by a finite type $iota$ equipped with Fintype and DecidableEq. Here the index type is Fin 3, so the structure holds a $3times 3$ complex matrix. The module YM.Kernel works with transfer kernels and matrix bridges that act on these finite index sets.
proof idea
The definition is a direct record construction that sets the A field to the constant function returning the complex number one third.
why it matters
kernel3x3_with_bridge consumes this definition to produce a TransferKernel paired with a MatrixBridge. It supplies the uniform stochastic kernel required for the three-dimensional case, consistent with the eight-tick octave and D=3 forced in the UnifiedForcingChain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.