GI003A

gaussian_signed_euclidean_division_exists

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.

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. ¬(e = f ∧ g = h) → ∃ x. ∃ y. ∃ z. ∃ n. ∃ m. ∃ k. ∃ i. ∃ j. ∃ u. ∃ v. GaussianSignedDivisionRemainder(a,b,c,d,e,f,g,h,x,y,z,n,m,k,i,j,u,v)

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

Definition DAG

GaussianSignedNorm(ap,an,bp,bn,N) · 5RoundedSignedDivision(p,n,N,qp,qn,ep,en,t) · 2GaussianSignedDivisionRemainder(ap,an,bp,bn,cp,cn,dp,dn,qp,qn,up,un,rp,rn,sp,sn,U,V) · 1Lt(a,b) · 1

Actual proof prerequisites

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_dividendfour_square_descent_norm_bound_forces_smaller_multiplier · checked external prerequisiteadd_comm · checked external prerequisite
Original expanded first-order 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))))))

Complete tactic proof in conservative notation

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

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.

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 (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
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 : ∃ N. GaussianSignedNorm(e,f,g,h,N)Definitions: GaussianSignedNorm(e,f,g,h,N)Original native command in the exact edition
  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 : ∃ qp. ∃ qn. ∃ ep. ∃ en. ∃ t. RoundedSignedDivision(e · a + f · b + (h · d + g · c),e · b + f · a + (h · c + g · d),x,qp,qn,ep,en,t)Definitions: RoundedSignedDivision(e · a + f · b + (h · d + g · c),e · b + f · a + (h · c + g · d),x,qp,qn,ep,en,t)Original native command in the exact edition
  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 : ∃ qp. ∃ qn. ∃ ep. ∃ en. ∃ t. RoundedSignedDivision(e · c + f · d + (h · a + g · b),e · d + f · c + (h · b + g · a),x,qp,qn,ep,en,t)Definitions: RoundedSignedDivision(e · c + f · d + (h · a + g · b),e · d + f · c + (h · b + g · a),x,qp,qn,ep,en,t)Original native command in the exact edition
  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(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)Original native command in the exact edition
  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 : GaussianSignedNorm(x3,x4,x8,x9,x5 · x5 + x10 · x10)Definitions: GaussianSignedNorm(x3,x4,x8,x9,x5 · x5 + x10 · x10)Original native command in the exact edition
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(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)Original native command in the exact edition
  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 : GaussianSignedNorm(x3,x4,x8,x9,x · x11)Definitions: GaussianSignedNorm(x3,x4,x8,x9,x · x11)Original native command in the exact edition
  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 : Lt(x5 · x5 + x10 · x10,x · x)Definitions: Lt(x5 · x5 + x10 · x10,x · x)Original native command in the exact edition
  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 defined 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 : ∃ N. GaussianSignedNorm(e,f,g,h,N)
  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 : ∃ qp. ∃ qn. ∃ ep. ∃ en. ∃ t. RoundedSignedDivision(e · a + f · b + (h · d + g · c),e · b + f · a + (h · c + g · d),x,qp,qn,ep,en,t)
  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 : ∃ qp. ∃ qn. ∃ ep. ∃ en. ∃ t. RoundedSignedDivision(e · c + f · d + (h · a + g · b),e · d + f · c + (h · b + g · a),x,qp,qn,ep,en,t)
  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 : ∃ 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)
  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 : GaussianSignedNorm(x3,x4,x8,x9,x5 · x5 + x10 · x10)
  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 : 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)
  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 : GaussianSignedNorm(x3,x4,x8,x9,x · x11)
  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 : Lt(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