PF000P

pythagorean_square_gap_coprime_first_parameter

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

A square-difference leg is coprime to the first Euclidean parameter whenever the parameters themselves are coprime.

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 m n d. m * m = n * n + d -> (forall pff_divisor_primitive_parameters. (exists pff_left_primitive_parameters. (m) = pff_divisor_primitive_parameters * pff_left_primitive_parameters) -> (exists pff_right_primitive_parameters. (n) = pff_divisor_primitive_parameters * pff_right_primitive_parameters) -> pff_divisor_primitive_parameters = 1) -> (forall pff_divisor_gap_first_result. (exists pff_left_gap_first_result. (d) = pff_divisor_gap_first_result * pff_left_gap_first_result) -> (exists pff_right_gap_first_result. (m) = pff_divisor_gap_first_result * pff_right_gap_first_result) -> pff_divisor_gap_first_result = 1)

Constructive proof overview

Generated structural guide

A square-difference leg is coprime to the first Euclidean parameter whenever the parameters themselves are coprime.

The unchanged tactic script uses 5 declared prerequisites and contains 38 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

PF000O pythagorean_parameter_divisor_divides_square divides_remainder Stable theorem; checked-use authorized mul_one Stable theorem; checked-use authorized add_comm Stable theorem; checked-use authorized coprime_mul_right Stable theorem; checked-use authorized

Direct dependents

PF000R pythagorean_square_gap_coprime_parameter_product

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

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

Named ingredients (1)
pythagorean parameter divisor divides square
01Fix variables and assumptionsL1–8

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

  1. L1
    intro m
  2. L2
    intro n
  3. L3
    intro d
  4. L4
    intro hgap
  5. L5
    intro hcoprime
  6. L6
    intro divisor
  7. L7
    intro hd
  8. L8
    intro hm
02Establish hmsquareL9–13

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

  1. L9
    have hmsquare : exists q. m * m = divisor * q
  2. L10
    specialize pythagorean_parameter_divisor_divides_square divisor
  3. L11
    specialize pythagorean_parameter_divisor_divides_square m
  4. L12
    apply pythagorean_parameter_divisor_divides_square
  5. L13
    exact hm
03Establish hnsquareL14–23

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

  1. L14
    have hnsquare : exists q. n * n = divisor * q
  2. L15
    specialize divides_remainder divisor
  3. L16
    specialize divides_remainder (m * m)
  4. L17
    specialize divides_remainder d
  5. L18
    specialize divides_remainder 1
  6. L19
    specialize divides_remainder (n * n)
  7. L20
    apply divides_remainder
  8. L21
    exact hmsquare
  9. L22
    exact hd
  10. L23
    specialize mul_one d
04Calculate and transport equalitiesL24–25

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

  1. L24
    rewrite mul_one
  2. L25
    trans n * n + d
05Use earlier factsL26–27

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

  1. L26
    exact hgap
  2. L27
    apply add_comm
06Establish hsquarecopL28–37

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

  1. L28
    have hsquarecop : forall pff_divisor_first_square_local. (exists pff_left_first_square_local. (m) = pff_divisor_first_square_local * pff_left_first_square_local) -> (exists pff_right_first_square_local. (n * n) = pff_divisor_first_square_local * pff_right_first_square_local) -> pff_divisor_first_square_local = 1
  2. L29
    specialize coprime_mul_right m
  3. L30
    specialize coprime_mul_right n
  4. L31
    specialize coprime_mul_right n
  5. L32
    apply coprime_mul_right
  6. L33
    exact hcoprime
  7. L34
    exact hcoprime
  8. L35
    specialize hsquarecop divisor
  9. L36
    apply hsquarecop
  10. L37
    exact hm
07Use earlier factsL38–38

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

  1. L38
    exact hnsquare

Library-wide reading audit

Original exact command ledger · 38 lines
  1. 0001intro m
  2. 0002intro n
  3. 0003intro d
  4. 0004intro hgap
  5. 0005intro hcoprime
  6. 0006intro divisor
  7. 0007intro hd
  8. 0008intro hm
  9. 0009have hmsquare : exists q. m * m = divisor * q
  10. 0010specialize pythagorean_parameter_divisor_divides_square divisor
  11. 0011specialize pythagorean_parameter_divisor_divides_square m
  12. 0012apply pythagorean_parameter_divisor_divides_square
  13. 0013exact hm
  14. 0014have hnsquare : exists q. n * n = divisor * q
  15. 0015specialize divides_remainder divisor
  16. 0016specialize divides_remainder (m * m)
  17. 0017specialize divides_remainder d
  18. 0018specialize divides_remainder 1
  19. 0019specialize divides_remainder (n * n)
  20. 0020apply divides_remainder
  21. 0021exact hmsquare
  22. 0022exact hd
  23. 0023specialize mul_one d
  24. 0024rewrite mul_one
  25. 0025trans n * n + d
  26. 0026exact hgap
  27. 0027apply add_comm
  28. 0028have hsquarecop : forall pff_divisor_first_square_local. (exists pff_left_first_square_local. (m) = pff_divisor_first_square_local * pff_left_first_square_local) -> (exists pff_right_first_square_local. (n * n) = pff_divisor_first_square_local * pff_right_first_square_local) -> pff_divisor_first_square_local = 1
  29. 0029specialize coprime_mul_right m
  30. 0030specialize coprime_mul_right n
  31. 0031specialize coprime_mul_right n
  32. 0032apply coprime_mul_right
  33. 0033exact hcoprime
  34. 0034exact hcoprime
  35. 0035specialize hsquarecop divisor
  36. 0036apply hsquarecop
  37. 0037exact hm
  38. 0038exact hnsquare