GI003A

gaussian_signed_euclidean_division_exists

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

Construct a genuine Gaussian quotient and remainder with exact a=bq+r and strict norm decrease for every nonzero divisor; neither quotients nor a remainder bound are assumed.

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 e f g h. ~(e = f /\ g = h) -> exists qp qn up un rp rn sp sn U V. (((((((((((((((e) * (qp))) + (((f) * (qn))))) + (((((g) * (un))) + (((h) * (up))))))) + (rp))) + (b)) = ((a) + (((((((((e) * (qn))) + (((f) * (qp))))) + (((((g) * (up))) + (((h) * (un))))))) + (rn))))) /\ (((((((((((e) * (up))) + (((f) * (un))))) + (((((g) * (qp))) + (((h) * (qn))))))) + (sp))) + (d)) = ((c) + (((((((((e) * (un))) + (((f) * (up))))) + (((((g) * (qn))) + (((h) * (qp))))))) + (sn))))))) /\ ((exists ge_real_square_full_signed_divisionremainder ge_imaginary_square_full_signed_divisionremainder. ((((((rp) * (rp))) + (((rn) * (rn)))) = ((ge_real_square_full_signed_divisionremainder) + (((((rp) * (rn))) + (((rn) * (rp))))))) /\ ((((((sp) * (sp))) + (((sn) * (sn)))) = ((ge_imaginary_square_full_signed_divisionremainder) + (((((sp) * (sn))) + (((sn) * (sp))))))) /\ ((U) = ge_real_square_full_signed_divisionremainder + ge_imaginary_square_full_signed_divisionremainder)))) /\ ((exists ge_real_square_full_signed_divisiondivisor ge_imaginary_square_full_signed_divisiondivisor. ((((((e) * (e))) + (((f) * (f)))) = ((ge_real_square_full_signed_divisiondivisor) + (((((e) * (f))) + (((f) * (e))))))) /\ ((((((g) * (g))) + (((h) * (h)))) = ((ge_imaginary_square_full_signed_divisiondivisor) + (((((g) * (h))) + (((h) * (g))))))) /\ ((V) = ge_real_square_full_signed_divisiondivisor + ge_imaginary_square_full_signed_divisiondivisor)))) /\ (exists ge_gap_full_signed_divisionstrict. ge_gap_full_signed_divisionstrict + S (U) = (V))))))

Constructive proof overview

Generated structural guide

Construct a genuine Gaussian quotient and remainder with exact a=bq+r and strict norm decrease for every nonzero divisor; neither quotients nor a remainder bound are assumed.

The unchanged tactic script uses 13 declared prerequisites and contains 187 exact native proof lines.

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

Proof neighborhood

Direct dependencies

GI0012 gaussian_signed_norm_exists GI001E gaussian_signed_norm_nonzero GI0039 gaussian_nearest_signed_quotient_exists GI002C gaussian_equal_transitive GI0033 gaussian_residual_conjugate_identity GI001A gaussian_signed_norm_product GI001C gaussian_signed_norm_conjugate GI001B gaussian_signed_norm_integer_transport GI0013 gaussian_signed_norm_functional GI0038 gaussian_two_half_squares_strict GI0034 gaussian_difference_reconstructs_dividend four_square_descent_norm_bound_forces_smaller_multiplier Alpha theorem; checked-use authorized add_comm Stable theorem; checked-use authorized

Direct dependents

GI005D gaussian_euclidean_division_exists

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

187 script commands · 40 reading checkpoints · 12 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 (11)
gaussian signed norm existsgaussian signed norm nonzerogaussian nearest signed quotient existsgaussian equal transitivegaussian residual conjugate identitygaussian signed norm productgaussian signed norm conjugategaussian signed norm integer transportgaussian signed norm functionalgaussian two half squares strictgaussian difference reconstructs dividend

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–9

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 hnonzero
02Establish hdivisorL10–15

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

  1. L10
    have hdivisor : exists N. (exists ge_real_square_division_divisor_norm ge_imaginary_square_division_divisor_norm. ((((((e) * (e))) + (((f) * (f)))) = ((ge_real_square_division_divisor_norm) + (((((e) * (f))) + (((f) * (e))))))) /\ ((((((g) * (g))) + (((h) * (h)))) = ((ge_imaginary_square_division_divisor_norm) + (((((g) * (h))) + (((h) * (g))))))) /\ ((N) = ge_real_square_division_divisor_norm + ge_imaginary_square_division_divisor_norm))))
  2. L11
    specialize gaussian_signed_norm_exists e
  3. L12
    specialize gaussian_signed_norm_exists f
  4. L13
    specialize gaussian_signed_norm_exists g
  5. L14
    specialize gaussian_signed_norm_exists h
  6. L15
    apply gaussian_signed_norm_exists
03Separate the logical casesL16–16

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

  1. L16
    cases hdivisor
04Establish hNL17–26

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

  1. L17
    have hN : ~(x = 0)
  2. L18
    intro hzero
  3. L19
    specialize gaussian_signed_norm_nonzero e
  4. L20
    specialize gaussian_signed_norm_nonzero f
  5. L21
    specialize gaussian_signed_norm_nonzero g
  6. L22
    specialize gaussian_signed_norm_nonzero h
  7. L23
    specialize gaussian_signed_norm_nonzero x
  8. L24
    apply gaussian_signed_norm_nonzero
  9. L25
    exact hdivisor_witness
  10. L26
    exact hnonzero
