A non-square natural number has a prime factor of odd multiplicity

If $a$ is a nonzero natural number that is not a perfect square then some prime $t$ divides $a$ to an odd multiplicity, i.e. $a.factorization\, t$ is not even. Mathlib has no $\mathbb{N}$-valued square predicate, so squares are phrased with $\exists y,\, y^2 = a$ to match the surrounding $k=5$ children. The proof uses the accepted bridge OddPerfectNumber.Kernel.isSq_iff_even_factorization (28b00e2d-2e78-4683-8075-7135bec4a50b), which characterises squares by even prime multiplicities: if every multiplicity were even then $a$ would be a square, so some $t$ has odd multiplicity; that multiplicity value is nonzero, so $t$ lies in the support of $a$, which makes $t$ a prime dividing $a$. This is the forcing half of the contextual two-prime argument and is elementary exponent bookkeeping; it encodes no conjecture-specific content.