GI0033

gaussian_residual_conjugate_identity

For the actual residual a-bq, multiplication by the conjugate divisor gives exactly the rounded numerator error a*conjugate(b)-N(b)q.

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. ∀ i. ∀ j. ∀ k. ∀ l. ∀ N. GaussianSignedNorm(e,f,g,h,N) → e · (a + (e · j + f · i + (g · k + h · l))) + f · (b + (e · i + f · j + (g · l + h · k))) + (h · (d + (e · k + f · l + (g · i + h · j))) + g · (c + (e · l + f · k + (g · j + h · i)))) + (e · b + f · a + (h · c + g · d) + N · i) = e · a + f · b + (h · d + g · c) + N · j + (e · (b + (e · i + f · j + (g · l + h · k))) + f · (a + (e · j + f · i + (g · k + h · l))) + (h · (c + (e · l + f · k + (g · j + h · i))) + g · (d + (e · k + f · l + (g · i + h · j))))) ∧ e · (c + (e · l + f · k + (g · j + h · i))) + f · (d + (e · k + f · l + (g · i + h · j))) + (h · (a + (e · j + f · i + (g · k + h · l))) + g · (b + (e · i + f · j + (g · l + h · k)))) + (e · d + f · c + (h · b + g · a) + N · k) = e · c + f · d + (h · a + g · b) + N · l + (e · (d + (e · k + f · l + (g · i + h · j))) + f · (c + (e · l + f · k + (g · j + h · i))) + (h · (b + (e · i + f · j + (g · l + h · k))) + g · (a + (e · j + f · i + (g · k + h · l)))))

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

Definition DAG

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

Actual proof prerequisites