05Use earlier factsL27–27

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

  1. L27
    exact hzero
06Establish hrealL28–33

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

  1. L28
    have hreal : exists qp qn ep en t. (((((((((((e) * (a))) + (((f) * (b))))) + (((((h) * (d))) + (((g) * (c))))))) + (x) * (qn)) + (en) = ((((((((e) * (b))) + (((f) * (a))))) + (((((h) * (c))) + (((g) * (d))))))) + (x) * (qp)) + (ep)) /\ ((((((ep) * (ep))) + (((en) * (en)))) = ((((t) * (t))) + (((((ep) * (en))) + (((en) * (ep))))))) /\ (exists ge_gap_division_real_roundhalf_bound. ge_gap_division_real_roundhalf_bound + (((t) + (t))) = (x)))))
  2. L29
    specialize gaussian_nearest_signed_quotient_exists ((((((e) * (a))) + (((f) * (b))))) + (((((h) * (d))) + (((g) * (c))))))
  3. L30
    specialize gaussian_nearest_signed_quotient_exists ((((((e) * (b))) + (((f) * (a))))) + (((((h) * (c))) + (((g) * (d))))))
  4. L31
    specialize gaussian_nearest_signed_quotient_exists x
  5. L32
    apply gaussian_nearest_signed_quotient_exists
  6. L33
    exact hN
07Separate the logical casesL34–40

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

  1. L34
    cases hreal
  2. L35
    cases hreal_witness
  3. L36
    cases hreal_witness_witness
  4. L37
    cases hreal_witness_witness_witness
  5. L38
    cases hreal_witness_witness_witness_witness
  6. L39
    cases hreal_witness_witness_witness_witness_witness
  7. L40
    cases hreal_witness_witness_witness_witness_witness_right
08Establish himaginaryL41–46

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

  1. L41
    have himaginary : exists qp qn ep en t. (((((((((((e) * (c))) + (((f) * (d))))) + (((((h) * (a))) + (((g) * (b))))))) + (x) * (qn)) + (en) = ((((((((e) * (d))) + (((f) * (c))))) + (((((h) * (b))) + (((g) * (a))))))) + (x) * (qp)) + (ep)) /\ ((((((ep) * (ep))) + (((en) * (en)))) = ((((t) * (t))) + (((((ep) * (en))) + (((en) * (ep))))))) /\ (exists ge_gap_division_imaginary_roundhalf_bound. ge_gap_division_imaginary_roundhalf_bound + (((t) + (t))) = (x)))))
  2. L42
    specialize gaussian_nearest_signed_quotient_exists ((((((e) * (c))) + (((f) * (d))))) + (((((h) * (a))) + (((g) * (b))))))
  3. L43
    specialize gaussian_nearest_signed_quotient_exists ((((((e) * (d))) + (((f) * (c))))) + (((((h) * (b))) + (((g) * (a))))))
  4. L44
    specialize gaussian_nearest_signed_quotient_exists x
  5. L45
    apply gaussian_nearest_signed_quotient_exists
  6. L46
    exact hN
09Separate the logical casesL47–53

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

  1. L47
    cases himaginary
  2. L48
    cases himaginary_witness
  3. L49
    cases himaginary_witness_witness
  4. L50
    cases himaginary_witness_witness_witness
  5. L51
    cases himaginary_witness_witness_witness_witness
  6. L52
    cases himaginary_witness_witness_witness_witness_witness
  7. L53
    cases himaginary_witness_witness_witness_witness_witness_right
10Establish hremainderL54–59

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

  1. L54
    have hremainder : ∃ M. GaussianSignedNorm(a + (e · x2 + f · x1 + (g · x6 + h · x7)),b + (e · x1 + f · x2 + (g · x7 + h · x6)),c + (e · x7 + f · x6 + (g · x2 + h · x1)),d + (e · x6 + f · x7 + (g · x1 + h · x2)),M)Definitions: GaussianSignedNorm
  2. L55
    specialize gaussian_signed_norm_exists ((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))
  3. L56
    specialize gaussian_signed_norm_exists ((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))
  4. L57
    specialize gaussian_signed_norm_exists ((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))
  5. L58
    specialize gaussian_signed_norm_exists ((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))
  6. L59
    apply gaussian_signed_norm_exists
11Separate the logical casesL60–60

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

  1. L60
    cases hremainder
12Establish herror_normL61–61

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

  1. L61
    have herror_norm : exists ge_real_square_constructed_error_norm ge_imaginary_square_constructed_error_norm. ((((((x3) * (x3))) + (((x4) * (x4)))) = ((ge_real_square_constructed_error_norm) + (((((x3) * (x4))) + (((x4) * (x3))))))) /\ ((((((x8) * (x8))) + (((x9) * (x9)))) = ((ge_imaginary_square_constructed_error_norm) + (((((x8) * (x9))) + (((x9) * (x8))))))) /\ ((x5 * x5 + x10 * x10) = ge_real_square_constructed_error_norm + ge_imaginary_square_constructed_error_norm)))
13Construct an explicit witnessL62–63

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

  1. L62
    exists x5 * x5
  2. L63
    exists x10 * x10
14Separate the logical casesL64–64

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

  1. L64
    split
15Use earlier factsL65–65

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

  1. L65
    exact hreal_witness_witness_witness_witness_witness_right_left
