EI0017

eisenstein_weighted_square_lagrange

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

Weighted Lagrange cancellation uses actual scalar squares and exact signed cross-component equations, with no norm oracle.

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 up un vp vn wp wn xp xn su sv sw sx R I. (((((up) * (up))) + (((un) * (un)))) = ((su) + (((((up) * (un))) + (((un) * (up))))))) -> (((((vp) * (vp))) + (((vn) * (vn)))) = ((sv) + (((((vp) * (vn))) + (((vn) * (vp))))))) -> (((((wp) * (wp))) + (((wn) * (wn)))) = ((sw) + (((((wp) * (wn))) + (((wn) * (wp))))))) -> (((((xp) * (xp))) + (((xn) * (xn)))) = ((sx) + (((((xp) * (xn))) + (((xn) * (xp))))))) -> (((((up) * (vp))) + (((un) * (vn)))) = 3 * (((((wp) * (xp))) + (((wn) * (xn)))))) -> (((((up) * (vn))) + (((un) * (vp)))) = 3 * (((((wp) * (xn))) + (((wn) * (xp)))))) -> (((((up + vn) * (up + vn))) + (((un + vp) * (un + vp)))) = ((R) + (((((up + vn) * (un + vp))) + (((un + vp) * (up + vn))))))) -> (((((wp + xp) * (wp + xp))) + (((wn + xn) * (wn + xn)))) = ((I) + (((((wp + xp) * (wn + xn))) + (((wn + xn) * (wp + xp))))))) -> R + 3 * I = (su + sv) + 3 * (sw + sx)

Constructive proof overview

Generated structural guide

Weighted Lagrange cancellation uses actual scalar squares and exact signed cross-component equations, with no norm oracle.

The unchanged tactic script uses 3 declared prerequisites and contains 61 exact native proof lines.

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

Proof neighborhood

Direct dependencies

gaussian_signed_square_difference_compensation Alpha theorem; checked-use authorized gaussian_signed_square_sum_compensation Alpha theorem; checked-use authorized EI0016 eisenstein_weighted_lagrange_compensation

Direct dependents

EI0018 eisenstein_weighted_norm_product

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

61 script commands · 8 reading checkpoints · 2 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)
eisenstein weighted lagrange compensation
01Fix variables and assumptionsL1–10

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

  1. L1
    intro up
  2. L2
    intro un
  3. L3
    intro vp
  4. L4
    intro vn
  5. L5
    intro wp
  6. L6
    intro wn
  7. L7
    intro xp
  8. L8
    intro xn
  9. L9
    intro su
  10. L10
    intro sv
02Fix variables and assumptionsL11–20

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

  1. L11
    intro sw
  2. L12
    intro sx
  3. L13
    intro R
  4. L14
    intro I
  5. L15
    intro hu
  6. L16
    intro hv
  7. L17
    intro hw
  8. L18
    intro hx
  9. L19
    intro hp
  10. L20
    intro hq
03Fix variables and assumptionsL21–22

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

  1. L21
    intro hr
  2. L22
    intro hi
04Establish hdifferenceL23–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian signed square difference compensation.

  1. L23
    have hdifference : R + (((((((up) * (vp))) + (((un) * (vn))))) + (((((up) * (vp))) + (((un) * (vn))))))) = (su + sv) + (((((((up) * (vn))) + (((un) * (vp))))) + (((((up) * (vn))) + (((un) * (vp)))))))
  2. L24
    specialize gaussian_signed_square_difference_compensation up
  3. L25
    specialize gaussian_signed_square_difference_compensation un
  4. L26
    specialize gaussian_signed_square_difference_compensation vp
  5. L27
    specialize gaussian_signed_square_difference_compensation vn
  6. L28
    specialize gaussian_signed_square_difference_compensation su
  7. L29
    specialize gaussian_signed_square_difference_compensation sv
  8. L30
    specialize gaussian_signed_square_difference_compensation R
  9. L31
    apply gaussian_signed_square_difference_compensation
  10. L32
    exact hu
05Use earlier factsL33–34

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

  1. L33
    exact hv
  2. L34
    exact hr
06Establish hsumL35–44

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian signed square sum compensation.

  1. L35
    have hsum : I + (((((((wp) * (xn))) + (((wn) * (xp))))) + (((((wp) * (xn))) + (((wn) * (xp))))))) = (sw + sx) + (((((((wp) * (xp))) + (((wn) * (xn))))) + (((((wp) * (xp))) + (((wn) * (xn)))))))
  2. L36
    specialize gaussian_signed_square_sum_compensation wp
  3. L37
    specialize gaussian_signed_square_sum_compensation wn
  4. L38
    specialize gaussian_signed_square_sum_compensation xp
  5. L39
    specialize gaussian_signed_square_sum_compensation xn
  6. L40
    specialize gaussian_signed_square_sum_compensation sw
  7. L41
    specialize gaussian_signed_square_sum_compensation sx
  8. L42
    specialize gaussian_signed_square_sum_compensation I
  9. L43
    apply gaussian_signed_square_sum_compensation
  10. L44
    exact hw
