SK000B

squarefree_decomposition_bounded_exists

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

Finite prime-square search and ordinary bounded induction construct the squarefree kernel and its square-factor root for every positive input.

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 B n. ~(n = 0) -> (exists pvs_gap_decomposition_bound. pvs_gap_decomposition_bound + S (n) = (B)) -> exists r s. (((((~((r) = 0)) /\ (forall sfd_prime_decomposition_resultkernel. (~((sfd_prime_decomposition_resultkernel) = 1) /\ forall pvs_left_decomposition_resultkerneldomain pvs_right_decomposition_resultkerneldomain. (sfd_prime_decomposition_resultkernel) = pvs_left_decomposition_resultkerneldomain * pvs_right_decomposition_resultkerneldomain -> pvs_left_decomposition_resultkerneldomain = 1 \/ pvs_right_decomposition_resultkerneldomain = 1) -> (exists pvs_le_gap_decomposition_resultkernelbound. pvs_le_gap_decomposition_resultkernelbound + (sfd_prime_decomposition_resultkernel) = (r)) -> ~(exists pvs_factor_decomposition_resultkernelsquare. (r) = (sfd_prime_decomposition_resultkernel * sfd_prime_decomposition_resultkernel) * pvs_factor_decomposition_resultkernelsquare)))) /\ ((n) = (r) * ((s) * (s)))))

Constructive proof overview

Generated structural guide

Finite prime-square search and ordinary bounded induction construct the squarefree kernel and its square-factor root for every positive input.

The unchanged tactic script uses 10 declared prerequisites and contains 77 exact native proof lines.

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

Proof neighborhood

Direct dependencies

factor_permutation_below_zero_impossible Alpha theorem; checked-use authorized SK000A squarefree_or_prime_square_divisor mul_one Stable theorem; checked-use authorized factor_nonzero_right Alpha theorem; checked-use authorized proper_factor_lt Stable theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized SK0003 prime_square_ne_one lt_of_lt_of_le Stable theorem; checked-use authorized le_of_succ_le_succ Stable theorem; checked-use authorized SK0007 squarefree_square_factor_reassociate

Direct dependents

SK000C squarefree_decomposition_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

77 script commands · 26 reading checkpoints · 4 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 (3)
squarefree or prime square divisorprime square ne onesquarefree square factor reassociate

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–1

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

  1. L1
    intro B
02Induction on BL2–5

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction B
  2. L3
    intro n
  3. L4
    intro hn
  4. L5
    intro hbound
03Separate the logical casesL6–6

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

  1. L6
    exfalso
04Use earlier factsL7–9

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

  1. L7
    specialize factor_permutation_below_zero_impossible (n)
  2. L8
    apply factor_permutation_below_zero_impossible
  3. L9
    exact hbound
05Fix variables and assumptionsL10–12

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

  1. L10
    intro n
  2. L11
    intro hn
  3. L12
    intro hbound
06Establish hcaseL13–16

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

  1. L13
    have hcase : Squarefree(n) ∨ (∃ x. Prime(x) ∧ Dvd(x · x,n))Definitions: SquarefreeDvdPrime
  2. L14
    specialize squarefree_or_prime_square_divisor (n)
  3. L15
    apply squarefree_or_prime_square_divisor
  4. L16
    exact hn
07Separate the logical casesL17–17

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

  1. L17
    cases hcase
08Construct an explicit witnessL18–19

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

  1. L18
    exists n
  2. L19
    exists 1
09Separate the logical casesL20–20

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

  1. L20
    split
10Use earlier factsL21–21

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

  1. L21
    exact hcase_left
11Calculate and transport equalitiesL22–25

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L22
    symm
  2. L23
    trans n * 1
  3. L24
    congr
  4. L25
    refl
12Use earlier factsL26–27

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

  1. L26
    apply mul_one
  2. L27
    apply mul_one
13Separate the logical casesL28–30

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

  1. L28
    cases hcase_right
  2. L29
    cases hcase_right_witness
  3. L30
    cases hcase_right_witness_right