16Separate the logical casesL66–66

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

  1. L66
    split
17Use earlier factsL67–67

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

  1. L67
    exact himaginary_witness_witness_witness_witness_witness_right_left
18Calculate and transport equalitiesL68–68

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

  1. L68
    refl
19Establish herror_equationL69–69

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

  1. L69
    have herror_equation : ((((((((((((e) * (a))) + (((f) * (b))))) + (((((h) * (d))) + (((g) * (c))))))) + (((x) * (x2))))) + (x4)) = ((x3) + (((((((((e) * (b))) + (((f) * (a))))) + (((((h) * (c))) + (((g) * (d))))))) + (((x) * (x1))))))) /\ (((((((((((e) * (c))) + (((f) * (d))))) + (((((h) * (a))) + (((g) * (b))))))) + (((x) * (x7))))) + (x9)) = ((x8) + (((((((((e) * (d))) + (((f) * (c))))) + (((((h) * (b))) + (((g) * (a))))))) + (((x) * (x6))))))))
20Separate the logical casesL70–70

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

  1. L70
    split
21Calculate and transport equalitiesL71–71

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

  1. L71
    trans ((((((((e) * (b))) + (((f) * (a))))) + (((((h) * (c))) + (((g) * (d))))))) + x * (x1)) + (x3)
22Use earlier factsL72–73

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

  1. L72
    exact hreal_witness_witness_witness_witness_witness_left
  2. L73
    apply add_comm
23Calculate and transport equalitiesL74–74

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

  1. L74
    trans ((((((((e) * (d))) + (((f) * (c))))) + (((((h) * (b))) + (((g) * (a))))))) + x * (x6)) + (x8)
24Use earlier factsL75–76

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

  1. L75
    exact himaginary_witness_witness_witness_witness_witness_left
  2. L76
    apply add_comm
25Establish hconjugate_errorL77–86

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

  1. L77
    have hconjugate_error · expand full local formula (1,712 characters)have hconjugate_error : ((((((((((e) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))) + (((f) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))))) + (((((h) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))) + (((g) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))))))) + (x4)) = ((x3) + (((((((e) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))) + (((f) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))))) + (((((h) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))) + (((g) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))))))))) /\ (((((((((e) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))) + (((f) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))))) + (((((h) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))) + (((g) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))))))) + (x9)) = ((x8) + (((((((e) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))) + (((f) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))))) + (((((h) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))) + (((g) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))))))))))
  2. L78
    specialize gaussian_equal_transitive ((((((e) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))) + (((f) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))))) + (((((h) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))) + (((g) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))))))
  3. L79
    specialize gaussian_equal_transitive ((((((e) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))) + (((f) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))))) + (((((h) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))) + (((g) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))))))
  4. L80
    specialize gaussian_equal_transitive ((((((e) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))) + (((f) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))))) + (((((h) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))) + (((g) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))))))
  5. L81
    specialize gaussian_equal_transitive ((((((e) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))) + (((f) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))))) + (((((h) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))) + (((g) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))))))
  6. L82
    specialize gaussian_equal_transitive ((((((((e) * (a))) + (((f) * (b))))) + (((((h) * (d))) + (((g) * (c))))))) + (((x) * (x2))))
  7. L83
    specialize gaussian_equal_transitive ((((((((e) * (b))) + (((f) * (a))))) + (((((h) * (c))) + (((g) * (d))))))) + (((x) * (x1))))
  8. L84
    specialize gaussian_equal_transitive ((((((((e) * (c))) + (((f) * (d))))) + (((((h) * (a))) + (((g) * (b))))))) + (((x) * (x7))))
  9. L85
    specialize gaussian_equal_transitive ((((((((e) * (d))) + (((f) * (c))))) + (((((h) * (b))) + (((g) * (a))))))) + (((x) * (x6))))
  10. L86
    specialize gaussian_equal_transitive x3
26Use earlier factsL87–96

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

  1. L87
    specialize gaussian_equal_transitive x4
  2. L88
    specialize gaussian_equal_transitive x8
  3. L89
    specialize gaussian_equal_transitive x9
  4. L90
    apply gaussian_equal_transitive
  5. L91
    specialize gaussian_residual_conjugate_identity a
  6. L92
    specialize gaussian_residual_conjugate_identity b
  7. L93
    specialize gaussian_residual_conjugate_identity c
  8. L94
    specialize gaussian_residual_conjugate_identity d
  9. L95
    specialize gaussian_residual_conjugate_identity e
  10. L96
    specialize gaussian_residual_conjugate_identity f
27Use earlier factsL97–106

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

  1. L97
    specialize gaussian_residual_conjugate_identity g
  2. L98
    specialize gaussian_residual_conjugate_identity h
  3. L99
    specialize gaussian_residual_conjugate_identity x1
  4. L100
    specialize gaussian_residual_conjugate_identity x2
  5. L101
    specialize gaussian_residual_conjugate_identity x6
  6. L102
    specialize gaussian_residual_conjugate_identity x7
  7. L103
    specialize gaussian_residual_conjugate_identity x
  8. L104
    apply gaussian_residual_conjugate_identity
  9. L105
    exact hdivisor_witness
  10. L106
    exact herror_equation