07Use earlier factsL45–54

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

  1. L45
    exact hx
  2. L46
    exact hi
  3. L47
    specialize eisenstein_weighted_lagrange_compensation su
  4. L48
    specialize eisenstein_weighted_lagrange_compensation sv
  5. L49
    specialize eisenstein_weighted_lagrange_compensation sw
  6. L50
    specialize eisenstein_weighted_lagrange_compensation sx
  7. L51
    specialize eisenstein_weighted_lagrange_compensation R
  8. L52
    specialize eisenstein_weighted_lagrange_compensation I
  9. L53
    specialize eisenstein_weighted_lagrange_compensation ((((up) * (vp))) + (((un) * (vn))))
  10. L54
    specialize eisenstein_weighted_lagrange_compensation ((((up) * (vn))) + (((un) * (vp))))
08Use earlier factsL55–61

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

  1. L55
    specialize eisenstein_weighted_lagrange_compensation ((((wp) * (xp))) + (((wn) * (xn))))
  2. L56
    specialize eisenstein_weighted_lagrange_compensation ((((wp) * (xn))) + (((wn) * (xp))))
  3. L57
    apply eisenstein_weighted_lagrange_compensation
  4. L58
    exact hp
  5. L59
    exact hq
  6. L60
    exact hdifference
  7. L61
    exact hsum

Library-wide reading audit

Original exact command ledger · 61 lines
  1. 0001intro up
  2. 0002intro un
  3. 0003intro vp
  4. 0004intro vn
  5. 0005intro wp
  6. 0006intro wn
  7. 0007intro xp
  8. 0008intro xn
  9. 0009intro su
  10. 0010intro sv
  11. 0011intro sw
  12. 0012intro sx
  13. 0013intro R
  14. 0014intro I
  15. 0015intro hu
  16. 0016intro hv
  17. 0017intro hw
  18. 0018intro hx
  19. 0019intro hp
  20. 0020intro hq
  21. 0021intro hr
  22. 0022intro hi
  23. 0023have hdifference : R + (((((((up) * (vp))) + (((un) * (vn))))) + (((((up) * (vp))) + (((un) * (vn))))))) = (su + sv) + (((((((up) * (vn))) + (((un) * (vp))))) + (((((up) * (vn))) + (((un) * (vp)))))))
  24. 0024specialize gaussian_signed_square_difference_compensation up
  25. 0025specialize gaussian_signed_square_difference_compensation un
  26. 0026specialize gaussian_signed_square_difference_compensation vp
  27. 0027specialize gaussian_signed_square_difference_compensation vn
  28. 0028specialize gaussian_signed_square_difference_compensation su
  29. 0029specialize gaussian_signed_square_difference_compensation sv
  30. 0030specialize gaussian_signed_square_difference_compensation R
  31. 0031apply gaussian_signed_square_difference_compensation
  32. 0032exact hu
  33. 0033exact hv
  34. 0034exact hr
  35. 0035have hsum : I + (((((((wp) * (xn))) + (((wn) * (xp))))) + (((((wp) * (xn))) + (((wn) * (xp))))))) = (sw + sx) + (((((((wp) * (xp))) + (((wn) * (xn))))) + (((((wp) * (xp))) + (((wn) * (xn)))))))
  36. 0036specialize gaussian_signed_square_sum_compensation wp
  37. 0037specialize gaussian_signed_square_sum_compensation wn
  38. 0038specialize gaussian_signed_square_sum_compensation xp
  39. 0039specialize gaussian_signed_square_sum_compensation xn
  40. 0040specialize gaussian_signed_square_sum_compensation sw
  41. 0041specialize gaussian_signed_square_sum_compensation sx
  42. 0042specialize gaussian_signed_square_sum_compensation I
  43. 0043apply gaussian_signed_square_sum_compensation
  44. 0044exact hw
  45. 0045exact hx
  46. 0046exact hi
  47. 0047specialize eisenstein_weighted_lagrange_compensation su
  48. 0048specialize eisenstein_weighted_lagrange_compensation sv
  49. 0049specialize eisenstein_weighted_lagrange_compensation sw
  50. 0050specialize eisenstein_weighted_lagrange_compensation sx
  51. 0051specialize eisenstein_weighted_lagrange_compensation R
  52. 0052specialize eisenstein_weighted_lagrange_compensation I
  53. 0053specialize eisenstein_weighted_lagrange_compensation ((((up) * (vp))) + (((un) * (vn))))
  54. 0054specialize eisenstein_weighted_lagrange_compensation ((((up) * (vn))) + (((un) * (vp))))
  55. 0055specialize eisenstein_weighted_lagrange_compensation ((((wp) * (xp))) + (((wn) * (xn))))
  56. 0056specialize eisenstein_weighted_lagrange_compensation ((((wp) * (xn))) + (((wn) * (xp))))
  57. 0057apply eisenstein_weighted_lagrange_compensation
  58. 0058exact hp
  59. 0059exact hq
  60. 0060exact hdifference
  61. 0061exact hsum