The Beal Symmetry Collision: A Machine-Certified Solution via p-adic Valuations

This paper presents a formal verification of the structural impossibility underlying the Beal Conjecture for coprime bases. By employing a p-adic valuation, we identify a fundamental disparity between the additive properties of powers and the multiplicative requirements of a z-th power. We demonstrate that for coprime integers a, b where aˣ + bʸ = cᶻ, there exists a prime p such that the valuation vₚ (aˣ + bʸ) = 1, whereas the Law of Symmetry requires vₚ (cᶻ) 0 z. For z > 2, this creates a non-conditional logical collision (1 = z k) machine-certified through the Lean 4 kernel.