Pure Algebraic Formulation of Casimir Variational Decomposition and Non-Commutative Arithmetic Heights: A Formally Verified Framework

We establish a self-contained, purely algebraic formulation of the variational decomposition of finite-dimensional representations over the complex Lie algebra sl2(C) and construct an arithmetic bridge to Diophantine geometry via non-commutative height functions.First, eliminating all physical heuristics (such as D-branes, dielectric polarizations, andgauge instantons), we define a canonical cubic-Casimir trace functional V on the categoryRepfd(sl2(C)). We prove that under norm-preserving bilinear decomposition, compositedimensional representations of rank n = ab (a,b ≥ 2) are strictly unstable with respectto V, relaxing unconditionally into tensor-product factors governed by the strictly positivequartic identity ab(a2 − 1)(b2 − 1) > 0. Consequently, the critical points of minimal functional value terminate uniquely at irreducible blocks whose dimensions are prime numbersp ∈ P. In the proof assistant Lean 4, we formalize this entire algebraic core and prove thebi-directional logical equivalence between representation-theoretic tensor irreducibility andclassical primality (IsPrimeDim(p) ↔ StandardPrime(p)) without axioms or circular hypotheses (sorry-free). Second, we translate this algebraic prime selection into Diophantinegeometry by constructing an arithmetic height function on the non-commutative direct sumalgebra An = ⨁︁p|nMp(C). We formulate a conditional characterization theorem establishing that the bounded determinantal distortion condition is sufficient to yield the classicalDiophantine radical bound c ≤ Cϵrad(abc)1+ϵ, elucidating its conceptual correspondence toMochizuki’s log-shells in Inter-Universal Teichm¨uller theory.