14Establish huL31–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor nonzero right.

  1. L31
    have hu : ~(x1 = 0)
  2. L32
    intro hzero
  3. L33
    specialize factor_nonzero_right (n)
  4. L34
    specialize factor_nonzero_right (x * x)
  5. L35
    specialize factor_nonzero_right (x1)
  6. L36
    apply factor_nonzero_right
  7. L37
    exact hn
  8. L38
    exact hcase_right_witness_right_witness
  9. L39
    exact hzero
15Establish hsmallL40–49

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply proper factor lt.

  1. L40
    have hsmall : exists pvs_gap_exists_descent. pvs_gap_exists_descent + S (x1) = (n)
  2. L41
    specialize proper_factor_lt (n)
  3. L42
    specialize proper_factor_lt (x1)
  4. L43
    specialize proper_factor_lt (x * x)
  5. L44
    apply proper_factor_lt
  6. L45
    exact hn
  7. L46
    trans (x * x) * x1
  8. L47
    exact hcase_right_witness_right_witness
  9. L48
    apply mul_comm
  10. L49
    intro hone
16Use earlier factsL50–53

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

  1. L50
    specialize prime_square_ne_one (x)
  2. L51
    apply prime_square_ne_one
  3. L52
    exact hcase_right_witness_left
  4. L53
    exact hone
17Establish hrecL54–63

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.

  1. L54
    have hrec : ∃ r. ∃ s. NaturalSquarefreeDecomposition(x1,r,s)Definitions: NaturalSquarefreeDecomposition
  2. L55
    specialize IH (x1)
  3. L56
    apply IH
  4. L57
    exact hu
  5. L58
    specialize lt_of_lt_of_le (x1)
  6. L59
    specialize lt_of_lt_of_le (n)
  7. L60
    specialize lt_of_lt_of_le (B)
  8. L61
    apply lt_of_lt_of_le
  9. L62
    exact hsmall
  10. L63
    specialize le_of_succ_le_succ (n)
18Use earlier factsL64–66

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

  1. L64
    specialize le_of_succ_le_succ (B)
  2. L65
    apply le_of_succ_le_succ
  3. L66
    exact hbound
19Separate the logical casesL67–69

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

  1. L67
    cases hrec
  2. L68
    cases hrec_witness
  3. L69
    cases hrec_witness_witness
20Construct an explicit witnessL70–71

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

  1. L70
    exists x2
  2. L71
    exists x * x3
21Separate the logical casesL72–72

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

  1. L72
    split
22Use earlier factsL73–73

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

  1. L73
    exact hrec_witness_witness_left
23Calculate and transport equalitiesL74–74

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L74
    trans (x * x) * x1
24Use earlier factsL75–75

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

  1. L75
    exact hcase_right_witness_right_witness
25Calculate and transport equalitiesL76–76

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L76
    rewrite hrec_witness_witness_right
26Use earlier factsL77–77

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

  1. L77
    apply squarefree_square_factor_reassociate

Library-wide reading audit