28Establish hproduct_normL107–116

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

  1. L107
    have hproduct_norm · expand full local formula (848 characters)have hproduct_norm : GaussianSignedNorm(e · (a + (e · x2 + f · x1 + (g · x6 + h · x7))) + f · (b + (e · x1 + f · x2 + (g · x7 + h · x6))) + (h · (d + (e · x6 + f · x7 + (g · x1 + h · x2))) + g · (c + (e · x7 + f · x6 + (g · x2 + h · x1)))),e · (b + (e · x1 + f · x2 + (g · x7 + h · x6))) + f · (a + (e · x2 + f · x1 + (g · x6 + h · x7))) + (h · (c + (e · x7 + f · x6 + (g · x2 + h · x1))) + g · (d + (e · x6 + f · x7 + (g · x1 + h · x2)))),e · (c + (e · x7 + f · x6 + (g · x2 + h · x1))) + f · (d + (e · x6 + f · x7 + (g · x1 + h · x2))) + (h · (a + (e · x2 + f · x1 + (g · x6 + h · x7))) + g · (b + (e · x1 + f · x2 + (g · x7 + h · x6)))),e · (d + (e · x6 + f · x7 + (g · x1 + h · x2))) + f · (c + (e · x7 + f · x6 + (g · x2 + h · x1))) + (h · (b + (e · x1 + f · x2 + (g · x7 + h · x6))) + g · (a + (e · x2 + f · x1 + (g · x6 + h · x7)))),x · x11)
    Definitions: GaussianSignedNorm
  2. L108
    specialize gaussian_signed_norm_product e
  3. L109
    specialize gaussian_signed_norm_product f
  4. L110
    specialize gaussian_signed_norm_product h
  5. L111
    specialize gaussian_signed_norm_product g
  6. L112
    specialize gaussian_signed_norm_product ((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))
  7. L113
    specialize gaussian_signed_norm_product ((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))
  8. L114
    specialize gaussian_signed_norm_product ((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))
  9. L115
    specialize gaussian_signed_norm_product ((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))
  10. L116
    specialize gaussian_signed_norm_product x
29Use earlier factsL117–126

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

  1. L117
    specialize gaussian_signed_norm_product x11
  2. L118
    apply gaussian_signed_norm_product
  3. L119
    specialize gaussian_signed_norm_conjugate e
  4. L120
    specialize gaussian_signed_norm_conjugate f
  5. L121
    specialize gaussian_signed_norm_conjugate g
  6. L122
    specialize gaussian_signed_norm_conjugate h
  7. L123
    specialize gaussian_signed_norm_conjugate x
  8. L124
    apply gaussian_signed_norm_conjugate
  9. L125
    exact hdivisor_witness
  10. L126
    exact hremainder_witness
30Establish htransported_normL127–136

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

  1. L127
    have htransported_norm : exists ge_real_square_actual_error_product_norm ge_imaginary_square_actual_error_product_norm. ((((((x3) * (x3))) + (((x4) * (x4)))) = ((ge_real_square_actual_error_product_norm) + (((((x3) * (x4))) + (((x4) * (x3))))))) /\ ((((((x8) * (x8))) + (((x9) * (x9)))) = ((ge_imaginary_square_actual_error_product_norm) + (((((x8) * (x9))) + (((x9) * (x8))))))) /\ ((x * x11) = ge_real_square_actual_error_product_norm + ge_imaginary_square_actual_error_product_norm)))
  2. L128
    specialize gaussian_signed_norm_integer_transport ((((((e) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))) + (((f) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))))) + (((((h) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))) + (((g) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))))))
  3. L129
    specialize gaussian_signed_norm_integer_transport ((((((e) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))) + (((f) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))))) + (((((h) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))) + (((g) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))))))
  4. L130
    specialize gaussian_signed_norm_integer_transport ((((((e) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))) + (((f) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))))) + (((((h) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))) + (((g) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))))))
  5. L131
    specialize gaussian_signed_norm_integer_transport ((((((e) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))) + (((f) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))))) + (((((h) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))) + (((g) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))))))
  6. L132
    specialize gaussian_signed_norm_integer_transport x3
  7. L133
    specialize gaussian_signed_norm_integer_transport x4
  8. L134
    specialize gaussian_signed_norm_integer_transport x8
  9. L135
    specialize gaussian_signed_norm_integer_transport x9
  10. L136
    specialize gaussian_signed_norm_integer_transport x * x11
31Use earlier factsL137–139

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

  1. L137
    apply gaussian_signed_norm_integer_transport
  2. L138
    exact hconjugate_error
  3. L139
    exact hproduct_norm
32Establish hnorm_equationL140–149

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

  1. L140
    have hnorm_equation : x * x11 = x5 * x5 + x10 * x10
  2. L141
    specialize gaussian_signed_norm_functional x3
  3. L142
    specialize gaussian_signed_norm_functional x4
  4. L143
    specialize gaussian_signed_norm_functional x8
  5. L144
    specialize gaussian_signed_norm_functional x9
  6. L145
    specialize gaussian_signed_norm_functional x * x11
  7. L146
    specialize gaussian_signed_norm_functional x5 * x5 + x10 * x10
  8. L147
    apply gaussian_signed_norm_functional
  9. L148
    exact htransported_norm
  10. L149
    exact herror_norm
