PF002E

fermat_four_odd_double_square_factors

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

A square twice a coprime product with odd first factor supplies an actual square first factor and twice-square second factor.

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 y. (forall pff_divisor_ffd_double_source. (exists pff_left_ffd_double_source. (m) = pff_divisor_ffd_double_source * pff_left_ffd_double_source) -> (exists pff_right_ffd_double_source. (n) = pff_divisor_ffd_double_source * pff_right_ffd_double_source) -> pff_divisor_ffd_double_source = 1) -> (exists k. m = 2 * k + 1) -> y * y = 2 * (m * n) -> exists u v. (m = u * u /\ n = 2 * (v * v))

Constructive proof overview

Generated structural guide

A square twice a coprime product with odd first factor supplies an actual square first factor and twice-square second factor.

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

PF000N pythagorean_odd_coordinate_coprime_two coprime_mul_right Stable theorem; checked-use authorized PF001E coprime_square_product_factors PF002D fermat_four_double_product_commute PF002C fermat_four_even_square_root mul_left_cancel_nonzero Stable theorem; checked-use authorized four_square_product_square Alpha theorem; checked-use authorized mul_assoc Stable theorem; checked-use authorized succ_ne_zero Stable theorem; checked-use authorized

Direct dependents

PF002K fermat_four_primitive_odd_even_descent

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

54 script commands · 19 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 (4)
pythagorean odd coordinate coprime twocoprime square product factorsfermat four double product commutefermat four even square root
01Fix variables and assumptionsL1–6

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

  1. L1
    intro m
  2. L2
    intro n
  3. L3
    intro y
  4. L4
    intro hcoprime
  5. L5
    intro hm
  6. L6
    intro hequation
02Establish hm2L7–9

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

  1. L7
    have hm2 : forall pff_divisor_ffd_double_two. (exists pff_left_ffd_double_two. (m) = pff_divisor_ffd_double_two * pff_left_ffd_double_two) -> (exists pff_right_ffd_double_two. (2) = pff_divisor_ffd_double_two * pff_right_ffd_double_two) -> pff_divisor_ffd_double_two = 1
  2. L8
    apply pythagorean_odd_coordinate_coprime_two
  3. L9
    exact hm
03Establish hm2nL10–16

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

  1. L10
    have hm2n : forall pff_divisor_ffd_double_product. (exists pff_left_ffd_double_product. (m) = pff_divisor_ffd_double_product * pff_left_ffd_double_product) -> (exists pff_right_ffd_double_product. (2 * n) = pff_divisor_ffd_double_product * pff_right_ffd_double_product) -> pff_divisor_ffd_double_product = 1
  2. L11
    specialize coprime_mul_right (m)
  3. L12
    specialize coprime_mul_right (2)
  4. L13
    specialize coprime_mul_right (n)
  5. L14
    apply coprime_mul_right
  6. L15
    exact hm2
  7. L16
    exact hcoprime
04Establish hpartsL17–26

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

  1. L17
    have hparts : exists u v. (m = u * u /\ 2 * n = v * v)
  2. L18
    specialize coprime_square_product_factors (m)
  3. L19
    specialize coprime_square_product_factors (2 * n)
  4. L20
    specialize coprime_square_product_factors (y)
  5. L21
    apply coprime_square_product_factors
  6. L22
    exact hm2n
  7. L23
    trans 2 * (m * n)
  8. L24
    apply fermat_four_double_product_commute
  9. L25
    symm
  10. L26
    exact hequation
05Separate the logical casesL27–29

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

  1. L27
    cases hparts
  2. L28
    cases hparts_witness
  3. L29
    cases hparts_witness_witness
06Establish hhalfL30–31

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

  1. L30
    have hhalf : exists k. x1 = 2 * k
  2. L31
    apply fermat_four_even_square_root
07Construct an explicit witnessL32–32

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

  1. L32
    exists n
08Calculate and transport equalitiesL33–33

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

  1. L33
    symm
09Use earlier factsL34–34

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

  1. L34
    exact hparts_witness_witness_right
10Separate the logical casesL35–35

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

  1. L35
    cases hhalf
11Construct an explicit witnessL36–37

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

  1. L36
    exists x
  2. L37
    exists x2
12Separate the logical casesL38–38

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

  1. L38
    split
