PF001F · theorem body

square_divides_square_reduced_root

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

A square divisibility equation between reduced coprime cofactors forces the denominator cofactor to be one.

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.

Statement with defined notation

∀ a. ∀ b. ∀ g. ∀ A. ∀ B. ∀ q. ¬g = 0 → a = g · A → b = g · B → Coprime(A,B) → b · b = a · a · q → Dvd(a,b)

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0003 Dvd PD0005 Coprime

In local proof propositions

PD0005 Coprime
Exact expanded first-order statement
forall a b g A B q. ~(g = 0) -> a = g * A -> b = g * B -> (forall frp_divisor_csf_divisibility_reduced. (exists frp_left_factor_csf_divisibility_reduced. A = frp_divisor_csf_divisibility_reduced * frp_left_factor_csf_divisibility_reduced) -> (exists frp_right_factor_csf_divisibility_reduced. B = frp_divisor_csf_divisibility_reduced * frp_right_factor_csf_divisibility_reduced) -> frp_divisor_csf_divisibility_reduced = 1) -> b * b = (a * a) * q -> exists k. b = a * k

Proof neighborhood

Direct theorem prerequisites

four_square_descent_square_factor_cancel · Alpha closed four_square_product_square · Alpha closed mul_assoc · Stable closed coprime_mul_right · Stable closed mul_one · Stable closed

Direct theorem dependents

PF001G square_divides_square_root

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

57 script commands · 24 reading checkpoints · 3 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.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro g
  4. L4
    intro A
  5. L5
    intro B
  6. L6
    intro q
  7. L7
    intro hg
  8. L8
    intro ha
  9. L9
    intro hb
  10. L10
    intro hcop
02Fix variables and assumptionsL11–11

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

  1. L11
    intro heq
03Establish hreduceL12–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square descent square factor cancel.

  1. L12
    have hreduce : B * B = (A * A) * q
  2. L13
    specialize four_square_descent_square_factor_cancel g
  3. L14
    specialize four_square_descent_square_factor_cancel (B * B)
  4. L15
    specialize four_square_descent_square_factor_cancel ((A * A) * q)
  5. L16
    apply four_square_descent_square_factor_cancel
  6. L17
    exact hg
  7. L18
    trans b * b
  8. L19
    rewrite hb
  9. L20
    rewrite hb
  10. L21
    symm
04Use earlier factsL22–22

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

  1. L22
    apply four_square_product_square
05Calculate and transport equalitiesL23–23

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

  1. L23
    trans (a * a) * q
06Use earlier factsL24–24

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

  1. L24
    exact heq
07Calculate and transport equalitiesL25–28

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

  1. L25
    rewrite ha
  2. L26
    rewrite ha
  3. L27
    trans ((g * g) * (A * A)) * q
  4. L28
    congr
08Use earlier factsL29–29

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

  1. L29
    apply four_square_product_square
09Calculate and transport equalitiesL30–30

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

  1. L30
    refl
10Use earlier factsL31–31

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

  1. L31
    apply mul_assoc
11Establish hcop_squareL32–38

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

  1. L32
    have hcop_square : Coprime(A,B · B)Definitions: Coprime(A,B · B)Original native command in the exact edition
  2. L33
    specialize coprime_mul_right A
  3. L34
    specialize coprime_mul_right B
  4. L35
    specialize coprime_mul_right B
  5. L36
    apply coprime_mul_right
  6. L37
    exact hcop
  7. L38
    exact hcop
12Establish hAoneL39–41

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

  1. L39
    have hAone : A = 1
  2. L40
    specialize hcop_square A
  3. L41
    apply hcop_square
13Construct an explicit witnessL42–42

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

  1. L42
    exists 1
14Calculate and transport equalitiesL43–43

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

  1. L43
    symm
15Use earlier factsL44–44

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

  1. L44
    apply mul_one
16Construct an explicit witnessL45–45

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

  1. L45
    exists (A * q)
17Calculate and transport equalitiesL46–46

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

  1. L46
    trans (A * A) * q
18Use earlier factsL47–48

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

  1. L47
    exact hreduce
  2. L48
    apply mul_assoc
19Construct an explicit witnessL49–49

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

  1. L49
    exists B
20Calculate and transport equalitiesL50–50

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

  1. L50
    trans g * B
21Use earlier factsL51–51

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

  1. L51
    exact hb
22Calculate and transport equalitiesL52–55

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

  1. L52
    rewrite ha
  2. L53
    rewrite hAone
  3. L54
    congr
  4. L55
    symm
23Use earlier factsL56–56

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

  1. L56
    apply mul_one
24Calculate and transport equalitiesL57–57

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

  1. L57
    refl

Library-wide reading audit

Original defined command ledger · 57 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro g
  4. 0004intro A
  5. 0005intro B
  6. 0006intro q
  7. 0007intro hg
  8. 0008intro ha
  9. 0009intro hb
  10. 0010intro hcop
  11. 0011intro heq
  12. 0012have hreduce : B * B = (A * A) * q
  13. 0013specialize four_square_descent_square_factor_cancel g
  14. 0014specialize four_square_descent_square_factor_cancel (B * B)
  15. 0015specialize four_square_descent_square_factor_cancel ((A * A) * q)
  16. 0016apply four_square_descent_square_factor_cancel
  17. 0017exact hg
  18. 0018trans b * b
  19. 0019rewrite hb
  20. 0020rewrite hb
  21. 0021symm
  22. 0022apply four_square_product_square
  23. 0023trans (a * a) * q
  24. 0024exact heq
  25. 0025rewrite ha
  26. 0026rewrite ha
  27. 0027trans ((g * g) * (A * A)) * q
  28. 0028congr
  29. 0029apply four_square_product_square
  30. 0030refl
  31. 0031apply mul_assoc
  32. 0032have hcop_square : Coprime(A,B · B)
    Exact native replay linehave hcop_square : forall d. (exists x. A = d * x) -> (exists y. B * B = d * y) -> d = 1
  33. 0033specialize coprime_mul_right A
  34. 0034specialize coprime_mul_right B
  35. 0035specialize coprime_mul_right B
  36. 0036apply coprime_mul_right
  37. 0037exact hcop
  38. 0038exact hcop
  39. 0039have hAone : A = 1
  40. 0040specialize hcop_square A
  41. 0041apply hcop_square
  42. 0042exists 1
  43. 0043symm
  44. 0044apply mul_one
  45. 0045exists (A * q)
  46. 0046trans (A * A) * q
  47. 0047exact hreduce
  48. 0048apply mul_assoc
  49. 0049exists B
  50. 0050trans g * B
  51. 0051exact hb
  52. 0052rewrite ha
  53. 0053rewrite hAone
  54. 0054congr
  55. 0055symm
  56. 0056apply mul_one
  57. 0057refl