SK0009

bounded_prime_square_divisor_search

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

Finite induction decides absence of all squared prime divisors below any bound or constructs an actual bounded prime-square divisor.

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 L n. (forall sfd_search_prime_search_absent. (exists pvs_gap_search_absentbound. pvs_gap_search_absentbound + S (sfd_search_prime_search_absent) = (L)) -> (~((sfd_search_prime_search_absent) = 1) /\ forall pvs_left_search_absentdomain pvs_right_search_absentdomain. (sfd_search_prime_search_absent) = pvs_left_search_absentdomain * pvs_right_search_absentdomain -> pvs_left_search_absentdomain = 1 \/ pvs_right_search_absentdomain = 1) -> ~(exists pvs_factor_search_absentsquare. (n) = (sfd_search_prime_search_absent * sfd_search_prime_search_absent) * pvs_factor_search_absentsquare)) \/ exists p. (((exists pvs_gap_search_presentbound. pvs_gap_search_presentbound + S (p) = (L)) /\ (((~((p) = 1) /\ forall pvs_left_search_presentprime pvs_right_search_presentprime. (p) = pvs_left_search_presentprime * pvs_right_search_presentprime -> pvs_left_search_presentprime = 1 \/ pvs_right_search_presentprime = 1) /\ (exists pvs_factor_search_presentsquare. (n) = (p * p) * pvs_factor_search_presentsquare)))))

Constructive proof overview

Generated structural guide

Finite induction decides absence of all squared prime divisors below any bound or constructs an actual bounded prime-square divisor.

The unchanged tactic script uses 6 declared prerequisites and contains 80 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 prime_decidable Stable theorem; checked-use authorized multiple_decidable Stable theorem; checked-use authorized le_refl Stable theorem; checked-use authorized finite_lt_succ_eq_or_lt Stable theorem; checked-use authorized le_succ Stable theorem; checked-use authorized

Direct dependents

SK000A squarefree_or_prime_square_divisor

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

80 script commands · 35 reading checkpoints · 2 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.

01Fix variables and assumptionsL1–1

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

  1. L1
    intro L
02Induction on LL2–3

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

  1. L2
    induction L
  2. L3
    intro n
03Separate the logical casesL4–4

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

  1. L4
    left
04Fix variables and assumptionsL5–8

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

  1. L5
    intro p
  2. L6
    intro hbound
  3. L7
    intro hp
  4. L8
    intro hdiv
05Use earlier factsL9–11

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

  1. L9
    specialize factor_permutation_below_zero_impossible (p)
  2. L10
    apply factor_permutation_below_zero_impossible
  3. L11
    exact hbound
06Fix variables and assumptionsL12–12

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

  1. L12
    intro n
07Use earlier factsL13–13

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

  1. L13
    specialize IH n
08Separate the logical casesL14–14

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

  1. L14
    cases IH
09Use earlier factsL15–15

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

  1. L15
    specialize prime_decidable L
10Separate the logical casesL16–16

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

  1. L16
    cases prime_decidable
11Use earlier factsL17–18

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

  1. L17
    specialize multiple_decidable (L * L)
  2. L18
    specialize multiple_decidable n
12Separate the logical casesL19–20

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

  1. L19
    cases multiple_decidable
  2. L20
    right
13Construct an explicit witnessL21–21

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

  1. L21
    exists L
14Separate the logical casesL22–22

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

  1. L22
    split
15Use earlier factsL23–24

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

  1. L23
    specialize le_refl (S L)
  2. L24
    apply le_refl
16Separate the logical casesL25–25

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

  1. L25
    split
17Use earlier factsL26–27

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

  1. L26
    exact prime_decidable_left
  2. L27
    exact multiple_decidable_left
18Separate the logical casesL28–28

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

  1. L28
    left
19Fix variables and assumptionsL29–32

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

  1. L29
    intro p
  2. L30
    intro hbound
  3. L31
    intro hp
  4. L32
    intro hdiv
20Establish hcaseL33–37

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L33
    have hcase : p = L \/ (exists pvs_gap_search_case. pvs_gap_search_case + S (p) = (L))
  2. L34
    specialize finite_lt_succ_eq_or_lt (L)
  3. L35
    specialize finite_lt_succ_eq_or_lt (p)
  4. L36
    apply finite_lt_succ_eq_or_lt
  5. L37
    exact hbound
21Separate the logical casesL38–38

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

  1. L38
    cases hcase
22Calculate and transport equalitiesL39–40

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

  1. L39
    rewrite hcase_left at hdiv
  2. L40
    rewrite hcase_left at hdiv
23Use earlier factsL41–47

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

  1. L41
    apply multiple_decidable_right
  2. L42
    exact hdiv
  3. L43
    specialize IH_left (p)
  4. L44
    apply IH_left
  5. L45
    exact hcase_right
  6. L46
    exact hp
  7. L47
    exact hdiv
24Separate the logical casesL48–48

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

  1. L48
    left
