SK000A

squarefree_or_prime_square_divisor

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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.

Exact expanded first-order arithmetic 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)

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 30 exact native proof lines.

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

Proof neighborhood

Direct dependencies

SK0009 bounded_prime_square_divisor_search succ_le_succ Stable theorem; checked-use authorized

Direct dependents

SK000B squarefree_decomposition_bounded_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

Named ingredients (1)
bounded prime square divisor search

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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: LtDvdPrime
  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 exact command ledger · 30 lines
  1. 0001intro n
  2. 0002intro hn
  3. 0003have hsearch : (forall sfd_search_prime_decision_absent. (exists pvs_gap_decision_absentbound. pvs_gap_decision_absentbound + S (sfd_search_prime_decision_absent) = (S n)) -> (~((sfd_search_prime_decision_absent) = 1) /\ forall pvs_left_decision_absentdomain pvs_right_decision_absentdomain. (sfd_search_prime_decision_absent) = pvs_left_decision_absentdomain * pvs_right_decision_absentdomain -> pvs_left_decision_absentdomain = 1 \/ pvs_right_decision_absentdomain = 1) -> ~(exists pvs_factor_decision_absentsquare. (n) = (sfd_search_prime_decision_absent * sfd_search_prime_decision_absent) * pvs_factor_decision_absentsquare)) \/ exists p. (((exists pvs_gap_decision_presentbound. pvs_gap_decision_presentbound + S (p) = (S n)) /\ (((~((p) = 1) /\ forall pvs_left_decision_presentprime pvs_right_decision_presentprime. (p) = pvs_left_decision_presentprime * pvs_right_decision_presentprime -> pvs_left_decision_presentprime = 1 \/ pvs_right_decision_presentprime = 1) /\ (exists pvs_factor_decision_presentsquare. (n) = (p * p) * pvs_factor_decision_presentsquare)))))
  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