EL0001

lte_natural_difference_square

The square difference has a genuine nonnegative geometric quotient.

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

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.

All displayed hypotheses are required. Powers and positive differences are actual existential outputs. The proof constructs second-order correction identities and iterates the prime step; no binomial expansion or LTE oracle is assumed. The 2-adic variants remain separate open targets.

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ d. a = b + d → a · a = b · b + d · (a + b)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

none

Actual proof prerequisites

add_mul · checked external prerequisitemul_add · checked external prerequisitemul_assoc · checked external prerequisitemul_comm · checked external prerequisiteadd_assoc · checked external prerequisiteadd_comm · checked external prerequisite
Original expanded first-order statement 
forall a b d. a = b + d -> a * a = b * b + d * (a + b)

Complete tactic proof in conservative notation

All 50 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 defined 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]