ND0234

HasPrimeSquareDivisor(n)

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

A genuine prime p and an actual quotient witness p*p dividing n. This is not an asserted factorization oracle.

Conservative notation; not a theorem, primitive, or axiom.

Definition in prerequisite notation

∃ mv_square_prime_bottomlayer. Prime(mv_square_prime_bottomlayer) ∧ Dvd(mv_square_prime_bottomlayer · mv_square_prime_bottomlayer,n)

Only definitions earlier in this acyclic notation graph are used here.

Hygienic expanded first-order definition 
exists mv_square_prime_bottomlayer. ((~((mv_square_prime_bottomlayer) = 1) /\ forall pvs_left_bottomlayerprime pvs_right_bottomlayerprime. (mv_square_prime_bottomlayer) = pvs_left_bottomlayerprime * pvs_right_bottomlayerprime -> pvs_left_bottomlayerprime = 1 \/ pvs_right_bottomlayerprime = 1) /\ (exists pvs_factor_bottomlayerdivisor. ((n)) = (mv_square_prime_bottomlayer * mv_square_prime_bottomlayer) * pvs_factor_bottomlayerdivisor))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

Prime(p)Dvd(d,n)

Definitions depending on this notation

Mobius(n,z)

Checked theorems using this definition

MV0009 · mobius_value_exists