GI0030

gaussian_conjugate_product_is_norm

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

Multiplication by the genuine complex conjugate produces the actual natural norm with zero imaginary coordinate.

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 a b c d N. (exists ge_real_square_self_norm ge_imaginary_square_self_norm. ((((((a) * (a))) + (((b) * (b)))) = ((ge_real_square_self_norm) + (((((a) * (b))) + (((b) * (a))))))) /\ ((((((c) * (c))) + (((d) * (d)))) = ((ge_imaginary_square_self_norm) + (((((c) * (d))) + (((d) * (c))))))) /\ ((N) = ge_real_square_self_norm + ge_imaginary_square_self_norm)))) -> (((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) + (0)) = ((N) + (((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))))) /\ (((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (0)) = ((0) + (((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a)))))))))))

Constructive proof overview

Generated structural guide

Multiplication by the genuine complex conjugate produces the actual natural norm with zero imaginary coordinate.

The unchanged tactic script uses 6 declared prerequisites and contains 37 exact native proof lines.

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

Proof neighborhood

Direct dependencies

GI002F gaussian_signed_norm_balance mul_comm Stable theorem; checked-use authorized zero_add Stable theorem; checked-use authorized add_assoc Stable theorem; checked-use authorized add_comm Stable theorem; checked-use authorized four_square_add_swap_right_tail Alpha theorem; checked-use authorized

Direct dependents

GI0032 gaussian_adjoint_product_is_norm_scale

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

37 script commands · 20 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 norm balance
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
02Establish hbalanceL7–14

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

  1. L7
    have hbalance : ((((((a) * (a))) + (((b) * (b))))) + (((((c) * (c))) + (((d) * (d)))))) = ((N) + (((((((a) * (b))) + (((b) * (a))))) + (((((c) * (d))) + (((d) * (c))))))))
  2. L8
    specialize gaussian_signed_norm_balance a
  3. L9
    specialize gaussian_signed_norm_balance b
  4. L10
    specialize gaussian_signed_norm_balance c
  5. L11
    specialize gaussian_signed_norm_balance d
  6. L12
    specialize gaussian_signed_norm_balance N
  7. L13
    apply gaussian_signed_norm_balance
  8. L14
    exact hnorm
03Establish hpositiveL15–16

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

  1. L15
    have hpositive : ((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c)))))) = ((((((a) * (a))) + (((b) * (b))))) + (((((c) * (c))) + (((d) * (d))))))
  2. L16
    simp [mul_comm, add_assoc, add_comm, four_square_add_swap_right_tail]
04Establish hnegativeL17–18

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

  1. L17
    have hnegative : ((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d)))))) = ((((((a) * (b))) + (((b) * (a))))) + (((((c) * (d))) + (((d) * (c))))))
  2. L18
    simp [mul_comm, add_assoc, add_comm, four_square_add_swap_right_tail]
05Establish himaginaryL19–20

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

  1. L19
    have himaginary : ((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b)))))) = ((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))
  2. L20
    simp [mul_comm, add_assoc, add_comm, four_square_add_swap_right_tail]
06Separate the logical casesL21–21

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

  1. L21
    split
07Calculate and transport equalitiesL22–22

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

  1. L22
    trans ((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))
08Use earlier factsL23–23

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

  1. L23
    apply PA3
09Calculate and transport equalitiesL24–24

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

  1. L24
    trans ((((((a) * (a))) + (((b) * (b))))) + (((((c) * (c))) + (((d) * (d))))))
10Use earlier factsL25–25

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

  1. L25
    exact hpositive
11Calculate and transport equalitiesL26–26

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

  1. L26
    trans ((N) + (((((((a) * (b))) + (((b) * (a))))) + (((((c) * (d))) + (((d) * (c))))))))
12Use earlier factsL27–27

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

  1. L27
    exact hbalance
13Calculate and transport equalitiesL28–30

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

  1. L28
    congr
  2. L29
    refl
  3. L30
    symm
14Use earlier factsL31–31

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

  1. L31
    exact hnegative
15Calculate and transport equalitiesL32–32

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

  1. L32
    trans ((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))
16Use earlier factsL33–33

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

  1. L33
    apply PA3
17Calculate and transport equalitiesL34–34

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

  1. L34
    trans ((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))
18Use earlier factsL35–35

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

  1. L35
    exact himaginary
19Calculate and transport equalitiesL36–36

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

  1. L36
    symm
20Use earlier factsL37–37

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

  1. L37
    apply zero_add

Library-wide reading audit

Original exact command ledger · 37 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro N
  6. 0006intro hnorm
  7. 0007have hbalance : ((((((a) * (a))) + (((b) * (b))))) + (((((c) * (c))) + (((d) * (d)))))) = ((N) + (((((((a) * (b))) + (((b) * (a))))) + (((((c) * (d))) + (((d) * (c))))))))
  8. 0008specialize gaussian_signed_norm_balance a
  9. 0009specialize gaussian_signed_norm_balance b
  10. 0010specialize gaussian_signed_norm_balance c
  11. 0011specialize gaussian_signed_norm_balance d
  12. 0012specialize gaussian_signed_norm_balance N
  13. 0013apply gaussian_signed_norm_balance
  14. 0014exact hnorm
  15. 0015have hpositive : ((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c)))))) = ((((((a) * (a))) + (((b) * (b))))) + (((((c) * (c))) + (((d) * (d))))))
  16. 0016simp [mul_comm, add_assoc, add_comm, four_square_add_swap_right_tail]
  17. 0017have hnegative : ((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d)))))) = ((((((a) * (b))) + (((b) * (a))))) + (((((c) * (d))) + (((d) * (c))))))
  18. 0018simp [mul_comm, add_assoc, add_comm, four_square_add_swap_right_tail]
  19. 0019have himaginary : ((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b)))))) = ((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))
  20. 0020simp [mul_comm, add_assoc, add_comm, four_square_add_swap_right_tail]
  21. 0021split
  22. 0022trans ((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))
  23. 0023apply PA3
  24. 0024trans ((((((a) * (a))) + (((b) * (b))))) + (((((c) * (c))) + (((d) * (d))))))
  25. 0025exact hpositive
  26. 0026trans ((N) + (((((((a) * (b))) + (((b) * (a))))) + (((((c) * (d))) + (((d) * (c))))))))
  27. 0027exact hbalance
  28. 0028congr
  29. 0029refl
  30. 0030symm
  31. 0031exact hnegative
  32. 0032trans ((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))
  33. 0033apply PA3
  34. 0034trans ((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))
  35. 0035exact himaginary
  36. 0036symm
  37. 0037apply zero_add