PF001M · theorem body

pythagorean_half_product_is_square

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

Cancelling the exact square of two proves that the two half-factors multiply to the even-leg half-square.

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. ∀ c. ∀ h. ∀ t. Pythagorean(a,2 · h,c) → c = a + 2 · t → (a + t) · t = h · h

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

CF0011 Pythagorean

In local proof propositions

none
Exact expanded first-order statement
forall a c h t. a * a + (2 * h) * (2 * h) = c * c -> c = a + 2 * t -> (a + t) * t = h * h

Proof neighborhood

Direct theorem prerequisites

four_square_ordered_square_difference_factor · Alpha closed PF001K pythagorean_half_sum_reassociation four_square_product_shuffle · Alpha closed four_square_product_square · Alpha closed add_left_cancel · Stable closed mul_left_cancel_nonzero · Stable closed mul_ne_zero · Stable closed succ_ne_zero · Stable closed mul_comm · Stable closed

Direct theorem dependents

PF001V pythagorean_odd_even_half_factors

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

51 script commands · 12 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)
pythagorean half sum reassociation
01Fix variables and assumptionsL1–6

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

  1. L1
    intro a
  2. L2
    intro c
  3. L3
    intro h
  4. L4
    intro t
  5. L5
    intro hequation
  6. L6
    intro hgap
02Establish hfactorL7–12

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

  1. L7
    have hfactor : a * a + (2 * t) * (c + a) = c * c
  2. L8
    specialize four_square_ordered_square_difference_factor a
  3. L9
    specialize four_square_ordered_square_difference_factor c
  4. L10
    specialize four_square_ordered_square_difference_factor (2 * t)
  5. L11
    apply four_square_ordered_square_difference_factor
  6. L12
    exact hgap
03Establish hsumL13–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pythagorean half sum reassociation.

  1. L13
    have hsum : c + a = 2 * (a + t)
  2. L14
    rewrite hgap
  3. L15
    apply pythagorean_half_sum_reassociation
  4. L16
    rewrite hsum at hfactor
04Establish hcancelL17–25

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

  1. L17
    have hcancel : (2 * h) * (2 * h) = (2 * t) * (2 * (a + t))
  2. L18
    specialize add_left_cancel (a * a)
  3. L19
    specialize add_left_cancel ((2 * h) * (2 * h))
  4. L20
    specialize add_left_cancel ((2 * t) * (2 * (a + t)))
  5. L21
    apply add_left_cancel
  6. L22
    trans c * c
  7. L23
    exact hequation
  8. L24
    symm
  9. L25
    exact hfactor
05Establish hproductL26–32

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

  1. L26
    have hproduct : (2 * 2) * (h * h) = (2 * 2) * (t * (a + t))
  2. L27
    trans (2 * h) * (2 * h)
  3. L28
    symm
  4. L29
    apply four_square_product_square
  5. L30
    trans (2 * t) * (2 * (a + t))
  6. L31
    exact hcancel
  7. L32
    apply four_square_product_shuffle
06Establish hhalfL33–42

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

  1. L33
    have hhalf : h * h = t * (a + t)
  2. L34
    specialize mul_left_cancel_nonzero (2 * 2)
  3. L35
    specialize mul_left_cancel_nonzero (h * h)
  4. L36
    specialize mul_left_cancel_nonzero (t * (a + t))
  5. L37
    apply mul_left_cancel_nonzero
  6. L38
    intro hzero
  7. L39
    apply mul_ne_zero
  8. L40
    intro htwo
  9. L41
    apply succ_ne_zero
  10. L42
    exact htwo
07Fix variables and assumptionsL43–43

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

  1. L43
    intro htwo
08Use earlier factsL44–47

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

  1. L44
    apply succ_ne_zero
  2. L45
    exact htwo
  3. L46
    exact hzero
  4. L47
    exact hproduct
09Calculate and transport equalitiesL48–48

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

  1. L48
    trans t * (a + t)
10Use earlier factsL49–49

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

  1. L49
    apply mul_comm
11Calculate and transport equalitiesL50–50

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

  1. L50
    symm
12Use earlier factsL51–51

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

  1. L51
    exact hhalf

Library-wide reading audit

Original defined command ledger · 51 lines
  1. 0001intro a
  2. 0002intro c
  3. 0003intro h
  4. 0004intro t
  5. 0005intro hequation
  6. 0006intro hgap
  7. 0007have hfactor : a * a + (2 * t) * (c + a) = c * c
  8. 0008specialize four_square_ordered_square_difference_factor a
  9. 0009specialize four_square_ordered_square_difference_factor c
  10. 0010specialize four_square_ordered_square_difference_factor (2 * t)
  11. 0011apply four_square_ordered_square_difference_factor
  12. 0012exact hgap
  13. 0013have hsum : c + a = 2 * (a + t)
  14. 0014rewrite hgap
  15. 0015apply pythagorean_half_sum_reassociation
  16. 0016rewrite hsum at hfactor
  17. 0017have hcancel : (2 * h) * (2 * h) = (2 * t) * (2 * (a + t))
  18. 0018specialize add_left_cancel (a * a)
  19. 0019specialize add_left_cancel ((2 * h) * (2 * h))
  20. 0020specialize add_left_cancel ((2 * t) * (2 * (a + t)))
  21. 0021apply add_left_cancel
  22. 0022trans c * c
  23. 0023exact hequation
  24. 0024symm
  25. 0025exact hfactor
  26. 0026have hproduct : (2 * 2) * (h * h) = (2 * 2) * (t * (a + t))
  27. 0027trans (2 * h) * (2 * h)
  28. 0028symm
  29. 0029apply four_square_product_square
  30. 0030trans (2 * t) * (2 * (a + t))
  31. 0031exact hcancel
  32. 0032apply four_square_product_shuffle
  33. 0033have hhalf : h * h = t * (a + t)
  34. 0034specialize mul_left_cancel_nonzero (2 * 2)
  35. 0035specialize mul_left_cancel_nonzero (h * h)
  36. 0036specialize mul_left_cancel_nonzero (t * (a + t))
  37. 0037apply mul_left_cancel_nonzero
  38. 0038intro hzero
  39. 0039apply mul_ne_zero
  40. 0040intro htwo
  41. 0041apply succ_ne_zero
  42. 0042exact htwo
  43. 0043intro htwo
  44. 0044apply succ_ne_zero
  45. 0045exact htwo
  46. 0046exact hzero
  47. 0047exact hproduct
  48. 0048trans t * (a + t)
  49. 0049apply mul_comm
  50. 0050symm
  51. 0051exact hhalf