13Use earlier factsL39–43

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

  1. L39
    exact hparts_witness_witness_left
  2. L40
    specialize mul_left_cancel_nonzero (2)
  3. L41
    specialize mul_left_cancel_nonzero (n)
  4. L42
    specialize mul_left_cancel_nonzero (2 * (x2 * x2))
  5. L43
    apply mul_left_cancel_nonzero
14Fix variables and assumptionsL44–44

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

  1. L44
    intro hzero
15Use earlier factsL45–47

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

  1. L45
    specialize succ_ne_zero 1
  2. L46
    apply succ_ne_zero
  3. L47
    exact hzero
16Calculate and transport equalitiesL48–48

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

  1. L48
    trans x1 * x1
17Use earlier factsL49–49

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

  1. L49
    exact hparts_witness_witness_right
18Calculate and transport equalitiesL50–52

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

  1. L50
    rewrite hhalf_witness
  2. L51
    rewrite hhalf_witness
  3. L52
    trans (2 * 2) * (x2 * x2)
19Use earlier factsL53–54

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

  1. L53
    apply four_square_product_square
  2. L54
    apply mul_assoc

Library-wide reading audit

Original exact command ledger · 54 lines
  1. 0001intro m
  2. 0002intro n
  3. 0003intro y
  4. 0004intro hcoprime
  5. 0005intro hm
  6. 0006intro hequation
  7. 0007have hm2 : forall pff_divisor_ffd_double_two. (exists pff_left_ffd_double_two. (m) = pff_divisor_ffd_double_two * pff_left_ffd_double_two) -> (exists pff_right_ffd_double_two. (2) = pff_divisor_ffd_double_two * pff_right_ffd_double_two) -> pff_divisor_ffd_double_two = 1
  8. 0008apply pythagorean_odd_coordinate_coprime_two
  9. 0009exact hm
  10. 0010have hm2n : forall pff_divisor_ffd_double_product. (exists pff_left_ffd_double_product. (m) = pff_divisor_ffd_double_product * pff_left_ffd_double_product) -> (exists pff_right_ffd_double_product. (2 * n) = pff_divisor_ffd_double_product * pff_right_ffd_double_product) -> pff_divisor_ffd_double_product = 1
  11. 0011specialize coprime_mul_right (m)
  12. 0012specialize coprime_mul_right (2)
  13. 0013specialize coprime_mul_right (n)
  14. 0014apply coprime_mul_right
  15. 0015exact hm2
  16. 0016exact hcoprime
  17. 0017have hparts : exists u v. (m = u * u /\ 2 * n = v * v)
  18. 0018specialize coprime_square_product_factors (m)
  19. 0019specialize coprime_square_product_factors (2 * n)
  20. 0020specialize coprime_square_product_factors (y)
  21. 0021apply coprime_square_product_factors
  22. 0022exact hm2n
  23. 0023trans 2 * (m * n)
  24. 0024apply fermat_four_double_product_commute
  25. 0025symm
  26. 0026exact hequation
  27. 0027cases hparts
  28. 0028cases hparts_witness
  29. 0029cases hparts_witness_witness
  30. 0030have hhalf : exists k. x1 = 2 * k
  31. 0031apply fermat_four_even_square_root
  32. 0032exists n
  33. 0033symm
  34. 0034exact hparts_witness_witness_right
  35. 0035cases hhalf
  36. 0036exists x
  37. 0037exists x2
  38. 0038split
  39. 0039exact hparts_witness_witness_left
  40. 0040specialize mul_left_cancel_nonzero (2)
  41. 0041specialize mul_left_cancel_nonzero (n)
  42. 0042specialize mul_left_cancel_nonzero (2 * (x2 * x2))
  43. 0043apply mul_left_cancel_nonzero
  44. 0044intro hzero
  45. 0045specialize succ_ne_zero 1
  46. 0046apply succ_ne_zero
  47. 0047exact hzero
  48. 0048trans x1 * x1
  49. 0049exact hparts_witness_witness_right
  50. 0050rewrite hhalf_witness
  51. 0051rewrite hhalf_witness
  52. 0052trans (2 * 2) * (x2 * x2)
  53. 0053apply four_square_product_square
  54. 0054apply mul_assoc