GI001A

gaussian_signed_norm_product

The actual squared Gaussian norm is multiplicative for arbitrary signed representatives, by checked two-coordinate Lagrange cancellation.

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. ∀ e. ∀ f. ∀ g. ∀ h. ∀ N. ∀ M. GaussianSignedNorm(a,b,c,d,N) → GaussianSignedNorm(e,f,g,h,M) → GaussianSignedNorm(a · e + b · f + (c · h + d · g),a · f + b · e + (c · g + d · h),a · g + b · h + (c · e + d · f),a · h + b · g + (c · f + d · e),N · M)

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

Definition DAG

SignedDifferenceSquare(p,n,s) · 2GaussianSignedNorm(ap,an,bp,bn,N) · 3

Actual proof prerequisites

gaussian_signed_square_existsgaussian_signed_product_cross_interchangegaussian_signed_square_lagrangegaussian_signed_square_productadd_mul · checked external prerequisitemul_add · checked external prerequisiteadd_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 e f g h N M. (exists ge_real_square_factor_left ge_imaginary_square_factor_left. ((((((a) * (a))) + (((b) * (b)))) = ((ge_real_square_factor_left) + (((((a) * (b))) + (((b) * (a))))))) /\ ((((((c) * (c))) + (((d) * (d)))) = ((ge_imaginary_square_factor_left) + (((((c) * (d))) + (((d) * (c))))))) /\ ((N) = ge_real_square_factor_left + ge_imaginary_square_factor_left)))) -> (exists ge_real_square_factor_right ge_imaginary_square_factor_right. ((((((e) * (e))) + (((f) * (f)))) = ((ge_real_square_factor_right) + (((((e) * (f))) + (((f) * (e))))))) /\ ((((((g) * (g))) + (((h) * (h)))) = ((ge_imaginary_square_factor_right) + (((((g) * (h))) + (((h) * (g))))))) /\ ((M) = ge_real_square_factor_right + ge_imaginary_square_factor_right)))) -> (exists ge_real_square_product_norm ge_imaginary_square_product_norm. ((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h)))))))))) = ((ge_real_square_product_norm) + (((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) /\ ((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e)))))))))) = ((ge_imaginary_square_product_norm) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))))))) /\ ((N * M) = ge_real_square_product_norm + ge_imaginary_square_product_norm))))

Complete tactic proof in conservative notation

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

109 script commands · 22 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 (4)
gaussian signed square existsgaussian signed product cross interchangegaussian signed square lagrangegaussian signed square product
01Fix variables and assumptionsL1–10

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 e
  6. L6
    intro f
  7. L7
    intro g
  8. L8
    intro h
  9. L9
    intro N
  10. L10
    intro M
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hfirst
  2. L12
    intro hsecond
03Separate the logical casesL13–20

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

  1. L13
    cases hfirst
  2. L14
    cases hfirst_witness
  3. L15
    cases hfirst_witness_witness
  4. L16
    cases hfirst_witness_witness_right
  5. L17
    cases hsecond
  6. L18
    cases hsecond_witness
  7. L19
    cases hsecond_witness_witness
  8. L20
    cases hsecond_witness_witness_right
04Establish hrealL21–24

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

  1. L21
    have hreal : ∃ s. SignedDifferenceSquare(a · e + b · f + (c · h + d · g),a · f + b · e + (c · g + d · h),s)Definitions: SignedDifferenceSquare(a · e + b · f + (c · h + d · g),a · f + b · e + (c · g + d · h),s)Original native command in the exact edition
  2. L22
    specialize gaussian_signed_square_exists ((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))
  3. L23
    specialize gaussian_signed_square_exists ((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))
  4. L24
    apply gaussian_signed_square_exists
05Separate the logical casesL25–25

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

  1. L25
    cases hreal
06Establish himaginaryL26–29

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

  1. L26
    have himaginary : ∃ t. SignedDifferenceSquare(a · g + b · h + (c · e + d · f),a · h + b · g + (c · f + d · e),t)Definitions: SignedDifferenceSquare(a · g + b · h + (c · e + d · f),a · h + b · g + (c · f + d · e),t)Original native command in the exact edition
  2. L27
    specialize gaussian_signed_square_exists ((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))
  3. L28
    specialize gaussian_signed_square_exists ((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))
  4. L29
    apply gaussian_signed_square_exists
07Separate the logical casesL30–30

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

  1. L30
    cases himaginary
