GI001D

gaussian_signed_square_zero_iff

A genuine natural signed square is zero exactly when the represented integer is 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. SignedDifferenceSquare(p,n,s) → (s = 0 → p = n) ∧ (p = n → s = 0)

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

Definition DAG

SignedDifferenceSquare(p,n,s) · 3

Actual proof prerequisites

matrix_lattice_absolute_difference_exists · checked external prerequisitefour_square_absolute_square_balance · checked external prerequisitegaussian_signed_square_functionalsquare_zero_root · checked external prerequisitezero_add · checked external prerequisite
Original expanded first-order statement 
forall p n s. (((((p) * (p))) + (((n) * (n)))) = ((s) + (((((p) * (n))) + (((n) * (p))))))) -> ((s = 0 -> p = n) /\ (p = n -> s = 0))

Complete tactic proof in conservative notation

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

48 script commands · 19 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 functional
01Fix variables and assumptionsL1–4

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 hsquare
02Separate the logical casesL5–5

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L5
    split
03Fix variables and assumptionsL6–6

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

  1. L6
    intro hzero
04Use earlier factsL7–8

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

  1. L7
    specialize matrix_lattice_absolute_difference_exists p
  2. L8
    specialize matrix_lattice_absolute_difference_exists n
05Separate the logical casesL9–9

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L9
    cases matrix_lattice_absolute_difference_exists
06Establish hmagnitudeL10–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square absolute square balance.

  1. L10
    have hmagnitude : SignedDifferenceSquare(p,n,x · x)Definitions: SignedDifferenceSquare(p,n,x · x)Original native command in the exact edition
  2. L11
    specialize four_square_absolute_square_balance p
  3. L12
    specialize four_square_absolute_square_balance n
  4. L13
    specialize four_square_absolute_square_balance x
  5. L14
    apply four_square_absolute_square_balance
  6. L15
    exact matrix_lattice_absolute_difference_exists_witness
07Establish hsquarezeroL16–24

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

  1. L16
    have hsquarezero : x * x = s
  2. L17
    specialize gaussian_signed_square_functional p
  3. L18
    specialize gaussian_signed_square_functional n
  4. L19
    specialize gaussian_signed_square_functional x * x
  5. L20
    specialize gaussian_signed_square_functional s
  6. L21
    apply gaussian_signed_square_functional
  7. L22
    exact hmagnitude
  8. L23
    exact hsquare
  9. L24
    rewrite hzero at hsquarezero
08Establish hmagnitudezeroL25–28

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

  1. L25
    have hmagnitudezero : x = 0
  2. L26
    specialize square_zero_root x
  3. L27
    apply square_zero_root
  4. L28
    exact hsquarezero
09Separate the logical casesL29–29

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L29
    cases matrix_lattice_absolute_difference_exists_witness
10Calculate and transport equalitiesL30–30

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

  1. L30
    trans n + x
11Use earlier factsL31–31

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

  1. L31
    exact matrix_lattice_absolute_difference_exists_witness_left
12Calculate and transport equalitiesL32–32

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

  1. L32
    rewrite hmagnitudezero
13Use earlier factsL33–33

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

  1. L33
    apply PA3
14Calculate and transport equalitiesL34–35

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

  1. L34
    symm
  2. L35
    trans p + x
15Use earlier factsL36–36

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

  1. L36
    exact matrix_lattice_absolute_difference_exists_witness_right
16Calculate and transport equalitiesL37–37

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

  1. L37
    rewrite hmagnitudezero
17Use earlier factsL38–38

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

  1. L38
    apply PA3
18Fix variables and assumptionsL39–39

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

  1. L39
    intro hequal
19Establish hzeroL40–48

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

  1. L40
    have hzero : SignedDifferenceSquare(p,n,0)Definitions: SignedDifferenceSquare(p,n,0)Original native command in the exact edition
  2. L41
    simp [hequal, zero_add]
  3. L42
    specialize gaussian_signed_square_functional p
  4. L43
    specialize gaussian_signed_square_functional n
  5. L44
    specialize gaussian_signed_square_functional s
  6. L45
    specialize gaussian_signed_square_functional 0
  7. L46
    apply gaussian_signed_square_functional
  8. L47
    exact hsquare
  9. L48
    exact hzero

Library-wide reading audit

Original defined command ledger · 48 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro s
  4. 0004intro hsquare
  5. 0005split
  6. 0006intro hzero
  7. 0007specialize matrix_lattice_absolute_difference_exists p
  8. 0008specialize matrix_lattice_absolute_difference_exists n
  9. 0009cases matrix_lattice_absolute_difference_exists
  10. 0010have hmagnitude : SignedDifferenceSquare(p,n,x · x)
  11. 0011specialize four_square_absolute_square_balance p
  12. 0012specialize four_square_absolute_square_balance n
  13. 0013specialize four_square_absolute_square_balance x
  14. 0014apply four_square_absolute_square_balance
  15. 0015exact matrix_lattice_absolute_difference_exists_witness
  16. 0016have hsquarezero : x * x = s
  17. 0017specialize gaussian_signed_square_functional p
  18. 0018specialize gaussian_signed_square_functional n
  19. 0019specialize gaussian_signed_square_functional x * x
  20. 0020specialize gaussian_signed_square_functional s
  21. 0021apply gaussian_signed_square_functional
  22. 0022exact hmagnitude
  23. 0023exact hsquare
  24. 0024rewrite hzero at hsquarezero
  25. 0025have hmagnitudezero : x = 0
  26. 0026specialize square_zero_root x
  27. 0027apply square_zero_root
  28. 0028exact hsquarezero
  29. 0029cases matrix_lattice_absolute_difference_exists_witness
  30. 0030trans n + x
  31. 0031exact matrix_lattice_absolute_difference_exists_witness_left
  32. 0032rewrite hmagnitudezero
  33. 0033apply PA3
  34. 0034symm
  35. 0035trans p + x
  36. 0036exact matrix_lattice_absolute_difference_exists_witness_right
  37. 0037rewrite hmagnitudezero
  38. 0038apply PA3
  39. 0039intro hequal
  40. 0040have hzero : SignedDifferenceSquare(p,n,0)
  41. 0041simp [hequal, zero_add]
  42. 0042specialize gaussian_signed_square_functional p
  43. 0043specialize gaussian_signed_square_functional n
  44. 0044specialize gaussian_signed_square_functional s
  45. 0045specialize gaussian_signed_square_functional 0
  46. 0046apply gaussian_signed_square_functional
  47. 0047exact hsquare
  48. 0048exact hzero