PF000Q

pythagorean_square_gap_coprime_second_parameter

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

A square-difference leg is coprime to the second 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_second_result. (exists pff_left_gap_second_result. (d) = pff_divisor_gap_second_result * pff_left_gap_second_result) -> (exists pff_right_gap_second_result. (n) = pff_divisor_gap_second_result * pff_right_gap_second_result) -> pff_divisor_gap_second_result = 1)

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 4 declared prerequisites and contains 37 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 multiple_add Stable theorem; checked-use authorized coprime_symm Stable theorem; checked-use authorized coprime_mul_right Stable theorem; checked-use authorized

Direct dependents

PF000R pythagorean_square_gap_coprime_parameter_product PF002G fermat_four_nested_primitive_triangle

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

37 script commands · 6 reading checkpoints · 4 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 hn
02Establish hnsquareL9–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 hnsquare : exists q. n * n = divisor * q
  2. L10
    specialize pythagorean_parameter_divisor_divides_square divisor
  3. L11
    specialize pythagorean_parameter_divisor_divides_square n
  4. L12
    apply pythagorean_parameter_divisor_divides_square
  5. L13
    exact hn
03Establish hmsquareL14–21

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

  1. L14
    have hmsquare : exists q. m * m = divisor * q
  2. L15
    rewrite hgap
  3. L16
    specialize multiple_add divisor
  4. L17
    specialize multiple_add (n * n)
  5. L18
    specialize multiple_add d
  6. L19
    apply multiple_add
  7. L20
    exact hnsquare
  8. L21
    exact hd
04Establish hreverseL22–26

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

  1. L22
    have hreverse : forall pff_divisor_second_reverse_local. (exists pff_left_second_reverse_local. (n) = pff_divisor_second_reverse_local * pff_left_second_reverse_local) -> (exists pff_right_second_reverse_local. (m) = pff_divisor_second_reverse_local * pff_right_second_reverse_local) -> pff_divisor_second_reverse_local = 1
  2. L23
    specialize coprime_symm m
  3. L24
    specialize coprime_symm n
  4. L25
    apply coprime_symm
  5. L26
    exact hcoprime
05Establish hsquarecopL27–36

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

  1. L27
    have hsquarecop : forall pff_divisor_second_square_local. (exists pff_left_second_square_local. (n) = pff_divisor_second_square_local * pff_left_second_square_local) -> (exists pff_right_second_square_local. (m * m) = pff_divisor_second_square_local * pff_right_second_square_local) -> pff_divisor_second_square_local = 1
  2. L28
    specialize coprime_mul_right n
  3. L29
    specialize coprime_mul_right m
  4. L30
    specialize coprime_mul_right m
  5. L31
    apply coprime_mul_right
  6. L32
    exact hreverse
  7. L33
    exact hreverse
  8. L34
    specialize hsquarecop divisor
  9. L35
    apply hsquarecop
  10. L36
    exact hn
06Use earlier factsL37–37

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

  1. L37
    exact hmsquare

Library-wide reading audit

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