SK000E

squarefree_coprime_square_balance

Equal squarefree-times-square values with coprime square roots force both reduced roots to be one and both squarefree factors to agree.

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

∀ r. ∀ u. ∀ a. ∀ b. Squarefree(r) → Squarefree(u) → (∀ x. Dvd(x,a) → Dvd(x,b) → x = 1) → r · (a · a) = u · (b · b) → u = r ∧ (a = 1 ∧ b = 1)

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

Definition DAG

Squarefree(n) · 2Dvd(d,n) · 2

Actual proof prerequisites

squarefree_coprime_square_factor_is_onecoprime_symm · checked external prerequisitemul_comm · checked external prerequisitemul_one · checked external prerequisite
Original expanded first-order statement 
forall r u a b. (((~((r) = 0)) /\ (forall sfd_prime_balance_left. (~((sfd_prime_balance_left) = 1) /\ forall pvs_left_balance_leftdomain pvs_right_balance_leftdomain. (sfd_prime_balance_left) = pvs_left_balance_leftdomain * pvs_right_balance_leftdomain -> pvs_left_balance_leftdomain = 1 \/ pvs_right_balance_leftdomain = 1) -> (exists pvs_le_gap_balance_leftbound. pvs_le_gap_balance_leftbound + (sfd_prime_balance_left) = (r)) -> ~(exists pvs_factor_balance_leftsquare. (r) = (sfd_prime_balance_left * sfd_prime_balance_left) * pvs_factor_balance_leftsquare)))) -> (((~((u) = 0)) /\ (forall sfd_prime_balance_right. (~((sfd_prime_balance_right) = 1) /\ forall pvs_left_balance_rightdomain pvs_right_balance_rightdomain. (sfd_prime_balance_right) = pvs_left_balance_rightdomain * pvs_right_balance_rightdomain -> pvs_left_balance_rightdomain = 1 \/ pvs_right_balance_rightdomain = 1) -> (exists pvs_le_gap_balance_rightbound. pvs_le_gap_balance_rightbound + (sfd_prime_balance_right) = (u)) -> ~(exists pvs_factor_balance_rightsquare. (u) = (sfd_prime_balance_right * sfd_prime_balance_right) * pvs_factor_balance_rightsquare)))) -> (forall sfd_common_divisor_balance_coprime. (exists pvs_factor_balance_coprimeleft. (a) = (sfd_common_divisor_balance_coprime) * pvs_factor_balance_coprimeleft) -> (exists pvs_factor_balance_coprimeright. (b) = (sfd_common_divisor_balance_coprime) * pvs_factor_balance_coprimeright) -> sfd_common_divisor_balance_coprime = 1) -> r * (a * a) = u * (b * b) -> u = r /\ (a = 1 /\ b = 1)

Complete tactic proof in conservative notation

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

54 script commands · 16 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.

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 (1)
squarefree coprime square factor is one
01Fix variables and assumptionsL1–8

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

  1. L1
    intro r
  2. L2
    intro u
  3. L3
    intro a
  4. L4
    intro b
  5. L5
    intro hr
  6. L6
    intro hu
  7. L7
    intro hcop
  8. L8
    intro heq
02Establish haL9–15

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

  1. L9
    have ha : a = 1
  2. L10
    specialize squarefree_coprime_square_factor_is_one (u)
  3. L11
    specialize squarefree_coprime_square_factor_is_one (a)
  4. L12
    specialize squarefree_coprime_square_factor_is_one (b)
  5. L13
    apply squarefree_coprime_square_factor_is_one
  6. L14
    exact hu
  7. L15
    exact hcop
03Construct an explicit witnessL16–16

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

  1. L16
    exists r
04Calculate and transport equalitiesL17–18

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

  1. L17
    trans r * (a * a)
  2. L18
    symm
05Use earlier factsL19–20

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

  1. L19
    exact heq
  2. L20
    apply mul_comm