08Establish hcrossL31–40

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

  1. L31
    have hcross · expand full local formula (642 characters)have hcross : (((((((((((a) * (e))) + (((b) * (f))))) * (((((c) * (g))) + (((d) * (h))))))) + (((((((a) * (f))) + (((b) * (e))))) * (((((c) * (h))) + (((d) * (g))))))))) = (((((((((a) * (g))) + (((b) * (h))))) * (((((c) * (e))) + (((d) * (f))))))) + (((((((a) * (h))) + (((b) * (g))))) * (((((c) * (f))) + (((d) * (e)))))))))) /\ ((((((((((a) * (e))) + (((b) * (f))))) * (((((c) * (h))) + (((d) * (g))))))) + (((((((a) * (f))) + (((b) * (e))))) * (((((c) * (g))) + (((d) * (h))))))))) = (((((((((a) * (g))) + (((b) * (h))))) * (((((c) * (f))) + (((d) * (e))))))) + (((((((a) * (h))) + (((b) * (g))))) * (((((c) * (e))) + (((d) * (f)))))))))))
  2. L32
    specialize gaussian_signed_product_cross_interchange a
  3. L33
    specialize gaussian_signed_product_cross_interchange b
  4. L34
    specialize gaussian_signed_product_cross_interchange c
  5. L35
    specialize gaussian_signed_product_cross_interchange d
  6. L36
    specialize gaussian_signed_product_cross_interchange e
  7. L37
    specialize gaussian_signed_product_cross_interchange f
  8. L38
    specialize gaussian_signed_product_cross_interchange g
  9. L39
    specialize gaussian_signed_product_cross_interchange h
  10. L40
    apply gaussian_signed_product_cross_interchange
09Separate the logical casesL41–41

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

  1. L41
    cases hcross
10Establish hnormL42–51

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

  1. L42
    have hnorm : x4 + x5 = ((((x * x2) + (x1 * x3))) + (((x * x3) + (x1 * x2))))
  2. L43
    specialize gaussian_signed_square_lagrange ((((a) * (e))) + (((b) * (f))))
  3. L44
    specialize gaussian_signed_square_lagrange ((((a) * (f))) + (((b) * (e))))
  4. L45
    specialize gaussian_signed_square_lagrange ((((c) * (g))) + (((d) * (h))))
  5. L46
    specialize gaussian_signed_square_lagrange ((((c) * (h))) + (((d) * (g))))
  6. L47
    specialize gaussian_signed_square_lagrange ((((a) * (g))) + (((b) * (h))))
  7. L48
    specialize gaussian_signed_square_lagrange ((((a) * (h))) + (((b) * (g))))
  8. L49
    specialize gaussian_signed_square_lagrange ((((c) * (e))) + (((d) * (f))))
  9. L50
    specialize gaussian_signed_square_lagrange ((((c) * (f))) + (((d) * (e))))
  10. L51
    specialize gaussian_signed_square_lagrange x * x2
11Use earlier factsL52–61

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

  1. L52
    specialize gaussian_signed_square_lagrange x1 * x3
  2. L53
    specialize gaussian_signed_square_lagrange x * x3
  3. L54
    specialize gaussian_signed_square_lagrange x1 * x2
  4. L55
    specialize gaussian_signed_square_lagrange x4
  5. L56
    specialize gaussian_signed_square_lagrange x5
  6. L57
    apply gaussian_signed_square_lagrange
  7. L58
    specialize gaussian_signed_square_product a
  8. L59
    specialize gaussian_signed_square_product b
  9. L60
    specialize gaussian_signed_square_product e
  10. L61
    specialize gaussian_signed_square_product f
12Use earlier factsL62–71

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

  1. L62
    specialize gaussian_signed_square_product x
  2. L63
    specialize gaussian_signed_square_product x2
  3. L64
    apply gaussian_signed_square_product
  4. L65
    exact hfirst_witness_witness_left
  5. L66
    exact hsecond_witness_witness_left
  6. L67
    specialize gaussian_signed_square_product c
  7. L68
    specialize gaussian_signed_square_product d
  8. L69
    specialize gaussian_signed_square_product g
  9. L70
    specialize gaussian_signed_square_product h
  10. L71
    specialize gaussian_signed_square_product x1
13Use earlier factsL72–81

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

  1. L72
    specialize gaussian_signed_square_product x3
  2. L73
    apply gaussian_signed_square_product
  3. L74
    exact hfirst_witness_witness_right_left
  4. L75
    exact hsecond_witness_witness_right_left
  5. L76
    specialize gaussian_signed_square_product a
  6. L77
    specialize gaussian_signed_square_product b
  7. L78
    specialize gaussian_signed_square_product g
  8. L79
    specialize gaussian_signed_square_product h
  9. L80
    specialize gaussian_signed_square_product x
  10. L81
    specialize gaussian_signed_square_product x3
