SK000A

squarefree_or_prime_square_divisor

Every positive input is squarefree or has a constructed actual prime-square divisor; no excluded-middle or factoring oracle is assumed.

Alpha v34 checked-use · first admitted v29 · independently kernel and Lean verified; not Stable

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

For n>1 the exponent gcd and a real beta table classify and witness all positive root degrees. The unit n=1 has a separate uniform certificate for every positive degree. Zero is excluded. NaturalSquarefreeDecomposition is deliberately distinct from the unrelated polynomial definition.

Exact theorem in conservative defined notation

∀ n. ¬n = 0 → Squarefree(n) ∨ (∃ x. Prime(x) ∧ Dvd(x · x,n))

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

Squarefree(n) · 1Lt(a,b) · 2Dvd(d,n) · 3Prime(p) · 3

Actual proof prerequisites

bounded_prime_square_divisor_searchsucc_le_succ · checked external prerequisite
Original expanded first-order statement 
forall n. ~(n = 0) -> (((~((n) = 0)) /\ (forall sfd_prime_decision_squarefree. (~((sfd_prime_decision_squarefree) = 1) /\ forall pvs_left_decision_squarefreedomain pvs_right_decision_squarefreedomain. (sfd_prime_decision_squarefree) = pvs_left_decision_squarefreedomain * pvs_right_decision_squarefreedomain -> pvs_left_decision_squarefreedomain = 1 \/ pvs_right_decision_squarefreedomain = 1) -> (exists pvs_le_gap_decision_squarefreebound. pvs_le_gap_decision_squarefreebound + (sfd_prime_decision_squarefree) = (n)) -> ~(exists pvs_factor_decision_squarefreesquare. (n) = (sfd_prime_decision_squarefree * sfd_prime_decision_squarefree) * pvs_factor_decision_squarefreesquare)))) \/ exists p. (~((p) = 1) /\ forall pvs_left_decision_prime pvs_right_decision_prime. (p) = pvs_left_decision_prime * pvs_right_decision_prime -> pvs_left_decision_prime = 1 \/ pvs_right_decision_prime = 1) /\ (exists pvs_factor_decision_divisor. (n) = (p * p) * pvs_factor_decision_divisor)

Complete tactic proof in conservative notation

All 30 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

30 script commands · 10 reading checkpoints · 1 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
bounded prime square divisor search
01Fix variables and assumptionsL1–2

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro n
  2. L2
    intro hn
02Establish hsearchL3–6

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bounded prime square divisor search.

  1. L3
    have hsearch : (∀ x. Lt(x,S n) → Prime(x) → ¬Dvd(x · x,n)) ∨ (∃ x. Lt(x,S n) ∧ (Prime(x) ∧ Dvd(x · x,n)))Definitions: Lt(x,S n)Prime(x)Dvd(x · x,n)Original native command in the exact edition
  2. L4
    specialize bounded_prime_square_divisor_search (S n)
  3. L5
    specialize bounded_prime_square_divisor_search (n)
  4. L6
    apply bounded_prime_square_divisor_search
03Separate the logical casesL7–9

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L7
    cases hsearch
  2. L8
    left
  3. L9
    split
04Use earlier factsL10–10

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L10
    exact hn
05Fix variables and assumptionsL11–14

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro p
  2. L12
    intro hp
  3. L13
    intro hle
  4. L14
    intro hdiv
06Use earlier factsL15–22

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L15
    specialize hsearch_left (p)
  2. L16
    apply hsearch_left
  3. L17
    specialize succ_le_succ (p)
  4. L18
    specialize succ_le_succ (n)
  5. L19
    apply succ_le_succ
  6. L20
    exact hle
  7. L21
    exact hp
  8. L22
    exact hdiv
07Separate the logical casesL23–26

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L23
    right
  2. L24
    cases hsearch_right
  3. L25
    cases hsearch_right_witness
  4. L26
    cases hsearch_right_witness_right
08Construct an explicit witnessL27–27

Supply the displayed value, then prove that it has the required property.

  1. L27
    exists x
09Separate the logical casesL28–28

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L28
    split
10Use earlier factsL29–30

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L29
    exact hsearch_right_witness_right_left
  2. L30
    exact hsearch_right_witness_right_right

Library-wide reading audit

Original defined command ledger · 30 lines
  1. 0001intro n
  2. 0002intro hn
  3. 0003have hsearch : (∀ x. Lt(x,S n) → Prime(x) → ¬Dvd(x · x,n)) ∨ (∃ x. Lt(x,S n) ∧ (Prime(x) ∧ Dvd(x · x,n)))
  4. 0004specialize bounded_prime_square_divisor_search (S n)
  5. 0005specialize bounded_prime_square_divisor_search (n)
  6. 0006apply bounded_prime_square_divisor_search
  7. 0007cases hsearch
  8. 0008left
  9. 0009split
  10. 0010exact hn
  11. 0011intro p
  12. 0012intro hp
  13. 0013intro hle
  14. 0014intro hdiv
  15. 0015specialize hsearch_left (p)
  16. 0016apply hsearch_left
  17. 0017specialize succ_le_succ (p)
  18. 0018specialize succ_le_succ (n)
  19. 0019apply succ_le_succ
  20. 0020exact hle
  21. 0021exact hp
  22. 0022exact hdiv
  23. 0023right
  24. 0024cases hsearch_right
  25. 0025cases hsearch_right_witness
  26. 0026cases hsearch_right_witness_right
  27. 0027exists x
  28. 0028split
  29. 0029exact hsearch_right_witness_right_left
  30. 0030exact hsearch_right_witness_right_right