GI001F

gaussian_signed_square_scaled

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

Scaling a genuine signed pair by any natural multiplies its actual square by the scalar square, including zero.

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 p n s k. (((((p) * (p))) + (((n) * (n)))) = ((s) + (((((p) * (n))) + (((n) * (p))))))) -> (((((k * p) * (k * p))) + (((k * n) * (k * n)))) = (((k * k) * s) + (((((k * p) * (k * n))) + (((k * n) * (k * p)))))))

Constructive proof overview

Generated structural guide

Scaling a genuine signed pair by any natural multiplies its actual square by the scalar square, including zero.

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

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

Proof neighborhood

Direct dependencies

GI000D gaussian_signed_square_product mul_zero_left Stable theorem; checked-use authorized zero_add Stable theorem; checked-use authorized

Direct dependents

none

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

30 script commands · 6 reading checkpoints · 4 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)
gaussian signed square product
01Fix variables and assumptionsL1–5

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro s
  4. L4
    intro k
  5. L5
    intro hsquare
02Establish hnaturalL6–7

Establish this local claim before using it. It is not an additional assumption.

  1. L6
    have hnatural : ((((k) * (k))) + (((0) * (0)))) = ((k * k) + (((((k) * (0))) + (((0) * (k))))))
  2. L7
    simp [mul_zero_left, zero_add]
03Establish hproductL8–17

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

  1. L8
    have hproduct : ((((((((k) * (p))) + (((0) * (n))))) * (((((k) * (p))) + (((0) * (n))))))) + (((((((k) * (n))) + (((0) * (p))))) * (((((k) * (n))) + (((0) * (p)))))))) = (((k * k) * s) + (((((((((k) * (p))) + (((0) * (n))))) * (((((k) * (n))) + (((0) * (p))))))) + (((((((k) * (n))) + (((0) * (p))))) * (((((k) * (p))) + (((0) * (n))))))))))
  2. L9
    specialize gaussian_signed_square_product k
  3. L10
    specialize gaussian_signed_square_product 0
  4. L11
    specialize gaussian_signed_square_product p
  5. L12
    specialize gaussian_signed_square_product n
  6. L13
    specialize gaussian_signed_square_product k * k
  7. L14
    specialize gaussian_signed_square_product s
  8. L15
    apply gaussian_signed_square_product
  9. L16
    exact hnatural
  10. L17
    exact hsquare
04Establish hpositiveL18–19

Establish this local claim before using it. It is not an additional assumption.

  1. L18
    have hpositive : k * p + 0 * n = k * p
  2. L19
    simp [mul_zero_left, zero_add]
05Establish hnegativeL20–29

Establish this local claim before using it. It is not an additional assumption.

  1. L20
    have hnegative : k * n + 0 * p = k * n
  2. L21
    simp [mul_zero_left, zero_add]
  3. L22
    rewrite hpositive at hproduct
  4. L23
    rewrite hpositive at hproduct
  5. L24
    rewrite hpositive at hproduct
  6. L25
    rewrite hpositive at hproduct
  7. L26
    rewrite hnegative at hproduct
  8. L27
    rewrite hnegative at hproduct
  9. L28
    rewrite hnegative at hproduct
  10. L29
    rewrite hnegative at hproduct
06Use earlier factsL30–30

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

  1. L30
    exact hproduct

Library-wide reading audit

Original exact command ledger · 30 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro s
  4. 0004intro k
  5. 0005intro hsquare
  6. 0006have hnatural : ((((k) * (k))) + (((0) * (0)))) = ((k * k) + (((((k) * (0))) + (((0) * (k))))))
  7. 0007simp [mul_zero_left, zero_add]
  8. 0008have hproduct : ((((((((k) * (p))) + (((0) * (n))))) * (((((k) * (p))) + (((0) * (n))))))) + (((((((k) * (n))) + (((0) * (p))))) * (((((k) * (n))) + (((0) * (p)))))))) = (((k * k) * s) + (((((((((k) * (p))) + (((0) * (n))))) * (((((k) * (n))) + (((0) * (p))))))) + (((((((k) * (n))) + (((0) * (p))))) * (((((k) * (p))) + (((0) * (n))))))))))
  9. 0009specialize gaussian_signed_square_product k
  10. 0010specialize gaussian_signed_square_product 0
  11. 0011specialize gaussian_signed_square_product p
  12. 0012specialize gaussian_signed_square_product n
  13. 0013specialize gaussian_signed_square_product k * k
  14. 0014specialize gaussian_signed_square_product s
  15. 0015apply gaussian_signed_square_product
  16. 0016exact hnatural
  17. 0017exact hsquare
  18. 0018have hpositive : k * p + 0 * n = k * p
  19. 0019simp [mul_zero_left, zero_add]
  20. 0020have hnegative : k * n + 0 * p = k * n
  21. 0021simp [mul_zero_left, zero_add]
  22. 0022rewrite hpositive at hproduct
  23. 0023rewrite hpositive at hproduct
  24. 0024rewrite hpositive at hproduct
  25. 0025rewrite hpositive at hproduct
  26. 0026rewrite hnegative at hproduct
  27. 0027rewrite hnegative at hproduct
  28. 0028rewrite hnegative at hproduct
  29. 0029rewrite hnegative at hproduct
  30. 0030exact hproduct