14Use earlier factsL82–91

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

  1. L82
    apply gaussian_signed_square_product
  2. L83
    exact hfirst_witness_witness_left
  3. L84
    exact hsecond_witness_witness_right_left
  4. L85
    specialize gaussian_signed_square_product c
  5. L86
    specialize gaussian_signed_square_product d
  6. L87
    specialize gaussian_signed_square_product e
  7. L88
    specialize gaussian_signed_square_product f
  8. L89
    specialize gaussian_signed_square_product x1
  9. L90
    specialize gaussian_signed_square_product x2
  10. L91
    apply gaussian_signed_square_product
15Use earlier factsL92–97

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

  1. L92
    exact hfirst_witness_witness_right_left
  2. L93
    exact hsecond_witness_witness_left
  3. L94
    exact hcross_left
  4. L95
    exact hcross_right
  5. L96
    exact hreal_witness
  6. L97
    exact himaginary_witness
16Construct an explicit witnessL98–99

Supply the displayed value, then prove that it has the required property.

  1. L98
    exists x4
  2. L99
    exists x5
17Separate the logical casesL100–100

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

  1. L100
    split
18Use earlier factsL101–101

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

  1. L101
    exact hreal_witness
19Separate the logical casesL102–102

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

  1. L102
    split
20Use earlier factsL103–103

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

  1. L103
    exact himaginary_witness
21Calculate and transport equalitiesL104–108

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

  1. L104
    rewrite hfirst_witness_witness_right_right
  2. L105
    rewrite hsecond_witness_witness_right_right
  3. L106
    trans ((((x * x2) + (x1 * x3))) + (((x * x3) + (x1 * x2))))
  4. L107
    simp [add_mul, mul_add, add_assoc, add_comm, four_square_add_swap_right_tail]
  5. L108
    symm
22Use earlier factsL109–109

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

  1. L109
    exact hnorm

Library-wide reading audit