06Establish hbL21–30

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

  1. L21
    have hb : b = 1
  2. L22
    specialize squarefree_coprime_square_factor_is_one (r)
  3. L23
    specialize squarefree_coprime_square_factor_is_one (b)
  4. L24
    specialize squarefree_coprime_square_factor_is_one (a)
  5. L25
    apply squarefree_coprime_square_factor_is_one
  6. L26
    exact hr
  7. L27
    specialize coprime_symm (a)
  8. L28
    specialize coprime_symm (b)
  9. L29
    apply coprime_symm
  10. L30
    exact hcop
07Construct an explicit witnessL31–31

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

  1. L31
    exists u
08Calculate and transport equalitiesL32–32

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

  1. L32
    trans u * (b * b)
09Use earlier factsL33–34

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

  1. L33
    exact heq
  2. L34
    apply mul_comm
10Separate the logical casesL35–35

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

  1. L35
    split
11Calculate and transport equalitiesL36–39

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

  1. L36
    rewrite ha at heq
  2. L37
    rewrite ha at heq
  3. L38
    rewrite hb at heq
  4. L39
    rewrite hb at heq
12Establish honeL40–43

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

  1. L40
    have hone : 1 * 1 = 1
  2. L41
    apply mul_one
  3. L42
    rewrite hone at heq
  4. L43
    rewrite hone at heq
13Establish hroneL44–46

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

  1. L44
    have hrone : r * 1 = r
  2. L45
    apply mul_one
  3. L46
    rewrite hrone at heq
14Establish huoneL47–51

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

  1. L47
    have huone : u * 1 = u
  2. L48
    apply mul_one
  3. L49
    rewrite huone at heq
  4. L50
    symm
  5. L51
    exact heq
15Separate the logical casesL52–52

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

  1. L52
    split
16Use earlier factsL53–54

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

  1. L53
    exact ha
  2. L54
    exact hb

Library-wide reading audit

Original defined command ledger · 54 lines
  1. 0001intro r
  2. 0002intro u
  3. 0003intro a
  4. 0004intro b
  5. 0005intro hr
  6. 0006intro hu
  7. 0007intro hcop
  8. 0008intro heq
  9. 0009have ha : a = 1
  10. 0010specialize squarefree_coprime_square_factor_is_one (u)
  11. 0011specialize squarefree_coprime_square_factor_is_one (a)
  12. 0012specialize squarefree_coprime_square_factor_is_one (b)
  13. 0013apply squarefree_coprime_square_factor_is_one
  14. 0014exact hu
  15. 0015exact hcop
  16. 0016exists r
  17. 0017trans r * (a * a)
  18. 0018symm
  19. 0019exact heq
  20. 0020apply mul_comm
  21. 0021have hb : b = 1
  22. 0022specialize squarefree_coprime_square_factor_is_one (r)
  23. 0023specialize squarefree_coprime_square_factor_is_one (b)
  24. 0024specialize squarefree_coprime_square_factor_is_one (a)
  25. 0025apply squarefree_coprime_square_factor_is_one
  26. 0026exact hr
  27. 0027specialize coprime_symm (a)
  28. 0028specialize coprime_symm (b)
  29. 0029apply coprime_symm
  30. 0030exact hcop
  31. 0031exists u
  32. 0032trans u * (b * b)
  33. 0033exact heq
  34. 0034apply mul_comm
  35. 0035split
  36. 0036rewrite ha at heq
  37. 0037rewrite ha at heq
  38. 0038rewrite hb at heq
  39. 0039rewrite hb at heq
  40. 0040have hone : 1 * 1 = 1
  41. 0041apply mul_one
  42. 0042rewrite hone at heq
  43. 0043rewrite hone at heq
  44. 0044have hrone : r * 1 = r
  45. 0045apply mul_one
  46. 0046rewrite hrone at heq
  47. 0047have huone : u * 1 = u
  48. 0048apply mul_one
  49. 0049rewrite huone at heq
  50. 0050symm
  51. 0051exact heq
  52. 0052split
  53. 0053exact ha
  54. 0054exact hb