PF001G

square_divides_square_root

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

For all naturals, if a squared divisor divides a squared value, the unsquared divisor divides the unsquared value.

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 a b. (exists q. b * b = (a * a) * q) -> exists k. b = a * k

Constructive proof overview

Generated structural guide

For all naturals, if a squared divisor divides a squared value, the unsquared divisor divides the unsquared value.

The unchanged tactic script uses 9 declared prerequisites and contains 66 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

eq_decidable Stable theorem; checked-use authorized mul_zero_left Stable theorem; checked-use authorized PF001C square_zero_root canonical_gcd_exists Alpha theorem; checked-use authorized is_gcd_dvd_left Stable theorem; checked-use authorized is_gcd_dvd_right Stable theorem; checked-use authorized factor_nonzero_left Stable theorem; checked-use authorized is_gcd_quotients_coprime_nonzero Stable theorem; checked-use authorized PF001F square_divides_square_reduced_root

Direct dependents

PF002F fermat_four_primitive_normalization

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

66 script commands · 17 reading checkpoints · 5 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 (2)
square zero rootsquare divides square reduced root
01Fix variables and assumptionsL1–3

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro hdiv
02Separate the logical casesL4–4

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

  1. L4
    cases hdiv
03Use earlier factsL5–6

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

  1. L5
    specialize eq_decidable a
  2. L6
    specialize eq_decidable 0
04Separate the logical casesL7–7

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

  1. L7
    cases eq_decidable
05Establish hbzeroL8–14

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

  1. L8
    have hbzero : b = 0
  2. L9
    specialize square_zero_root b
  3. L10
    apply square_zero_root
  4. L11
    trans (a * a) * x
  5. L12
    exact hdiv_witness
  6. L13
    rewrite eq_decidable_left
  7. L14
    simp [mul_zero_left]
06Construct an explicit witnessL15–15

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

  1. L15
    exists 0
07Calculate and transport equalitiesL16–17

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

  1. L16
    rewrite hbzero
  2. L17
    simp
08Use earlier factsL18–19

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

  1. L18
    specialize canonical_gcd_exists a
  2. L19
    specialize canonical_gcd_exists b
09Separate the logical casesL20–20

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

  1. L20
    cases canonical_gcd_exists
10Establish haquotL21–26

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

  1. L21
    have haquot : exists A. a = x1 * A
  2. L22
    specialize is_gcd_dvd_left x1
  3. L23
    specialize is_gcd_dvd_left a
  4. L24
    specialize is_gcd_dvd_left b
  5. L25
    apply is_gcd_dvd_left
  6. L26
    exact canonical_gcd_exists_witness
11Separate the logical casesL27–27

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

  1. L27
    cases haquot
12Establish hbquotL28–33

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

  1. L28
    have hbquot : exists B. b = x1 * B
  2. L29
    specialize is_gcd_dvd_right x1
  3. L30
    specialize is_gcd_dvd_right a
  4. L31
    specialize is_gcd_dvd_right b
  5. L32
    apply is_gcd_dvd_right
  6. L33
    exact canonical_gcd_exists_witness
13Separate the logical casesL34–34

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

  1. L34
    cases hbquot
14Establish hgnonzeroL35–43

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

  1. L35
    have hgnonzero : ~(x1 = 0)
  2. L36
    intro hzero
  3. L37
    specialize factor_nonzero_left a
  4. L38
    specialize factor_nonzero_left x1
  5. L39
    specialize factor_nonzero_left x2
  6. L40
    apply factor_nonzero_left
  7. L41
    exact eq_decidable_right
  8. L42
    exact haquot_witness
  9. L43
    exact hzero
15Establish hquotcopL44–53

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

  1. L44
    have hquotcop : forall frp_divisor_csf_divisibility_quotients. (exists frp_left_factor_csf_divisibility_quotients. x2 = frp_divisor_csf_divisibility_quotients * frp_left_factor_csf_divisibility_quotients) -> (exists frp_right_factor_csf_divisibility_quotients. x3 = frp_divisor_csf_divisibility_quotients * frp_right_factor_csf_divisibility_quotients) -> frp_divisor_csf_divisibility_quotients = 1
  2. L45
    specialize is_gcd_quotients_coprime_nonzero x1
  3. L46
    specialize is_gcd_quotients_coprime_nonzero a
  4. L47
    specialize is_gcd_quotients_coprime_nonzero b
  5. L48
    specialize is_gcd_quotients_coprime_nonzero x2
  6. L49
    specialize is_gcd_quotients_coprime_nonzero x3
  7. L50
    apply is_gcd_quotients_coprime_nonzero
  8. L51
    exact canonical_gcd_exists_witness
  9. L52
    exact hgnonzero
  10. L53
    exact haquot_witness