Original defined command ledger · 109 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro e
  6. 0006intro f
  7. 0007intro g
  8. 0008intro h
  9. 0009intro N
  10. 0010intro M
  11. 0011intro hfirst
  12. 0012intro hsecond
  13. 0013cases hfirst
  14. 0014cases hfirst_witness
  15. 0015cases hfirst_witness_witness
  16. 0016cases hfirst_witness_witness_right
  17. 0017cases hsecond
  18. 0018cases hsecond_witness
  19. 0019cases hsecond_witness_witness
  20. 0020cases hsecond_witness_witness_right
  21. 0021have hreal : ∃ s. SignedDifferenceSquare(a · e + b · f + (c · h + d · g),a · f + b · e + (c · g + d · h),s)
  22. 0022specialize gaussian_signed_square_exists ((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))
  23. 0023specialize gaussian_signed_square_exists ((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))
  24. 0024apply gaussian_signed_square_exists
  25. 0025cases hreal
  26. 0026have himaginary : ∃ t. SignedDifferenceSquare(a · g + b · h + (c · e + d · f),a · h + b · g + (c · f + d · e),t)
  27. 0027specialize gaussian_signed_square_exists ((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))
  28. 0028specialize gaussian_signed_square_exists ((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))
  29. 0029apply gaussian_signed_square_exists
  30. 0030cases himaginary
  31. 0031have hcross : (((((((((((a) * (e))) + (((b) * (f))))) * (((((c) * (g))) + (((d) * (h))))))) + (((((((a) * (f))) + (((b) * (e))))) * (((((c) * (h))) + (((d) * (g))))))))) = (((((((((a) * (g))) + (((b) * (h))))) * (((((c) * (e))) + (((d) * (f))))))) + (((((((a) * (h))) + (((b) * (g))))) * (((((c) * (f))) + (((d) * (e)))))))))) /\ ((((((((((a) * (e))) + (((b) * (f))))) * (((((c) * (h))) + (((d) * (g))))))) + (((((((a) * (f))) + (((b) * (e))))) * (((((c) * (g))) + (((d) * (h))))))))) = (((((((((a) * (g))) + (((b) * (h))))) * (((((c) * (f))) + (((d) * (e))))))) + (((((((a) * (h))) + (((b) * (g))))) * (((((c) * (e))) + (((d) * (f)))))))))))
  32. 0032specialize gaussian_signed_product_cross_interchange a
  33. 0033specialize gaussian_signed_product_cross_interchange b
  34. 0034specialize gaussian_signed_product_cross_interchange c
  35. 0035specialize gaussian_signed_product_cross_interchange d
  36. 0036specialize gaussian_signed_product_cross_interchange e
  37. 0037specialize gaussian_signed_product_cross_interchange f
  38. 0038specialize gaussian_signed_product_cross_interchange g
  39. 0039specialize gaussian_signed_product_cross_interchange h
  40. 0040apply gaussian_signed_product_cross_interchange
  41. 0041cases hcross
  42. 0042have hnorm : x4 + x5 = ((((x * x2) + (x1 * x3))) + (((x * x3) + (x1 * x2))))
  43. 0043specialize gaussian_signed_square_lagrange ((((a) * (e))) + (((b) * (f))))
  44. 0044specialize gaussian_signed_square_lagrange ((((a) * (f))) + (((b) * (e))))
  45. 0045specialize gaussian_signed_square_lagrange ((((c) * (g))) + (((d) * (h))))
  46. 0046specialize gaussian_signed_square_lagrange ((((c) * (h))) + (((d) * (g))))
  47. 0047specialize gaussian_signed_square_lagrange ((((a) * (g))) + (((b) * (h))))
  48. 0048specialize gaussian_signed_square_lagrange ((((a) * (h))) + (((b) * (g))))
  49. 0049specialize gaussian_signed_square_lagrange ((((c) * (e))) + (((d) * (f))))
  50. 0050specialize gaussian_signed_square_lagrange ((((c) * (f))) + (((d) * (e))))
  51. 0051specialize gaussian_signed_square_lagrange x * x2
  52. 0052specialize gaussian_signed_square_lagrange x1 * x3
  53. 0053specialize gaussian_signed_square_lagrange x * x3
  54. 0054specialize gaussian_signed_square_lagrange x1 * x2
  55. 0055specialize gaussian_signed_square_lagrange x4
  56. 0056specialize gaussian_signed_square_lagrange x5
  57. 0057apply gaussian_signed_square_lagrange
  58. 0058specialize gaussian_signed_square_product a
  59. 0059specialize gaussian_signed_square_product b
  60. 0060specialize gaussian_signed_square_product e
  61. 0061specialize gaussian_signed_square_product f
  62. 0062specialize gaussian_signed_square_product x
  63. 0063specialize gaussian_signed_square_product x2
  64. 0064apply gaussian_signed_square_product
  65. 0065exact hfirst_witness_witness_left
  66. 0066exact hsecond_witness_witness_left
  67. 0067specialize gaussian_signed_square_product c
  68. 0068specialize gaussian_signed_square_product d
  69. 0069specialize gaussian_signed_square_product g
  70. 0070specialize gaussian_signed_square_product h
  71. 0071specialize gaussian_signed_square_product x1
  72. 0072specialize gaussian_signed_square_product x3
  73. 0073apply gaussian_signed_square_product
  74. 0074exact hfirst_witness_witness_right_left
  75. 0075exact hsecond_witness_witness_right_left
  76. 0076specialize gaussian_signed_square_product a
  77. 0077specialize gaussian_signed_square_product b
  78. 0078specialize gaussian_signed_square_product g
  79. 0079specialize gaussian_signed_square_product h
  80. 0080specialize gaussian_signed_square_product x
  81. 0081specialize gaussian_signed_square_product x3
  82. 0082apply gaussian_signed_square_product
  83. 0083exact hfirst_witness_witness_left
  84. 0084exact hsecond_witness_witness_right_left
  85. 0085specialize gaussian_signed_square_product c
  86. 0086specialize gaussian_signed_square_product d
  87. 0087specialize gaussian_signed_square_product e
  88. 0088specialize gaussian_signed_square_product f
  89. 0089specialize gaussian_signed_square_product x1
  90. 0090specialize gaussian_signed_square_product x2
  91. 0091apply gaussian_signed_square_product
  92. 0092exact hfirst_witness_witness_right_left
  93. 0093exact hsecond_witness_witness_left
  94. 0094exact hcross_left
  95. 0095exact hcross_right
  96. 0096exact hreal_witness
  97. 0097exact himaginary_witness
  98. 0098exists x4
  99. 0099exists x5
  100. 0100split
  101. 0101exact hreal_witness
  102. 0102split
  103. 0103exact himaginary_witness
  104. 0104rewrite hfirst_witness_witness_right_right
  105. 0105rewrite hsecond_witness_witness_right_right
  106. 0106trans ((((x * x2) + (x1 * x3))) + (((x * x3) + (x1 * x2))))
  107. 0107simp [add_mul, mul_add, add_assoc, add_comm, four_square_add_swap_right_tail]
  108. 0108symm
  109. 0109exact hnorm