GI0019

gaussian_signed_square_lagrange

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

Lagrange cancellation for two signed squared coordinates, with exact cross-product equations and all four actual scalar squares.

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

Constructive proof overview

Generated structural guide

Lagrange cancellation for two signed squared coordinates, with exact cross-product equations and all four actual scalar squares.

The unchanged tactic script uses 4 declared prerequisites and contains 63 exact native proof lines.

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

Proof neighborhood

Direct dependencies

GI0011 gaussian_signed_square_difference_compensation GI0010 gaussian_signed_square_sum_compensation add_cross_sum_chain Alpha theorem; checked-use authorized add_comm Stable theorem; checked-use authorized

Direct dependents

GI001A gaussian_signed_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

63 script commands · 13 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 (2)
gaussian signed square difference compensationgaussian signed square sum 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 hpositive
  10. L20
    intro hnegative
03Fix variables and assumptionsL21–22

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

  1. L21
    intro hreal
  2. L22
    intro himaginary
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 hreal
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–46

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

  1. L45
    exact hx
  2. L46
    exact himaginary
08Calculate and transport equalitiesL47–50

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

  1. L47
    rewrite <- hpositive at hsum
  2. L48
    rewrite <- hpositive at hsum
  3. L49
    rewrite <- hnegative at hsum
  4. L50
    rewrite <- hnegative at hsum
09Use earlier factsL51–58

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

  1. L51
    specialize add_cross_sum_chain R
  2. L52
    specialize add_cross_sum_chain su + sv
  3. L53
    specialize add_cross_sum_chain ((((((up) * (vp))) + (((un) * (vn))))) + (((((up) * (vp))) + (((un) * (vn))))))
  4. L54
    specialize add_cross_sum_chain ((((((up) * (vn))) + (((un) * (vp))))) + (((((up) * (vn))) + (((un) * (vp))))))
  5. L55
    specialize add_cross_sum_chain I
  6. L56
    specialize add_cross_sum_chain sw + sx
  7. L57
    apply add_cross_sum_chain
  8. L58
    exact hdifference
10Calculate and transport equalitiesL59–59

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

  1. L59
    trans ((I) + (((((((up) * (vn))) + (((un) * (vp))))) + (((((up) * (vn))) + (((un) * (vp))))))))
11Use earlier factsL60–60

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

  1. L60
    apply add_comm
12Calculate and transport equalitiesL61–61

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

  1. L61
    trans ((sw + sx) + (((((((up) * (vp))) + (((un) * (vn))))) + (((((up) * (vp))) + (((un) * (vn))))))))
13Use earlier factsL62–63

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

  1. L62
    exact hsum
  2. L63
    apply add_comm

Library-wide reading audit

Original exact command ledger · 63 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 hpositive
  20. 0020intro hnegative
  21. 0021intro hreal
  22. 0022intro himaginary
  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 hreal
  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 himaginary
  47. 0047rewrite <- hpositive at hsum
  48. 0048rewrite <- hpositive at hsum
  49. 0049rewrite <- hnegative at hsum
  50. 0050rewrite <- hnegative at hsum
  51. 0051specialize add_cross_sum_chain R
  52. 0052specialize add_cross_sum_chain su + sv
  53. 0053specialize add_cross_sum_chain ((((((up) * (vp))) + (((un) * (vn))))) + (((((up) * (vp))) + (((un) * (vn))))))
  54. 0054specialize add_cross_sum_chain ((((((up) * (vn))) + (((un) * (vp))))) + (((((up) * (vn))) + (((un) * (vp))))))
  55. 0055specialize add_cross_sum_chain I
  56. 0056specialize add_cross_sum_chain sw + sx
  57. 0057apply add_cross_sum_chain
  58. 0058exact hdifference
  59. 0059trans ((I) + (((((((up) * (vn))) + (((un) * (vp))))) + (((((up) * (vn))) + (((un) * (vp))))))))
  60. 0060apply add_comm
  61. 0061trans ((sw + sx) + (((((((up) * (vp))) + (((un) * (vn))))) + (((((up) * (vp))) + (((un) * (vn))))))))
  62. 0062exact hsum
  63. 0063apply add_comm