16Use earlier factsL54–63

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

  1. L54
    exact hbquot_witness
  2. L55
    specialize square_divides_square_reduced_root a
  3. L56
    specialize square_divides_square_reduced_root b
  4. L57
    specialize square_divides_square_reduced_root x1
  5. L58
    specialize square_divides_square_reduced_root x2
  6. L59
    specialize square_divides_square_reduced_root x3
  7. L60
    specialize square_divides_square_reduced_root x
  8. L61
    apply square_divides_square_reduced_root
  9. L62
    exact hgnonzero
  10. L63
    exact haquot_witness
17Use earlier factsL64–66

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

  1. L64
    exact hbquot_witness
  2. L65
    exact hquotcop
  3. L66
    exact hdiv_witness

Library-wide reading audit

Original exact command ledger · 66 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro hdiv
  4. 0004cases hdiv
  5. 0005specialize eq_decidable a
  6. 0006specialize eq_decidable 0
  7. 0007cases eq_decidable
  8. 0008have hbzero : b = 0
  9. 0009specialize square_zero_root b
  10. 0010apply square_zero_root
  11. 0011trans (a * a) * x
  12. 0012exact hdiv_witness
  13. 0013rewrite eq_decidable_left
  14. 0014simp [mul_zero_left]
  15. 0015exists 0
  16. 0016rewrite hbzero
  17. 0017simp
  18. 0018specialize canonical_gcd_exists a
  19. 0019specialize canonical_gcd_exists b
  20. 0020cases canonical_gcd_exists
  21. 0021have haquot : exists A. a = x1 * A
  22. 0022specialize is_gcd_dvd_left x1
  23. 0023specialize is_gcd_dvd_left a
  24. 0024specialize is_gcd_dvd_left b
  25. 0025apply is_gcd_dvd_left
  26. 0026exact canonical_gcd_exists_witness
  27. 0027cases haquot
  28. 0028have hbquot : exists B. b = x1 * B
  29. 0029specialize is_gcd_dvd_right x1
  30. 0030specialize is_gcd_dvd_right a
  31. 0031specialize is_gcd_dvd_right b
  32. 0032apply is_gcd_dvd_right
  33. 0033exact canonical_gcd_exists_witness
  34. 0034cases hbquot
  35. 0035have hgnonzero : ~(x1 = 0)
  36. 0036intro hzero
  37. 0037specialize factor_nonzero_left a
  38. 0038specialize factor_nonzero_left x1
  39. 0039specialize factor_nonzero_left x2
  40. 0040apply factor_nonzero_left
  41. 0041exact eq_decidable_right
  42. 0042exact haquot_witness
  43. 0043exact hzero
  44. 0044have hquotcop : forall frp_divisor_csf_divisibility_quotients. (exists frp_left_factor_csf_divisibility_quotients. x2 = frp_divisor_csf_divisibility_quotients * frp_left_factor_csf_divisibility_quotients) -> (exists frp_right_factor_csf_divisibility_quotients. x3 = frp_divisor_csf_divisibility_quotients * frp_right_factor_csf_divisibility_quotients) -> frp_divisor_csf_divisibility_quotients = 1
  45. 0045specialize is_gcd_quotients_coprime_nonzero x1
  46. 0046specialize is_gcd_quotients_coprime_nonzero a
  47. 0047specialize is_gcd_quotients_coprime_nonzero b
  48. 0048specialize is_gcd_quotients_coprime_nonzero x2
  49. 0049specialize is_gcd_quotients_coprime_nonzero x3
  50. 0050apply is_gcd_quotients_coprime_nonzero
  51. 0051exact canonical_gcd_exists_witness
  52. 0052exact hgnonzero
  53. 0053exact haquot_witness
  54. 0054exact hbquot_witness
  55. 0055specialize square_divides_square_reduced_root a
  56. 0056specialize square_divides_square_reduced_root b
  57. 0057specialize square_divides_square_reduced_root x1
  58. 0058specialize square_divides_square_reduced_root x2
  59. 0059specialize square_divides_square_reduced_root x3
  60. 0060specialize square_divides_square_reduced_root x
  61. 0061apply square_divides_square_reduced_root
  62. 0062exact hgnonzero
  63. 0063exact haquot_witness
  64. 0064exact hbquot_witness
  65. 0065exact hquotcop
  66. 0066exact hdiv_witness