GI002F

gaussian_signed_norm_balance

An actual Gaussian norm is exactly the difference of its positive-square and negative-cross blocks.

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

∀ a. ∀ b. ∀ c. ∀ d. ∀ N. GaussianSignedNorm(a,b,c,d,N) → a · a + b · b + (c · c + d · d) = N + (a · b + b · a + (c · d + d · c))

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

Definition DAG

GaussianSignedNorm(ap,an,bp,bn,N) · 1

Actual proof prerequisites

add_assoc · checked external prerequisiteadd_comm · checked external prerequisitefour_square_add_swap_right_tail · checked external prerequisite
Original expanded first-order statement 
forall a b c d N. (exists ge_real_square_norm_balance ge_imaginary_square_norm_balance. ((((((a) * (a))) + (((b) * (b)))) = ((ge_real_square_norm_balance) + (((((a) * (b))) + (((b) * (a))))))) /\ ((((((c) * (c))) + (((d) * (d)))) = ((ge_imaginary_square_norm_balance) + (((((c) * (d))) + (((d) * (c))))))) /\ ((N) = ge_real_square_norm_balance + ge_imaginary_square_norm_balance)))) -> ((((((a) * (a))) + (((b) * (b))))) + (((((c) * (c))) + (((d) * (d)))))) = ((N) + (((((((a) * (b))) + (((b) * (a))))) + (((((c) * (d))) + (((d) * (c))))))))

Complete tactic proof in conservative notation

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

14 script commands · 3 reading checkpoints · 0 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.

01Fix variables and assumptionsL1–6

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro d
  5. L5
    intro N
  6. L6
    intro hnorm
02Separate the logical casesL7–10

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

  1. L7
    cases hnorm
  2. L8
    cases hnorm_witness
  3. L9
    cases hnorm_witness_witness
  4. L10
    cases hnorm_witness_witness_right
03Calculate and transport equalitiesL11–14

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

  1. L11
    rewrite hnorm_witness_witness_left
  2. L12
    rewrite hnorm_witness_witness_right_left
  3. L13
    rewrite hnorm_witness_witness_right_right
  4. L14
    simp [add_assoc, add_comm, four_square_add_swap_right_tail]

Library-wide reading audit

Original defined command ledger · 14 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro N
  6. 0006intro hnorm
  7. 0007cases hnorm
  8. 0008cases hnorm_witness
  9. 0009cases hnorm_witness_witness
  10. 0010cases hnorm_witness_witness_right
  11. 0011rewrite hnorm_witness_witness_left
  12. 0012rewrite hnorm_witness_witness_right_left
  13. 0013rewrite hnorm_witness_witness_right_right
  14. 0014simp [add_assoc, add_comm, four_square_add_swap_right_tail]