The 0-Hecke Monoid H₀(A₃): Algebraic Structure, Yang–Baxter Equation, and Kashiwara Crystal Bases

We study the 0-Hecke monoid H₀(A₃) associated with the Coxeter system of type A₃. This finite monoid of 24 elements admits rich algebraic structure. We establish that the defining braid relations constitute the Yang–Baxter equation, and that the monoid is isomorphic to Kashiwara's crystal base B(A₃) at q = 0. The coproduct structure forces the coupling constant λ = −1 through idempotence constraints. We introduce the commutation deficit C(K) = K(K−3)/2 and prove that K = 3 is the unique positive integer satisfying C(K) = 0. The commutators of the three coproducts generate an su(2) Lie algebra with Casimir eigenvalues 3n. The 24 elements correspond bijectively to vertices of the truncated octahedron. Seven theorems are formally verified in Lean 4; cross-validation comprises 59 independent tests achieving complete agreement. Keywords: 0-Hecke monoid, Yang–Baxter equation, Kashiwara crystal, formal verification MSC 2020: 20M30, 17B37, 05E10, 16T25, 68V15