33Establish hstrictL150–157

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian two half squares strict.

  1. L150
    have hstrict : exists ge_gap_actual_error_strict_bound. ge_gap_actual_error_strict_bound + S (x5 * x5 + x10 * x10) = (x * x)
  2. L151
    specialize gaussian_two_half_squares_strict x
  3. L152
    specialize gaussian_two_half_squares_strict x5
  4. L153
    specialize gaussian_two_half_squares_strict x10
  5. L154
    apply gaussian_two_half_squares_strict
  6. L155
    exact hN
  7. L156
    exact hreal_witness_witness_witness_witness_witness_right_right
  8. L157
    exact himaginary_witness_witness_witness_witness_witness_right_right
34Construct an explicit witnessL158–167

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

  1. L158
    exists x1
  2. L159
    exists x2
  3. L160
    exists x6
  4. L161
    exists x7
  5. L162
    exists ((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))
  6. L163
    exists ((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))
  7. L164
    exists ((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))
  8. L165
    exists ((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))
  9. L166
    exists x11
  10. L167
    exists x
35Separate the logical casesL168–168

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

  1. L168
    split
36Use earlier factsL169–177

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

  1. L169
    specialize gaussian_difference_reconstructs_dividend a
  2. L170
    specialize gaussian_difference_reconstructs_dividend b
  3. L171
    specialize gaussian_difference_reconstructs_dividend c
  4. L172
    specialize gaussian_difference_reconstructs_dividend d
  5. L173
    specialize gaussian_difference_reconstructs_dividend ((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))
  6. L174
    specialize gaussian_difference_reconstructs_dividend ((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))
  7. L175
    specialize gaussian_difference_reconstructs_dividend ((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))
  8. L176
    specialize gaussian_difference_reconstructs_dividend ((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))
  9. L177
    apply gaussian_difference_reconstructs_dividend
37Separate the logical casesL178–178

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

  1. L178
    split
38Use earlier factsL179–179

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

  1. L179
    exact hremainder_witness
39Separate the logical casesL180–180

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

  1. L180
    split
40Use earlier factsL181–187

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

  1. L181
    exact hdivisor_witness
  2. L182
    specialize four_square_descent_norm_bound_forces_smaller_multiplier x
  3. L183
    specialize four_square_descent_norm_bound_forces_smaller_multiplier x11
  4. L184
    specialize four_square_descent_norm_bound_forces_smaller_multiplier x5 * x5 + x10 * x10
  5. L185
    apply four_square_descent_norm_bound_forces_smaller_multiplier
  6. L186
    exact hnorm_equation
  7. L187
    exact hstrict

Library-wide reading audit