25Fix variables and assumptionsL49–52

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

  1. L49
    intro p
  2. L50
    intro hbound
  3. L51
    intro hp
  4. L52
    intro hdiv
26Establish hcaseL53–57

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L53
    have hcase : p = L \/ (exists pvs_gap_search_case. pvs_gap_search_case + S (p) = (L))
  2. L54
    specialize finite_lt_succ_eq_or_lt (L)
  3. L55
    specialize finite_lt_succ_eq_or_lt (p)
  4. L56
    apply finite_lt_succ_eq_or_lt
  5. L57
    exact hbound
27Separate the logical casesL58–58

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

  1. L58
    cases hcase
28Calculate and transport equalitiesL59–60

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

  1. L59
    rewrite hcase_left at hp
  2. L60
    rewrite hcase_left at hp
29Use earlier factsL61–67

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

  1. L61
    apply prime_decidable_right
  2. L62
    exact hp
  3. L63
    specialize IH_left (p)
  4. L64
    apply IH_left
  5. L65
    exact hcase_right
  6. L66
    exact hp
  7. L67
    exact hdiv
30Separate the logical casesL68–71

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

  1. L68
    right
  2. L69
    cases IH_right
  3. L70
    cases IH_right_witness
  4. L71
    cases IH_right_witness_right
31Construct an explicit witnessL72–72

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

  1. L72
    exists x
32Separate the logical casesL73–73

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

  1. L73
    split
33Use earlier factsL74–77

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

  1. L74
    specialize le_succ (S x)
  2. L75
    specialize le_succ (L)
  3. L76
    apply le_succ
  4. L77
    exact IH_right_witness_left
34Separate the logical casesL78–78

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

  1. L78
    split
35Use earlier factsL79–80

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

  1. L79
    exact IH_right_witness_right_left
  2. L80
    exact IH_right_witness_right_right

Library-wide reading audit

Original exact command ledger · 80 lines
  1. 0001intro L
  2. 0002induction L
  3. 0003intro n
  4. 0004left
  5. 0005intro p
  6. 0006intro hbound
  7. 0007intro hp
  8. 0008intro hdiv
  9. 0009specialize factor_permutation_below_zero_impossible (p)
  10. 0010apply factor_permutation_below_zero_impossible
  11. 0011exact hbound
  12. 0012intro n
  13. 0013specialize IH n
  14. 0014cases IH
  15. 0015specialize prime_decidable L
  16. 0016cases prime_decidable
  17. 0017specialize multiple_decidable (L * L)
  18. 0018specialize multiple_decidable n
  19. 0019cases multiple_decidable
  20. 0020right
  21. 0021exists L
  22. 0022split
  23. 0023specialize le_refl (S L)
  24. 0024apply le_refl
  25. 0025split
  26. 0026exact prime_decidable_left
  27. 0027exact multiple_decidable_left
  28. 0028left
  29. 0029intro p
  30. 0030intro hbound
  31. 0031intro hp
  32. 0032intro hdiv
  33. 0033have hcase : p = L \/ (exists pvs_gap_search_case. pvs_gap_search_case + S (p) = (L))
  34. 0034specialize finite_lt_succ_eq_or_lt (L)
  35. 0035specialize finite_lt_succ_eq_or_lt (p)
  36. 0036apply finite_lt_succ_eq_or_lt
  37. 0037exact hbound
  38. 0038cases hcase
  39. 0039rewrite hcase_left at hdiv
  40. 0040rewrite hcase_left at hdiv
  41. 0041apply multiple_decidable_right
  42. 0042exact hdiv
  43. 0043specialize IH_left (p)
  44. 0044apply IH_left
  45. 0045exact hcase_right
  46. 0046exact hp
  47. 0047exact hdiv
  48. 0048left
  49. 0049intro p
  50. 0050intro hbound
  51. 0051intro hp
  52. 0052intro hdiv
  53. 0053have hcase : p = L \/ (exists pvs_gap_search_case. pvs_gap_search_case + S (p) = (L))
  54. 0054specialize finite_lt_succ_eq_or_lt (L)
  55. 0055specialize finite_lt_succ_eq_or_lt (p)
  56. 0056apply finite_lt_succ_eq_or_lt
  57. 0057exact hbound
  58. 0058cases hcase
  59. 0059rewrite hcase_left at hp
  60. 0060rewrite hcase_left at hp
  61. 0061apply prime_decidable_right
  62. 0062exact hp
  63. 0063specialize IH_left (p)
  64. 0064apply IH_left
  65. 0065exact hcase_right
  66. 0066exact hp
  67. 0067exact hdiv
  68. 0068right
  69. 0069cases IH_right
  70. 0070cases IH_right_witness
  71. 0071cases IH_right_witness_right
  72. 0072exists x
  73. 0073split
  74. 0074specialize le_succ (S x)
  75. 0075specialize le_succ (L)
  76. 0076apply le_succ
  77. 0077exact IH_right_witness_left
  78. 0078split
  79. 0079exact IH_right_witness_right_left
  80. 0080exact IH_right_witness_right_right