gaussian_equal_transitivegaussian_product_differencegaussian_difference_integer_congruencegaussian_equal_reflexivegaussian_adjoint_product_is_norm_scale
Original expanded first-order statement 
forall a b c d e f g h i j k l N. (exists ge_real_square_residual_divisor_norm ge_imaginary_square_residual_divisor_norm. ((((((e) * (e))) + (((f) * (f)))) = ((ge_real_square_residual_divisor_norm) + (((((e) * (f))) + (((f) * (e))))))) /\ ((((((g) * (g))) + (((h) * (h)))) = ((ge_imaginary_square_residual_divisor_norm) + (((((g) * (h))) + (((h) * (g))))))) /\ ((N) = ge_real_square_residual_divisor_norm + ge_imaginary_square_residual_divisor_norm)))) -> (((((((((((e) * (((a) + (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((f) * (((b) + (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))))) + (((((h) * (((d) + (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))))) + (((g) * (((c) + (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))))))))) + (((((((((e) * (b))) + (((f) * (a))))) + (((((h) * (c))) + (((g) * (d))))))) + (((N) * (i)))))) = ((((((((((e) * (a))) + (((f) * (b))))) + (((((h) * (d))) + (((g) * (c))))))) + (((N) * (j))))) + (((((((e) * (((b) + (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((f) * (((a) + (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))))) + (((((h) * (((c) + (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))))) + (((g) * (((d) + (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))))))))))) /\ (((((((((e) * (((c) + (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))))) + (((f) * (((d) + (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))))))) + (((((h) * (((a) + (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((g) * (((b) + (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))))))) + (((((((((e) * (d))) + (((f) * (c))))) + (((((h) * (b))) + (((g) * (a))))))) + (((N) * (k)))))) = ((((((((((e) * (c))) + (((f) * (d))))) + (((((h) * (a))) + (((g) * (b))))))) + (((N) * (l))))) + (((((((e) * (((d) + (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))))) + (((f) * (((c) + (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))))))) + (((((h) * (((b) + (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((g) * (((a) + (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l)))))))))))))))))))

Complete tactic proof in conservative notation

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

73 script commands · 8 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.

Named ingredients (5)
gaussian equal transitivegaussian product differencegaussian difference integer congruencegaussian equal reflexivegaussian adjoint product is norm scale
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 i
  10. L10
    intro j
02Fix variables and assumptionsL11–14

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

  1. L11
    intro k
  2. L12
    intro l
  3. L13
    intro N
  4. L14
    intro hnorm
03Use earlier factsL15–24

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

  1. L15
    specialize gaussian_equal_transitive ((((((e) * (((a) + (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((f) * (((b) + (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))))) + (((((h) * (((d) + (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))))) + (((g) * (((c) + (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))))))))
  2. L16
    specialize gaussian_equal_transitive ((((((e) * (((b) + (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((f) * (((a) + (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))))) + (((((h) * (((c) + (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))))) + (((g) * (((d) + (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))))))))
  3. L17
    specialize gaussian_equal_transitive ((((((e) * (((c) + (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))))) + (((f) * (((d) + (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))))))) + (((((h) * (((a) + (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((g) * (((b) + (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))))))
  4. L18
    specialize gaussian_equal_transitive ((((((e) * (((d) + (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))))) + (((f) * (((c) + (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))))))) + (((((h) * (((b) + (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((g) * (((a) + (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))))))
  5. L19
    specialize gaussian_equal_transitive ((((((((e) * (a))) + (((f) * (b))))) + (((((h) * (d))) + (((g) * (c))))))) + (((((((e) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((f) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((((h) * (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))) + (((g) * (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))))))))
  6. L20
    specialize gaussian_equal_transitive ((((((((e) * (b))) + (((f) * (a))))) + (((((h) * (c))) + (((g) * (d))))))) + (((((((e) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((f) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((((h) * (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))) + (((g) * (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))))))))
  7. L21
    specialize gaussian_equal_transitive ((((((((e) * (c))) + (((f) * (d))))) + (((((h) * (a))) + (((g) * (b))))))) + (((((((e) * (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))) + (((f) * (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))))) + (((((h) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((g) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))))))
  8. L22
    specialize gaussian_equal_transitive ((((((((e) * (d))) + (((f) * (c))))) + (((((h) * (b))) + (((g) * (a))))))) + (((((((e) * (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))) + (((f) * (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))))) + (((((h) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((g) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))))))
  9. L23
    specialize gaussian_equal_transitive ((((((((e) * (a))) + (((f) * (b))))) + (((((h) * (d))) + (((g) * (c))))))) + (((N) * (j))))
  10. L24
    specialize gaussian_equal_transitive ((((((((e) * (b))) + (((f) * (a))))) + (((((h) * (c))) + (((g) * (d))))))) + (((N) * (i))))
04Use earlier factsL25–34

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

  1. L25
    specialize gaussian_equal_transitive ((((((((e) * (c))) + (((f) * (d))))) + (((((h) * (a))) + (((g) * (b))))))) + (((N) * (l))))
  2. L26
    specialize gaussian_equal_transitive ((((((((e) * (d))) + (((f) * (c))))) + (((((h) * (b))) + (((g) * (a))))))) + (((N) * (k))))
  3. L27
    apply gaussian_equal_transitive
  4. L28
    specialize gaussian_product_difference e
  5. L29
    specialize gaussian_product_difference f
  6. L30
    specialize gaussian_product_difference h
  7. L31
    specialize gaussian_product_difference g
  8. L32
    specialize gaussian_product_difference a
  9. L33
    specialize gaussian_product_difference b
  10. L34
    specialize gaussian_product_difference c
05Use earlier factsL35–44

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

  1. L35
    specialize gaussian_product_difference d
  2. L36
    specialize gaussian_product_difference ((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))
  3. L37
    specialize gaussian_product_difference ((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))
  4. L38
    specialize gaussian_product_difference ((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))
  5. L39
    specialize gaussian_product_difference ((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))
  6. L40
    apply gaussian_product_difference
  7. L41
    specialize gaussian_difference_integer_congruence ((((((e) * (a))) + (((f) * (b))))) + (((((h) * (d))) + (((g) * (c))))))
  8. L42
    specialize gaussian_difference_integer_congruence ((((((e) * (b))) + (((f) * (a))))) + (((((h) * (c))) + (((g) * (d))))))
  9. L43
    specialize gaussian_difference_integer_congruence ((((((e) * (c))) + (((f) * (d))))) + (((((h) * (a))) + (((g) * (b))))))
  10. L44
    specialize gaussian_difference_integer_congruence ((((((e) * (d))) + (((f) * (c))))) + (((((h) * (b))) + (((g) * (a))))))
06Use earlier factsL45–54

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

  1. L45
    specialize gaussian_difference_integer_congruence ((((((e) * (a))) + (((f) * (b))))) + (((((h) * (d))) + (((g) * (c))))))
  2. L46
    specialize gaussian_difference_integer_congruence ((((((e) * (b))) + (((f) * (a))))) + (((((h) * (c))) + (((g) * (d))))))
  3. L47
    specialize gaussian_difference_integer_congruence ((((((e) * (c))) + (((f) * (d))))) + (((((h) * (a))) + (((g) * (b))))))
  4. L48
    specialize gaussian_difference_integer_congruence ((((((e) * (d))) + (((f) * (c))))) + (((((h) * (b))) + (((g) * (a))))))
  5. L49
    specialize gaussian_difference_integer_congruence ((((((e) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((f) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((((h) * (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))) + (((g) * (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))))))
  6. L50
    specialize gaussian_difference_integer_congruence ((((((e) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((f) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((((h) * (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))) + (((g) * (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))))))
  7. L51
    specialize gaussian_difference_integer_congruence ((((((e) * (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))) + (((f) * (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))))) + (((((h) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((g) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))))
  8. L52
    specialize gaussian_difference_integer_congruence ((((((e) * (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))) + (((f) * (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))))) + (((((h) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((g) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))))
  9. L53
    specialize gaussian_difference_integer_congruence ((N) * (i))
  10. L54
    specialize gaussian_difference_integer_congruence ((N) * (j))
07Use earlier factsL55–64

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

  1. L55
    specialize gaussian_difference_integer_congruence ((N) * (k))
  2. L56
    specialize gaussian_difference_integer_congruence ((N) * (l))
  3. L57
    apply gaussian_difference_integer_congruence
  4. L58
    specialize gaussian_equal_reflexive ((((((e) * (a))) + (((f) * (b))))) + (((((h) * (d))) + (((g) * (c))))))
  5. L59
    specialize gaussian_equal_reflexive ((((((e) * (b))) + (((f) * (a))))) + (((((h) * (c))) + (((g) * (d))))))
  6. L60
    specialize gaussian_equal_reflexive ((((((e) * (c))) + (((f) * (d))))) + (((((h) * (a))) + (((g) * (b))))))
  7. L61
    specialize gaussian_equal_reflexive ((((((e) * (d))) + (((f) * (c))))) + (((((h) * (b))) + (((g) * (a))))))
  8. L62
    apply gaussian_equal_reflexive
  9. L63
    specialize gaussian_adjoint_product_is_norm_scale e
  10. L64
    specialize gaussian_adjoint_product_is_norm_scale f
08Use earlier factsL65–73

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

  1. L65
    specialize gaussian_adjoint_product_is_norm_scale g
  2. L66
    specialize gaussian_adjoint_product_is_norm_scale h
  3. L67
    specialize gaussian_adjoint_product_is_norm_scale i
  4. L68
    specialize gaussian_adjoint_product_is_norm_scale j
  5. L69
    specialize gaussian_adjoint_product_is_norm_scale k
  6. L70
    specialize gaussian_adjoint_product_is_norm_scale l
  7. L71
    specialize gaussian_adjoint_product_is_norm_scale N
  8. L72
    apply gaussian_adjoint_product_is_norm_scale
  9. L73
    exact hnorm

Library-wide reading audit

Original defined command ledger · 73 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 i
  10. 0010intro j
  11. 0011intro k
  12. 0012intro l
  13. 0013intro N
  14. 0014intro hnorm
  15. 0015specialize gaussian_equal_transitive ((((((e) * (((a) + (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((f) * (((b) + (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))))) + (((((h) * (((d) + (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))))) + (((g) * (((c) + (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))))))))
  16. 0016specialize gaussian_equal_transitive ((((((e) * (((b) + (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((f) * (((a) + (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))))) + (((((h) * (((c) + (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))))) + (((g) * (((d) + (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))))))))
  17. 0017specialize gaussian_equal_transitive ((((((e) * (((c) + (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))))) + (((f) * (((d) + (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))))))) + (((((h) * (((a) + (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((g) * (((b) + (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))))))
  18. 0018specialize gaussian_equal_transitive ((((((e) * (((d) + (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))))) + (((f) * (((c) + (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))))))) + (((((h) * (((b) + (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((g) * (((a) + (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))))))
  19. 0019specialize gaussian_equal_transitive ((((((((e) * (a))) + (((f) * (b))))) + (((((h) * (d))) + (((g) * (c))))))) + (((((((e) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((f) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((((h) * (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))) + (((g) * (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))))))))
  20. 0020specialize gaussian_equal_transitive ((((((((e) * (b))) + (((f) * (a))))) + (((((h) * (c))) + (((g) * (d))))))) + (((((((e) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((f) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((((h) * (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))) + (((g) * (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))))))))
  21. 0021specialize gaussian_equal_transitive ((((((((e) * (c))) + (((f) * (d))))) + (((((h) * (a))) + (((g) * (b))))))) + (((((((e) * (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))) + (((f) * (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))))) + (((((h) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((g) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))))))
  22. 0022specialize gaussian_equal_transitive ((((((((e) * (d))) + (((f) * (c))))) + (((((h) * (b))) + (((g) * (a))))))) + (((((((e) * (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))) + (((f) * (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))))) + (((((h) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((g) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))))))
  23. 0023specialize gaussian_equal_transitive ((((((((e) * (a))) + (((f) * (b))))) + (((((h) * (d))) + (((g) * (c))))))) + (((N) * (j))))
  24. 0024specialize gaussian_equal_transitive ((((((((e) * (b))) + (((f) * (a))))) + (((((h) * (c))) + (((g) * (d))))))) + (((N) * (i))))
  25. 0025specialize gaussian_equal_transitive ((((((((e) * (c))) + (((f) * (d))))) + (((((h) * (a))) + (((g) * (b))))))) + (((N) * (l))))
  26. 0026specialize gaussian_equal_transitive ((((((((e) * (d))) + (((f) * (c))))) + (((((h) * (b))) + (((g) * (a))))))) + (((N) * (k))))
  27. 0027apply gaussian_equal_transitive
  28. 0028specialize gaussian_product_difference e
  29. 0029specialize gaussian_product_difference f
  30. 0030specialize gaussian_product_difference h
  31. 0031specialize gaussian_product_difference g
  32. 0032specialize gaussian_product_difference a
  33. 0033specialize gaussian_product_difference b
  34. 0034specialize gaussian_product_difference c
  35. 0035specialize gaussian_product_difference d
  36. 0036specialize gaussian_product_difference ((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))
  37. 0037specialize gaussian_product_difference ((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))
  38. 0038specialize gaussian_product_difference ((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))
  39. 0039specialize gaussian_product_difference ((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))
  40. 0040apply gaussian_product_difference
  41. 0041specialize gaussian_difference_integer_congruence ((((((e) * (a))) + (((f) * (b))))) + (((((h) * (d))) + (((g) * (c))))))
  42. 0042specialize gaussian_difference_integer_congruence ((((((e) * (b))) + (((f) * (a))))) + (((((h) * (c))) + (((g) * (d))))))
  43. 0043specialize gaussian_difference_integer_congruence ((((((e) * (c))) + (((f) * (d))))) + (((((h) * (a))) + (((g) * (b))))))
  44. 0044specialize gaussian_difference_integer_congruence ((((((e) * (d))) + (((f) * (c))))) + (((((h) * (b))) + (((g) * (a))))))
  45. 0045specialize gaussian_difference_integer_congruence ((((((e) * (a))) + (((f) * (b))))) + (((((h) * (d))) + (((g) * (c))))))
  46. 0046specialize gaussian_difference_integer_congruence ((((((e) * (b))) + (((f) * (a))))) + (((((h) * (c))) + (((g) * (d))))))
  47. 0047specialize gaussian_difference_integer_congruence ((((((e) * (c))) + (((f) * (d))))) + (((((h) * (a))) + (((g) * (b))))))
  48. 0048specialize gaussian_difference_integer_congruence ((((((e) * (d))) + (((f) * (c))))) + (((((h) * (b))) + (((g) * (a))))))
  49. 0049specialize gaussian_difference_integer_congruence ((((((e) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((f) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((((h) * (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))) + (((g) * (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))))))
  50. 0050specialize gaussian_difference_integer_congruence ((((((e) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((f) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((((h) * (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))) + (((g) * (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))))))
  51. 0051specialize gaussian_difference_integer_congruence ((((((e) * (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))) + (((f) * (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))))) + (((((h) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((g) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))))
  52. 0052specialize gaussian_difference_integer_congruence ((((((e) * (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))) + (((f) * (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))))) + (((((h) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((g) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))))
  53. 0053specialize gaussian_difference_integer_congruence ((N) * (i))
  54. 0054specialize gaussian_difference_integer_congruence ((N) * (j))
  55. 0055specialize gaussian_difference_integer_congruence ((N) * (k))
  56. 0056specialize gaussian_difference_integer_congruence ((N) * (l))
  57. 0057apply gaussian_difference_integer_congruence
  58. 0058specialize gaussian_equal_reflexive ((((((e) * (a))) + (((f) * (b))))) + (((((h) * (d))) + (((g) * (c))))))
  59. 0059specialize gaussian_equal_reflexive ((((((e) * (b))) + (((f) * (a))))) + (((((h) * (c))) + (((g) * (d))))))
  60. 0060specialize gaussian_equal_reflexive ((((((e) * (c))) + (((f) * (d))))) + (((((h) * (a))) + (((g) * (b))))))
  61. 0061specialize gaussian_equal_reflexive ((((((e) * (d))) + (((f) * (c))))) + (((((h) * (b))) + (((g) * (a))))))
  62. 0062apply gaussian_equal_reflexive
  63. 0063specialize gaussian_adjoint_product_is_norm_scale e
  64. 0064specialize gaussian_adjoint_product_is_norm_scale f
  65. 0065specialize gaussian_adjoint_product_is_norm_scale g
  66. 0066specialize gaussian_adjoint_product_is_norm_scale h
  67. 0067specialize gaussian_adjoint_product_is_norm_scale i
  68. 0068specialize gaussian_adjoint_product_is_norm_scale j
  69. 0069specialize gaussian_adjoint_product_is_norm_scale k
  70. 0070specialize gaussian_adjoint_product_is_norm_scale l
  71. 0071specialize gaussian_adjoint_product_is_norm_scale N
  72. 0072apply gaussian_adjoint_product_is_norm_scale
  73. 0073exact hnorm