GI001F

gaussian_signed_square_scaled

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

Alpha v34 checked-use · first admitted v28 · 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.

The natural-code carrier consists of genuine pairs of the existing signed integers; no new primitive arithmetic is trusted. The theorem constructs quotient, remainder, and actual norm witnesses. Gaussian gcd, unique factorization, and prime classification are separate targets.

Exact theorem in conservative defined notation

∀ p. ∀ n. ∀ s. ∀ k. SignedDifferenceSquare(p,n,s) → SignedDifferenceSquare(k · p,k · n,k · k · s)

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

Definition DAG

SignedDifferenceSquare(p,n,s) · 4

Actual proof prerequisites

gaussian_signed_square_productmul_zero_left · checked external prerequisitezero_add · checked external prerequisite
Original expanded first-order 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)))))))

Complete tactic proof in conservative notation

All 30 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

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.

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

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 : SignedDifferenceSquare(k,0,k · k)Definitions: SignedDifferenceSquare(k,0,k · k)Original native command in the exact edition
  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 : SignedDifferenceSquare(k · p + 0 · n,k · n + 0 · p,k · k · s)Definitions: SignedDifferenceSquare(k · p + 0 · n,k · n + 0 · p,k · k · s)Original native command in the exact edition
  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 defined command ledger · 30 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro s
  4. 0004intro k
  5. 0005intro hsquare
  6. 0006have hnatural : SignedDifferenceSquare(k,0,k · k)
  7. 0007simp [mul_zero_left, zero_add]
  8. 0008have hproduct : SignedDifferenceSquare(k · p + 0 · n,k · n + 0 · p,k · k · s)
  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