EL0001

lte_natural_difference_square

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

The square difference has a genuine nonnegative geometric quotient.

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 a b d. a = b + d -> a * a = b * b + d * (a + b)

Constructive proof overview

Generated structural guide

The square difference has a genuine nonnegative geometric quotient.

The unchanged tactic script uses 6 declared prerequisites and contains 50 exact native proof lines.

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

Proof neighborhood

Direct dependencies

add_mul Stable theorem; checked-use authorized mul_add Stable theorem; checked-use authorized mul_assoc Stable theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized add_assoc Stable theorem; checked-use authorized add_comm Stable theorem; checked-use authorized

Direct dependents

EL000A lte_power_difference_second_order_exists

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

50 script commands · 11 reading checkpoints · 0 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.

01Fix variables and assumptionsL1–4

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro d
  4. L4
    intro ha
02Calculate and transport equalitiesL5–14

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

  1. L5
    rewrite ha
  2. L6
    rewrite ha
  3. L7
    rewrite ha
  4. L8
    trans ((((b) * (b))) + ((((b) * (d))) + ((((d) * (b))) + (((d) * (d))))))
  5. L9
    simp [add_mul, mul_add, mul_assoc, add_assoc]
  6. L10
    trans ((((b) * (b))) + ((((b) * (d))) + ((((b) * (d))) + (((d) * (d))))))
  7. L11
    congr
  8. L12
    refl
  9. L13
    congr
  10. L14
    refl
03Calculate and transport equalitiesL15–16

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

  1. L15
    congr
  2. L16
    trans ((b) * (d))
04Use earlier factsL17–17

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

  1. L17
    apply mul_comm
05Calculate and transport equalitiesL18–27

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

  1. L18
    congr
  2. L19
    refl
  3. L20
    refl
  4. L21
    refl
  5. L22
    trans ((((b) * (b))) + ((((b) * (d))) + ((((d) * (d))) + (((b) * (d))))))
  6. L23
    congr
  7. L24
    refl
  8. L25
    congr
  9. L26
    refl
  10. L27
    trans ((((d) * (d))) + (((b) * (d))))
06Use earlier factsL28–28

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

  1. L28
    apply add_comm
07Calculate and transport equalitiesL29–37

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

  1. L29
    congr
  2. L30
    refl
  3. L31
    refl
  4. L32
    trans ((((b) * (b))) + ((((d) * (b))) + ((((d) * (d))) + (((d) * (b))))))
  5. L33
    symm
  6. L34
    congr
  7. L35
    refl
  8. L36
    congr
  9. L37
    trans ((b) * (d))
08Use earlier factsL38–38

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

  1. L38
    apply mul_comm
09Calculate and transport equalitiesL39–44

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

  1. L39
    congr
  2. L40
    refl
  3. L41
    refl
  4. L42
    congr
  5. L43
    refl
  6. L44
    trans ((b) * (d))
10Use earlier factsL45–45

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

  1. L45
    apply mul_comm
11Calculate and transport equalitiesL46–50

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

  1. L46
    congr
  2. L47
    refl
  3. L48
    refl
  4. L49
    symm
  5. L50
    simp [add_mul, mul_add, mul_assoc, add_assoc]

Library-wide reading audit

Original exact command ledger · 50 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro d
  4. 0004intro ha
  5. 0005rewrite ha
  6. 0006rewrite ha
  7. 0007rewrite ha
  8. 0008trans ((((b) * (b))) + ((((b) * (d))) + ((((d) * (b))) + (((d) * (d))))))
  9. 0009simp [add_mul, mul_add, mul_assoc, add_assoc]
  10. 0010trans ((((b) * (b))) + ((((b) * (d))) + ((((b) * (d))) + (((d) * (d))))))
  11. 0011congr
  12. 0012refl
  13. 0013congr
  14. 0014refl
  15. 0015congr
  16. 0016trans ((b) * (d))
  17. 0017apply mul_comm
  18. 0018congr
  19. 0019refl
  20. 0020refl
  21. 0021refl
  22. 0022trans ((((b) * (b))) + ((((b) * (d))) + ((((d) * (d))) + (((b) * (d))))))
  23. 0023congr
  24. 0024refl
  25. 0025congr
  26. 0026refl
  27. 0027trans ((((d) * (d))) + (((b) * (d))))
  28. 0028apply add_comm
  29. 0029congr
  30. 0030refl
  31. 0031refl
  32. 0032trans ((((b) * (b))) + ((((d) * (b))) + ((((d) * (d))) + (((d) * (b))))))
  33. 0033symm
  34. 0034congr
  35. 0035refl
  36. 0036congr
  37. 0037trans ((b) * (d))
  38. 0038apply mul_comm
  39. 0039congr
  40. 0040refl
  41. 0041refl
  42. 0042congr
  43. 0043refl
  44. 0044trans ((b) * (d))
  45. 0045apply mul_comm
  46. 0046congr
  47. 0047refl
  48. 0048refl
  49. 0049symm
  50. 0050simp [add_mul, mul_add, mul_assoc, add_assoc]