Original exact command ledger · 187 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 hnonzero
  10. 0010have hdivisor : exists N. (exists ge_real_square_division_divisor_norm ge_imaginary_square_division_divisor_norm. ((((((e) * (e))) + (((f) * (f)))) = ((ge_real_square_division_divisor_norm) + (((((e) * (f))) + (((f) * (e))))))) /\ ((((((g) * (g))) + (((h) * (h)))) = ((ge_imaginary_square_division_divisor_norm) + (((((g) * (h))) + (((h) * (g))))))) /\ ((N) = ge_real_square_division_divisor_norm + ge_imaginary_square_division_divisor_norm))))
  11. 0011specialize gaussian_signed_norm_exists e
  12. 0012specialize gaussian_signed_norm_exists f
  13. 0013specialize gaussian_signed_norm_exists g
  14. 0014specialize gaussian_signed_norm_exists h
  15. 0015apply gaussian_signed_norm_exists
  16. 0016cases hdivisor
  17. 0017have hN : ~(x = 0)
  18. 0018intro hzero
  19. 0019specialize gaussian_signed_norm_nonzero e
  20. 0020specialize gaussian_signed_norm_nonzero f
  21. 0021specialize gaussian_signed_norm_nonzero g
  22. 0022specialize gaussian_signed_norm_nonzero h
  23. 0023specialize gaussian_signed_norm_nonzero x
  24. 0024apply gaussian_signed_norm_nonzero
  25. 0025exact hdivisor_witness
  26. 0026exact hnonzero
  27. 0027exact hzero
  28. 0028have hreal : exists qp qn ep en t. (((((((((((e) * (a))) + (((f) * (b))))) + (((((h) * (d))) + (((g) * (c))))))) + (x) * (qn)) + (en) = ((((((((e) * (b))) + (((f) * (a))))) + (((((h) * (c))) + (((g) * (d))))))) + (x) * (qp)) + (ep)) /\ ((((((ep) * (ep))) + (((en) * (en)))) = ((((t) * (t))) + (((((ep) * (en))) + (((en) * (ep))))))) /\ (exists ge_gap_division_real_roundhalf_bound. ge_gap_division_real_roundhalf_bound + (((t) + (t))) = (x)))))
  29. 0029specialize gaussian_nearest_signed_quotient_exists ((((((e) * (a))) + (((f) * (b))))) + (((((h) * (d))) + (((g) * (c))))))
  30. 0030specialize gaussian_nearest_signed_quotient_exists ((((((e) * (b))) + (((f) * (a))))) + (((((h) * (c))) + (((g) * (d))))))
  31. 0031specialize gaussian_nearest_signed_quotient_exists x
  32. 0032apply gaussian_nearest_signed_quotient_exists
  33. 0033exact hN
  34. 0034cases hreal
  35. 0035cases hreal_witness
  36. 0036cases hreal_witness_witness
  37. 0037cases hreal_witness_witness_witness
  38. 0038cases hreal_witness_witness_witness_witness
  39. 0039cases hreal_witness_witness_witness_witness_witness
  40. 0040cases hreal_witness_witness_witness_witness_witness_right
  41. 0041have himaginary : exists qp qn ep en t. (((((((((((e) * (c))) + (((f) * (d))))) + (((((h) * (a))) + (((g) * (b))))))) + (x) * (qn)) + (en) = ((((((((e) * (d))) + (((f) * (c))))) + (((((h) * (b))) + (((g) * (a))))))) + (x) * (qp)) + (ep)) /\ ((((((ep) * (ep))) + (((en) * (en)))) = ((((t) * (t))) + (((((ep) * (en))) + (((en) * (ep))))))) /\ (exists ge_gap_division_imaginary_roundhalf_bound. ge_gap_division_imaginary_roundhalf_bound + (((t) + (t))) = (x)))))
  42. 0042specialize gaussian_nearest_signed_quotient_exists ((((((e) * (c))) + (((f) * (d))))) + (((((h) * (a))) + (((g) * (b))))))
  43. 0043specialize gaussian_nearest_signed_quotient_exists ((((((e) * (d))) + (((f) * (c))))) + (((((h) * (b))) + (((g) * (a))))))
  44. 0044specialize gaussian_nearest_signed_quotient_exists x
  45. 0045apply gaussian_nearest_signed_quotient_exists
  46. 0046exact hN
  47. 0047cases himaginary
  48. 0048cases himaginary_witness
  49. 0049cases himaginary_witness_witness
  50. 0050cases himaginary_witness_witness_witness
  51. 0051cases himaginary_witness_witness_witness_witness
  52. 0052cases himaginary_witness_witness_witness_witness_witness
  53. 0053cases himaginary_witness_witness_witness_witness_witness_right
  54. 0054have hremainder : exists M. (exists ge_real_square_constructed_remainder_norm ge_imaginary_square_constructed_remainder_norm. ((((((((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))) + (((((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6)))))))))))) = ((ge_real_square_constructed_remainder_norm) + (((((((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))) + (((((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))))))) /\ ((((((((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))) + (((((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2)))))))))))) = ((ge_imaginary_square_constructed_remainder_norm) + (((((((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))) + (((((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))))))) /\ ((M) = ge_real_square_constructed_remainder_norm + ge_imaginary_square_constructed_remainder_norm))))
  55. 0055specialize gaussian_signed_norm_exists ((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))
  56. 0056specialize gaussian_signed_norm_exists ((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))
  57. 0057specialize gaussian_signed_norm_exists ((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))
  58. 0058specialize gaussian_signed_norm_exists ((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))
  59. 0059apply gaussian_signed_norm_exists
  60. 0060cases hremainder
  61. 0061have herror_norm : exists ge_real_square_constructed_error_norm ge_imaginary_square_constructed_error_norm. ((((((x3) * (x3))) + (((x4) * (x4)))) = ((ge_real_square_constructed_error_norm) + (((((x3) * (x4))) + (((x4) * (x3))))))) /\ ((((((x8) * (x8))) + (((x9) * (x9)))) = ((ge_imaginary_square_constructed_error_norm) + (((((x8) * (x9))) + (((x9) * (x8))))))) /\ ((x5 * x5 + x10 * x10) = ge_real_square_constructed_error_norm + ge_imaginary_square_constructed_error_norm)))
  62. 0062exists x5 * x5
  63. 0063exists x10 * x10
  64. 0064split
  65. 0065exact hreal_witness_witness_witness_witness_witness_right_left
  66. 0066split
  67. 0067exact himaginary_witness_witness_witness_witness_witness_right_left
  68. 0068refl
  69. 0069have herror_equation : ((((((((((((e) * (a))) + (((f) * (b))))) + (((((h) * (d))) + (((g) * (c))))))) + (((x) * (x2))))) + (x4)) = ((x3) + (((((((((e) * (b))) + (((f) * (a))))) + (((((h) * (c))) + (((g) * (d))))))) + (((x) * (x1))))))) /\ (((((((((((e) * (c))) + (((f) * (d))))) + (((((h) * (a))) + (((g) * (b))))))) + (((x) * (x7))))) + (x9)) = ((x8) + (((((((((e) * (d))) + (((f) * (c))))) + (((((h) * (b))) + (((g) * (a))))))) + (((x) * (x6))))))))
  70. 0070split
  71. 0071trans ((((((((e) * (b))) + (((f) * (a))))) + (((((h) * (c))) + (((g) * (d))))))) + x * (x1)) + (x3)
  72. 0072exact hreal_witness_witness_witness_witness_witness_left
  73. 0073apply add_comm
  74. 0074trans ((((((((e) * (d))) + (((f) * (c))))) + (((((h) * (b))) + (((g) * (a))))))) + x * (x6)) + (x8)
  75. 0075exact himaginary_witness_witness_witness_witness_witness_left
  76. 0076apply add_comm
  77. 0077have hconjugate_error : ((((((((((e) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))) + (((f) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))))) + (((((h) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))) + (((g) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))))))) + (x4)) = ((x3) + (((((((e) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))) + (((f) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))))) + (((((h) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))) + (((g) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))))))))) /\ (((((((((e) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))) + (((f) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))))) + (((((h) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))) + (((g) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))))))) + (x9)) = ((x8) + (((((((e) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))) + (((f) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))))) + (((((h) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))) + (((g) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))))))))))
  78. 0078specialize gaussian_equal_transitive ((((((e) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))) + (((f) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))))) + (((((h) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))) + (((g) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))))))
  79. 0079specialize gaussian_equal_transitive ((((((e) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))) + (((f) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))))) + (((((h) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))) + (((g) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))))))
  80. 0080specialize gaussian_equal_transitive ((((((e) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))) + (((f) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))))) + (((((h) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))) + (((g) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))))))
  81. 0081specialize gaussian_equal_transitive ((((((e) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))) + (((f) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))))) + (((((h) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))) + (((g) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))))))
  82. 0082specialize gaussian_equal_transitive ((((((((e) * (a))) + (((f) * (b))))) + (((((h) * (d))) + (((g) * (c))))))) + (((x) * (x2))))
  83. 0083specialize gaussian_equal_transitive ((((((((e) * (b))) + (((f) * (a))))) + (((((h) * (c))) + (((g) * (d))))))) + (((x) * (x1))))
  84. 0084specialize gaussian_equal_transitive ((((((((e) * (c))) + (((f) * (d))))) + (((((h) * (a))) + (((g) * (b))))))) + (((x) * (x7))))
  85. 0085specialize gaussian_equal_transitive ((((((((e) * (d))) + (((f) * (c))))) + (((((h) * (b))) + (((g) * (a))))))) + (((x) * (x6))))
  86. 0086specialize gaussian_equal_transitive x3
  87. 0087specialize gaussian_equal_transitive x4
  88. 0088specialize gaussian_equal_transitive x8
  89. 0089specialize gaussian_equal_transitive x9
  90. 0090apply gaussian_equal_transitive
  91. 0091specialize gaussian_residual_conjugate_identity a
  92. 0092specialize gaussian_residual_conjugate_identity b
  93. 0093specialize gaussian_residual_conjugate_identity c
  94. 0094specialize gaussian_residual_conjugate_identity d
  95. 0095specialize gaussian_residual_conjugate_identity e
  96. 0096specialize gaussian_residual_conjugate_identity f
  97. 0097specialize gaussian_residual_conjugate_identity g
  98. 0098specialize gaussian_residual_conjugate_identity h
  99. 0099specialize gaussian_residual_conjugate_identity x1
  100. 0100specialize gaussian_residual_conjugate_identity x2
  101. 0101specialize gaussian_residual_conjugate_identity x6
  102. 0102specialize gaussian_residual_conjugate_identity x7
  103. 0103specialize gaussian_residual_conjugate_identity x
  104. 0104apply gaussian_residual_conjugate_identity
  105. 0105exact hdivisor_witness
  106. 0106exact herror_equation
  107. 0107have hproduct_norm : exists ge_real_square_actual_product_norm ge_imaginary_square_actual_product_norm. ((((((((((((e) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))) + (((f) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))))) + (((((h) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))) + (((g) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))))))) * (((((((e) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))) + (((f) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))))) + (((((h) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))) + (((g) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))))))))) + (((((((((e) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))) + (((f) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))))) + (((((h) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))) + (((g) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))))))) * (((((((e) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))) + (((f) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))))) + (((((h) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))) + (((g) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2)))))))))))))))))) = ((ge_real_square_actual_product_norm) + (((((((((((e) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))) + (((f) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))))) + (((((h) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))) + (((g) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))))))) * (((((((e) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))) + (((f) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))))) + (((((h) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))) + (((g) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))))))))) + (((((((((e) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))) + (((f) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))))) + (((((h) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))) + (((g) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))))))) * (((((((e) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))) + (((f) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))))) + (((((h) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))) + (((g) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))))))))))))) /\ ((((((((((((e) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))) + (((f) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))))) + (((((h) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))) + (((g) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))))))) * (((((((e) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))) + (((f) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))))) + (((((h) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))) + (((g) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))))))))) + (((((((((e) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))) + (((f) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))))) + (((((h) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))) + (((g) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))))))) * (((((((e) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))) + (((f) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))))) + (((((h) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))) + (((g) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7)))))))))))))))))) = ((ge_imaginary_square_actual_product_norm) + (((((((((((e) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))) + (((f) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))))) + (((((h) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))) + (((g) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))))))) * (((((((e) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))) + (((f) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))))) + (((((h) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))) + (((g) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))))))))) + (((((((((e) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))) + (((f) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))))) + (((((h) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))) + (((g) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))))))) * (((((((e) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))) + (((f) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))))) + (((((h) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))) + (((g) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))))))))))))) /\ ((x * x11) = ge_real_square_actual_product_norm + ge_imaginary_square_actual_product_norm)))
  108. 0108specialize gaussian_signed_norm_product e
  109. 0109specialize gaussian_signed_norm_product f
  110. 0110specialize gaussian_signed_norm_product h
  111. 0111specialize gaussian_signed_norm_product g
  112. 0112specialize gaussian_signed_norm_product ((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))
  113. 0113specialize gaussian_signed_norm_product ((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))
  114. 0114specialize gaussian_signed_norm_product ((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))
  115. 0115specialize gaussian_signed_norm_product ((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))
  116. 0116specialize gaussian_signed_norm_product x
  117. 0117specialize gaussian_signed_norm_product x11
  118. 0118apply gaussian_signed_norm_product
  119. 0119specialize gaussian_signed_norm_conjugate e
  120. 0120specialize gaussian_signed_norm_conjugate f
  121. 0121specialize gaussian_signed_norm_conjugate g
  122. 0122specialize gaussian_signed_norm_conjugate h
  123. 0123specialize gaussian_signed_norm_conjugate x
  124. 0124apply gaussian_signed_norm_conjugate
  125. 0125exact hdivisor_witness
  126. 0126exact hremainder_witness
  127. 0127have htransported_norm : exists ge_real_square_actual_error_product_norm ge_imaginary_square_actual_error_product_norm. ((((((x3) * (x3))) + (((x4) * (x4)))) = ((ge_real_square_actual_error_product_norm) + (((((x3) * (x4))) + (((x4) * (x3))))))) /\ ((((((x8) * (x8))) + (((x9) * (x9)))) = ((ge_imaginary_square_actual_error_product_norm) + (((((x8) * (x9))) + (((x9) * (x8))))))) /\ ((x * x11) = ge_real_square_actual_error_product_norm + ge_imaginary_square_actual_error_product_norm)))
  128. 0128specialize gaussian_signed_norm_integer_transport ((((((e) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))) + (((f) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))))) + (((((h) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))) + (((g) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))))))
  129. 0129specialize gaussian_signed_norm_integer_transport ((((((e) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))) + (((f) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))))) + (((((h) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))) + (((g) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))))))
  130. 0130specialize gaussian_signed_norm_integer_transport ((((((e) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))) + (((f) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))))) + (((((h) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))) + (((g) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))))))
  131. 0131specialize gaussian_signed_norm_integer_transport ((((((e) * (((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))))) + (((f) * (((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))))))) + (((((h) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))))) + (((g) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))))))))
  132. 0132specialize gaussian_signed_norm_integer_transport x3
  133. 0133specialize gaussian_signed_norm_integer_transport x4
  134. 0134specialize gaussian_signed_norm_integer_transport x8
  135. 0135specialize gaussian_signed_norm_integer_transport x9
  136. 0136specialize gaussian_signed_norm_integer_transport x * x11
  137. 0137apply gaussian_signed_norm_integer_transport
  138. 0138exact hconjugate_error
  139. 0139exact hproduct_norm
  140. 0140have hnorm_equation : x * x11 = x5 * x5 + x10 * x10
  141. 0141specialize gaussian_signed_norm_functional x3
  142. 0142specialize gaussian_signed_norm_functional x4
  143. 0143specialize gaussian_signed_norm_functional x8
  144. 0144specialize gaussian_signed_norm_functional x9
  145. 0145specialize gaussian_signed_norm_functional x * x11
  146. 0146specialize gaussian_signed_norm_functional x5 * x5 + x10 * x10
  147. 0147apply gaussian_signed_norm_functional
  148. 0148exact htransported_norm
  149. 0149exact herror_norm
  150. 0150have hstrict : exists ge_gap_actual_error_strict_bound. ge_gap_actual_error_strict_bound + S (x5 * x5 + x10 * x10) = (x * x)
  151. 0151specialize gaussian_two_half_squares_strict x
  152. 0152specialize gaussian_two_half_squares_strict x5
  153. 0153specialize gaussian_two_half_squares_strict x10
  154. 0154apply gaussian_two_half_squares_strict
  155. 0155exact hN
  156. 0156exact hreal_witness_witness_witness_witness_witness_right_right
  157. 0157exact himaginary_witness_witness_witness_witness_witness_right_right
  158. 0158exists x1
  159. 0159exists x2
  160. 0160exists x6
  161. 0161exists x7
  162. 0162exists ((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))))
  163. 0163exists ((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))))
  164. 0164exists ((c) + (((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))))
  165. 0165exists ((d) + (((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))))
  166. 0166exists x11
  167. 0167exists x
  168. 0168split
  169. 0169specialize gaussian_difference_reconstructs_dividend a
  170. 0170specialize gaussian_difference_reconstructs_dividend b
  171. 0171specialize gaussian_difference_reconstructs_dividend c
  172. 0172specialize gaussian_difference_reconstructs_dividend d
  173. 0173specialize gaussian_difference_reconstructs_dividend ((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x7))) + (((h) * (x6))))))
  174. 0174specialize gaussian_difference_reconstructs_dividend ((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x6))) + (((h) * (x7))))))
  175. 0175specialize gaussian_difference_reconstructs_dividend ((((((e) * (x6))) + (((f) * (x7))))) + (((((g) * (x1))) + (((h) * (x2))))))
  176. 0176specialize gaussian_difference_reconstructs_dividend ((((((e) * (x7))) + (((f) * (x6))))) + (((((g) * (x2))) + (((h) * (x1))))))
  177. 0177apply gaussian_difference_reconstructs_dividend
  178. 0178split
  179. 0179exact hremainder_witness
  180. 0180split
  181. 0181exact hdivisor_witness
  182. 0182specialize four_square_descent_norm_bound_forces_smaller_multiplier x
  183. 0183specialize four_square_descent_norm_bound_forces_smaller_multiplier x11
  184. 0184specialize four_square_descent_norm_bound_forces_smaller_multiplier x5 * x5 + x10 * x10
  185. 0185apply four_square_descent_norm_bound_forces_smaller_multiplier
  186. 0186exact hnorm_equation
  187. 0187exact hstrict