SK000B

squarefree_decomposition_bounded_exists

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

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

∀ B. ∀ n. ¬n = 0 → Lt(n,B) → ∃ x. ∃ y. NaturalSquarefreeDecomposition(n,x,y)

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

Definition DAG

Squarefree(n) · 1NaturalSquarefreeDecomposition(n,r,s) · 2Lt(a,b) · 2Dvd(d,n) · 1Prime(p) · 1

Actual proof prerequisites

factor_permutation_below_zero_impossible · checked external prerequisitesquarefree_or_prime_square_divisormul_one · checked external prerequisitefactor_nonzero_right · checked external prerequisiteproper_factor_lt · checked external prerequisitemul_comm · checked external prerequisiteprime_square_ne_onelt_of_lt_of_le · checked external prerequisitele_of_succ_le_succ · checked external prerequisitesquarefree_square_factor_reassociate
Original expanded first-order 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)))))

Complete tactic proof in conservative notation

All 77 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

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.

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 (3)
squarefree or prime square divisorprime square ne onesquarefree square factor reassociate
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: Squarefree(n)Prime(x)Dvd(x · x,n)Original native command in the exact edition
  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 : Lt(x1,n)Definitions: Lt(x1,n)Original native command in the exact edition
  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(x1,r,s)Original native command in the exact edition
  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 defined 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 : Squarefree(n) ∨ (∃ x. Prime(x) ∧ Dvd(x · x,n))
  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 : Lt(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 : ∃ r. ∃ s. NaturalSquarefreeDecomposition(x1,r,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