Original exact command ledger · 77 lines
  1. 0001intro B
  2. 0002induction B
  3. 0003intro n
  4. 0004intro hn
  5. 0005intro hbound
  6. 0006exfalso
  7. 0007specialize factor_permutation_below_zero_impossible (n)
  8. 0008apply factor_permutation_below_zero_impossible
  9. 0009exact hbound
  10. 0010intro n
  11. 0011intro hn
  12. 0012intro hbound
  13. 0013have hcase : (((~((n) = 0)) /\ (forall sfd_prime_exists_decision. (~((sfd_prime_exists_decision) = 1) /\ forall pvs_left_exists_decisiondomain pvs_right_exists_decisiondomain. (sfd_prime_exists_decision) = pvs_left_exists_decisiondomain * pvs_right_exists_decisiondomain -> pvs_left_exists_decisiondomain = 1 \/ pvs_right_exists_decisiondomain = 1) -> (exists pvs_le_gap_exists_decisionbound. pvs_le_gap_exists_decisionbound + (sfd_prime_exists_decision) = (n)) -> ~(exists pvs_factor_exists_decisionsquare. (n) = (sfd_prime_exists_decision * sfd_prime_exists_decision) * pvs_factor_exists_decisionsquare)))) \/ exists p. (~((p) = 1) /\ forall pvs_left_exists_prime pvs_right_exists_prime. (p) = pvs_left_exists_prime * pvs_right_exists_prime -> pvs_left_exists_prime = 1 \/ pvs_right_exists_prime = 1) /\ (exists pvs_factor_exists_divisor. (n) = (p * p) * pvs_factor_exists_divisor)
  14. 0014specialize squarefree_or_prime_square_divisor (n)
  15. 0015apply squarefree_or_prime_square_divisor
  16. 0016exact hn
  17. 0017cases hcase
  18. 0018exists n
  19. 0019exists 1
  20. 0020split
  21. 0021exact hcase_left
  22. 0022symm
  23. 0023trans n * 1
  24. 0024congr
  25. 0025refl
  26. 0026apply mul_one
  27. 0027apply mul_one
  28. 0028cases hcase_right
  29. 0029cases hcase_right_witness
  30. 0030cases hcase_right_witness_right
  31. 0031have hu : ~(x1 = 0)
  32. 0032intro hzero
  33. 0033specialize factor_nonzero_right (n)
  34. 0034specialize factor_nonzero_right (x * x)
  35. 0035specialize factor_nonzero_right (x1)
  36. 0036apply factor_nonzero_right
  37. 0037exact hn
  38. 0038exact hcase_right_witness_right_witness
  39. 0039exact hzero
  40. 0040have hsmall : exists pvs_gap_exists_descent. pvs_gap_exists_descent + S (x1) = (n)
  41. 0041specialize proper_factor_lt (n)
  42. 0042specialize proper_factor_lt (x1)
  43. 0043specialize proper_factor_lt (x * x)
  44. 0044apply proper_factor_lt
  45. 0045exact hn
  46. 0046trans (x * x) * x1
  47. 0047exact hcase_right_witness_right_witness
  48. 0048apply mul_comm
  49. 0049intro hone
  50. 0050specialize prime_square_ne_one (x)
  51. 0051apply prime_square_ne_one
  52. 0052exact hcase_right_witness_left
  53. 0053exact hone
  54. 0054have hrec : exists r s. (((((~((r) = 0)) /\ (forall sfd_prime_exists_recursivekernel. (~((sfd_prime_exists_recursivekernel) = 1) /\ forall pvs_left_exists_recursivekerneldomain pvs_right_exists_recursivekerneldomain. (sfd_prime_exists_recursivekernel) = pvs_left_exists_recursivekerneldomain * pvs_right_exists_recursivekerneldomain -> pvs_left_exists_recursivekerneldomain = 1 \/ pvs_right_exists_recursivekerneldomain = 1) -> (exists pvs_le_gap_exists_recursivekernelbound. pvs_le_gap_exists_recursivekernelbound + (sfd_prime_exists_recursivekernel) = (r)) -> ~(exists pvs_factor_exists_recursivekernelsquare. (r) = (sfd_prime_exists_recursivekernel * sfd_prime_exists_recursivekernel) * pvs_factor_exists_recursivekernelsquare)))) /\ ((x1) = (r) * ((s) * (s)))))
  55. 0055specialize IH (x1)
  56. 0056apply IH
  57. 0057exact hu
  58. 0058specialize lt_of_lt_of_le (x1)
  59. 0059specialize lt_of_lt_of_le (n)
  60. 0060specialize lt_of_lt_of_le (B)
  61. 0061apply lt_of_lt_of_le
  62. 0062exact hsmall
  63. 0063specialize le_of_succ_le_succ (n)
  64. 0064specialize le_of_succ_le_succ (B)
  65. 0065apply le_of_succ_le_succ
  66. 0066exact hbound
  67. 0067cases hrec
  68. 0068cases hrec_witness
  69. 0069cases hrec_witness_witness
  70. 0070exists x2
  71. 0071exists x * x3
  72. 0072split
  73. 0073exact hrec_witness_witness_left
  74. 0074trans (x * x) * x1
  75. 0075exact hcase_right_witness_right_witness
  76. 0076rewrite hrec_witness_witness_right
  77. 0077apply squarefree_square_factor_reassociate