EI0033

eisenstein_signed_euclidean_division_exists

Construct a genuine Eisenstein quotient and remainder for every nonzero signed divisor, with exact a=bq+r and strict actual norm decrease; neither quotient, norm existence, nor a bound is supplied as a premise.

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.

A floor quotient in the fundamental parallelogram already gives the required strict norm decrease; global nearest-point optimality is not asserted. The shared carrier is identical to the Gaussian carrier, but the multiplication law and norm are different. Eisenstein gcd, factorization, and prime classification remain 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. EisensteinSignedDivisionRemainder(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

SignedFloor(p,n,m,q,t,r) · 2EisensteinCoordinateNorm(ap,an,bp,bn,n) · 5EisensteinCoordinateProduct(ap,an,bp,bn,cp,cn,dp,dn,rp,rn,sp,sn) · 1EisensteinSignedDivisionRemainder(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

eisenstein_coordinate_norm_existseisenstein_coordinate_norm_nonzerosigned_integer_floor_exists · checked external prerequisiteeisenstein_natural_norm_existseisenstein_natural_norm_coordinatesgaussian_equal_transitive · checked external prerequisiteeisenstein_residual_conjugate_identityeisenstein_coordinate_norm_producteisenstein_coordinate_norm_conjugateeisenstein_coordinate_norm_transporteisenstein_coordinate_norm_functionaleisenstein_parallelogram_norm_strictgaussian_difference_reconstructs_dividend · checked external prerequisitefour_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))))))) + (((((g) * (un))) + (((h) * (up))))))) + (sp))) + (d)) = ((c) + (((((((((((e) * (un))) + (((f) * (up))))) + (((((g) * (qn))) + (((h) * (qp))))))) + (((((g) * (up))) + (((h) * (un))))))) + (sn))))))) /\ ((((((((((rp) * (rp))) + (((rn) * (rn))))) + (((((sp) * (sp))) + (((sn) * (sn))))))) + (((((rp) * (sn))) + (((rn) * (sp)))))) = ((((((((((rp) * (rn))) + (((rn) * (rp))))) + (((((sp) * (sn))) + (((sn) * (sp))))))) + (((((rp) * (sp))) + (((rn) * (sn))))))) + (U))) /\ ((((((((((e) * (e))) + (((f) * (f))))) + (((((g) * (g))) + (((h) * (h))))))) + (((((e) * (h))) + (((f) * (g)))))) = ((((((((((e) * (f))) + (((f) * (e))))) + (((((g) * (h))) + (((h) * (g))))))) + (((((e) * (g))) + (((f) * (h))))))) + (V))) /\ (exists ee_gap_full_signed_division. ee_gap_full_signed_division + S (U) = (V))))))

Complete tactic proof in conservative notation

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

192 script commands · 44 reading checkpoints · 13 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 (10)
eisenstein coordinate norm existseisenstein coordinate norm nonzeroeisenstein natural norm existseisenstein natural norm coordinateseisenstein residual conjugate identityeisenstein coordinate norm producteisenstein coordinate norm conjugateeisenstein coordinate norm transporteisenstein coordinate norm functionaleisenstein parallelogram norm strict
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 eisenstein coordinate norm exists.

  1. L10
    have hdivisor : ∃ N. EisensteinCoordinateNorm(e,f,g,h,N)Definitions: EisensteinCoordinateNorm(e,f,g,h,N)Original native command in the exact edition
  2. L11
    specialize eisenstein_coordinate_norm_exists e
  3. L12
    specialize eisenstein_coordinate_norm_exists f
  4. L13
    specialize eisenstein_coordinate_norm_exists g
  5. L14
    specialize eisenstein_coordinate_norm_exists h
  6. L15
    apply eisenstein_coordinate_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 eisenstein coordinate norm nonzero.

  1. L17
    have hN : ~(x = 0)
  2. L18
    intro hzero
  3. L19
    specialize eisenstein_coordinate_norm_nonzero e
  4. L20
    specialize eisenstein_coordinate_norm_nonzero f
  5. L21
    specialize eisenstein_coordinate_norm_nonzero g
  6. L22
    specialize eisenstein_coordinate_norm_nonzero h
  7. L23
    specialize eisenstein_coordinate_norm_nonzero x
  8. L24
    apply eisenstein_coordinate_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 signed integer floor exists.

  1. L28
    have hreal : ∃ qp. ∃ qn. ∃ r. SignedFloor((e + h) · a + (f + g) · b + (h · d + g · c),(e + h) · b + (f + g) · a + (h · c + g · d),x,qp,qn,r)Definitions: SignedFloor((e + h) · a + (f + g) · b + (h · d + g · c),(e + h) · b + (f + g) · a + (h · c + g · d),x,qp,qn,r)Original native command in the exact edition
  2. L29
    specialize signed_integer_floor_exists ((((((((e) + (h))) * (a))) + (((((f) + (g))) * (b))))) + (((((h) * (d))) + (((g) * (c))))))
  3. L30
    specialize signed_integer_floor_exists ((((((((e) + (h))) * (b))) + (((((f) + (g))) * (a))))) + (((((h) * (c))) + (((g) * (d))))))
  4. L31
    specialize signed_integer_floor_exists x
  5. L32
    apply signed_integer_floor_exists
  6. L33
    exact hN
07Separate the logical casesL34–37

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
08Establish himaginaryL38–43

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

  1. L38
    have himaginary : ∃ qp. ∃ qn. ∃ r. SignedFloor((e + h) · c + (f + g) · d + (h · a + g · b) + (h · d + g · c),(e + h) · d + (f + g) · c + (h · b + g · a) + (h · c + g · d),x,qp,qn,r)Definitions: SignedFloor((e + h) · c + (f + g) · d + (h · a + g · b) + (h · d + g · c),(e + h) · d + (f + g) · c + (h · b + g · a) + (h · c + g · d),x,qp,qn,r)Original native command in the exact edition
  2. L39
    specialize signed_integer_floor_exists ((((((((((e) + (h))) * (c))) + (((((f) + (g))) * (d))))) + (((((h) * (a))) + (((g) * (b))))))) + (((((h) * (d))) + (((g) * (c))))))
  3. L40
    specialize signed_integer_floor_exists ((((((((((e) + (h))) * (d))) + (((((f) + (g))) * (c))))) + (((((h) * (b))) + (((g) * (a))))))) + (((((h) * (c))) + (((g) * (d))))))
  4. L41
    specialize signed_integer_floor_exists x
  5. L42
    apply signed_integer_floor_exists
  6. L43
    exact hN
09Separate the logical casesL44–47

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

  1. L44
    cases himaginary
  2. L45
    cases himaginary_witness
  3. L46
    cases himaginary_witness_witness
  4. L47
    cases himaginary_witness_witness_witness
10Establish hremainderL48–53

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

  1. L48
    have hremainder : ∃ M. EisensteinCoordinateNorm(a + (e · x2 + f · x1 + (g · x4 + h · x5)),b + (e · x1 + f · x2 + (g · x5 + h · x4)),c + (e · x5 + f · x4 + (g · x2 + h · x1) + (g · x4 + h · x5)),d + (e · x4 + f · x5 + (g · x1 + h · x2) + (g · x5 + h · x4)),M)Definitions: EisensteinCoordinateNorm(a + (e · x2 + f · x1 + (g · x4 + h · x5)),b + (e · x1 + f · x2 + (g · x5 + h · x4)),c + (e · x5 + f · x4 + (g · x2 + h · x1) + (g · x4 + h · x5)),d + (e · x4 + f · x5 + (g · x1 + h · x2) + (g · x5 + h · x4)),M)Original native command in the exact edition
  2. L49
    specialize eisenstein_coordinate_norm_exists ((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x4))) + (((h) * (x5))))))))
  3. L50
    specialize eisenstein_coordinate_norm_exists ((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x5))) + (((h) * (x4))))))))
  4. L51
    specialize eisenstein_coordinate_norm_exists ((c) + (((((((((e) * (x5))) + (((f) * (x4))))) + (((((g) * (x2))) + (((h) * (x1))))))) + (((((g) * (x4))) + (((h) * (x5))))))))
  5. L52
    specialize eisenstein_coordinate_norm_exists ((d) + (((((((((e) * (x4))) + (((f) * (x5))))) + (((((g) * (x1))) + (((h) * (x2))))))) + (((((g) * (x5))) + (((h) * (x4))))))))
  6. L53
    apply eisenstein_coordinate_norm_exists
11Separate the logical casesL54–54

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

  1. L54
    cases hremainder
12Establish herrorL55–58

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

  1. L55
    have herror : exists M. ((((x3) * (x3)) + ((x6) * (x6))) = (((x3) * (x6)) + (M)))
  2. L56
    specialize eisenstein_natural_norm_exists x3
  3. L57
    specialize eisenstein_natural_norm_exists x6
  4. L58
    apply eisenstein_natural_norm_exists
13Separate the logical casesL59–59

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

  1. L59
    cases herror
14Establish herrornormL60–65

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein natural norm coordinates.

  1. L60
    have herrornorm : EisensteinCoordinateNorm(x3,0,x6,0,x8)Definitions: EisensteinCoordinateNorm(x3,0,x6,0,x8)Original native command in the exact edition
  2. L61
    specialize eisenstein_natural_norm_coordinates x3
  3. L62
    specialize eisenstein_natural_norm_coordinates x6
  4. L63
    specialize eisenstein_natural_norm_coordinates x8
  5. L64
    apply eisenstein_natural_norm_coordinates
  6. L65
    exact herror_witness
15Establish herror_equationL66–66

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

  1. L66
    have herror_equation · expand full local formula (609 characters)have herror_equation : ((((((((((((((e) + (h))) * (a))) + (((((f) + (g))) * (b))))) + (((((h) * (d))) + (((g) * (c))))))) + (((x) * (x2))))) + (0)) = ((x3) + (((((((((((e) + (h))) * (b))) + (((((f) + (g))) * (a))))) + (((((h) * (c))) + (((g) * (d))))))) + (((x) * (x1))))))) /\ (((((((((((((((e) + (h))) * (c))) + (((((f) + (g))) * (d))))) + (((((h) * (a))) + (((g) * (b))))))) + (((((h) * (d))) + (((g) * (c))))))) + (((x) * (x5))))) + (0)) = ((x6) + (((((((((((((e) + (h))) * (d))) + (((((f) + (g))) * (c))))) + (((((h) * (b))) + (((g) * (a))))))) + (((((h) * (c))) + (((g) * (d))))))) + (((x) * (x4))))))))
16Separate the logical casesL67–67

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

  1. L67
    split
17Calculate and transport equalitiesL68–68

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

  1. L68
    trans ((((((((((e) + (h))) * (a))) + (((((f) + (g))) * (b))))) + (((((h) * (d))) + (((g) * (c))))))) + (((x) * (x2))))
18Use earlier factsL69–69

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

  1. L69
    apply PA3
19Calculate and transport equalitiesL70–70

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

  1. L70
    trans ((((((((((((e) + (h))) * (b))) + (((((f) + (g))) * (a))))) + (((((h) * (c))) + (((g) * (d))))))) + (((x) * (x1))))) + (x3))
20Use earlier factsL71–72

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

  1. L71
    exact hreal_witness_witness_witness_left
  2. L72
    apply add_comm
21Calculate and transport equalitiesL73–73

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

  1. L73
    trans ((((((((((((e) + (h))) * (c))) + (((((f) + (g))) * (d))))) + (((((h) * (a))) + (((g) * (b))))))) + (((((h) * (d))) + (((g) * (c))))))) + (((x) * (x5))))
22Use earlier factsL74–74

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

  1. L74
    apply PA3
23Calculate and transport equalitiesL75–75

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

  1. L75
    trans ((((((((((((((e) + (h))) * (d))) + (((((f) + (g))) * (c))))) + (((((h) * (b))) + (((g) * (a))))))) + (((((h) * (c))) + (((g) * (d))))))) + (((x) * (x4))))) + (x6))
24Use earlier factsL76–77

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

  1. L76
    exact himaginary_witness_witness_witness_left
  2. L77
    apply add_comm
25Establish hconjugate_errorL78–87

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

  1. L78
    have hconjugate_error : EisensteinCoordinateProduct(e + h,f + g,h,g,a + (e · x2 + f · x1 + (g · x4 + h · x5)),b + (e · x1 + f · x2 + (g · x5 + h · x4)),c + (e · x5 + f · x4 + (g · x2 + h · x1) + (g · x4 + h · x5)),d + (e · x4 + f · x5 + (g · x1 + h · x2) + (g · x5 + h · x4)),x3,0,x6,0)Definitions: EisensteinCoordinateProduct(e + h,f + g,h,g,a + (e · x2 + f · x1 + (g · x4 + h · x5)),b + (e · x1 + f · x2 + (g · x5 + h · x4)),c + (e · x5 + f · x4 + (g · x2 + h · x1) + (g · x4 + h · x5)),d + (e · x4 + f · x5 + (g · x1 + h · x2) + (g · x5 + h · x4)),x3,0,x6,0)Original native command in the exact edition
  2. L79
    specialize gaussian_equal_transitive ((((((((e) + (h))) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x4))) + (((h) * (x5))))))))))) + (((((f) + (g))) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x5))) + (((h) * (x4))))))))))))) + (((((h) * (((d) + (((((((((e) * (x4))) + (((f) * (x5))))) + (((((g) * (x1))) + (((h) * (x2))))))) + (((((g) * (x5))) + (((h) * (x4))))))))))) + (((g) * (((c) + (((((((((e) * (x5))) + (((f) * (x4))))) + (((((g) * (x2))) + (((h) * (x1))))))) + (((((g) * (x4))) + (((h) * (x5))))))))))))))
  3. L80
    specialize gaussian_equal_transitive ((((((((e) + (h))) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x5))) + (((h) * (x4))))))))))) + (((((f) + (g))) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x4))) + (((h) * (x5))))))))))))) + (((((h) * (((c) + (((((((((e) * (x5))) + (((f) * (x4))))) + (((((g) * (x2))) + (((h) * (x1))))))) + (((((g) * (x4))) + (((h) * (x5))))))))))) + (((g) * (((d) + (((((((((e) * (x4))) + (((f) * (x5))))) + (((((g) * (x1))) + (((h) * (x2))))))) + (((((g) * (x5))) + (((h) * (x4))))))))))))))
  4. L81
    specialize gaussian_equal_transitive ((((((((((e) + (h))) * (((c) + (((((((((e) * (x5))) + (((f) * (x4))))) + ( · expand full local formula (840 characters)specialize gaussian_equal_transitive ((((((((((e) + (h))) * (((c) + (((((((((e) * (x5))) + (((f) * (x4))))) + (((((g) * (x2))) + (((h) * (x1))))))) + (((((g) * (x4))) + (((h) * (x5))))))))))) + (((((f) + (g))) * (((d) + (((((((((e) * (x4))) + (((f) * (x5))))) + (((((g) * (x1))) + (((h) * (x2))))))) + (((((g) * (x5))) + (((h) * (x4))))))))))))) + (((((h) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x4))) + (((h) * (x5))))))))))) + (((g) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x5))) + (((h) * (x4))))))))))))))) + (((((h) * (((d) + (((((((((e) * (x4))) + (((f) * (x5))))) + (((((g) * (x1))) + (((h) * (x2))))))) + (((((g) * (x5))) + (((h) * (x4))))))))))) + (((g) * (((c) + (((((((((e) * (x5))) + (((f) * (x4))))) + (((((g) * (x2))) + (((h) * (x1))))))) + (((((g) * (x4))) + (((h) * (x5))))))))))))))
  5. L82
    specialize gaussian_equal_transitive ((((((((((e) + (h))) * (((d) + (((((((((e) * (x4))) + (((f) * (x5))))) + ( · expand full local formula (840 characters)specialize gaussian_equal_transitive ((((((((((e) + (h))) * (((d) + (((((((((e) * (x4))) + (((f) * (x5))))) + (((((g) * (x1))) + (((h) * (x2))))))) + (((((g) * (x5))) + (((h) * (x4))))))))))) + (((((f) + (g))) * (((c) + (((((((((e) * (x5))) + (((f) * (x4))))) + (((((g) * (x2))) + (((h) * (x1))))))) + (((((g) * (x4))) + (((h) * (x5))))))))))))) + (((((h) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x5))) + (((h) * (x4))))))))))) + (((g) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x4))) + (((h) * (x5))))))))))))))) + (((((h) * (((c) + (((((((((e) * (x5))) + (((f) * (x4))))) + (((((g) * (x2))) + (((h) * (x1))))))) + (((((g) * (x4))) + (((h) * (x5))))))))))) + (((g) * (((d) + (((((((((e) * (x4))) + (((f) * (x5))))) + (((((g) * (x1))) + (((h) * (x2))))))) + (((((g) * (x5))) + (((h) * (x4))))))))))))))
  6. L83
    specialize gaussian_equal_transitive ((((((((((e) + (h))) * (a))) + (((((f) + (g))) * (b))))) + (((((h) * (d))) + (((g) * (c))))))) + (((x) * (x2))))
  7. L84
    specialize gaussian_equal_transitive ((((((((((e) + (h))) * (b))) + (((((f) + (g))) * (a))))) + (((((h) * (c))) + (((g) * (d))))))) + (((x) * (x1))))
  8. L85
    specialize gaussian_equal_transitive ((((((((((((e) + (h))) * (c))) + (((((f) + (g))) * (d))))) + (((((h) * (a))) + (((g) * (b))))))) + (((((h) * (d))) + (((g) * (c))))))) + (((x) * (x5))))
  9. L86
    specialize gaussian_equal_transitive ((((((((((((e) + (h))) * (d))) + (((((f) + (g))) * (c))))) + (((((h) * (b))) + (((g) * (a))))))) + (((((h) * (c))) + (((g) * (d))))))) + (((x) * (x4))))
  10. L87
    specialize gaussian_equal_transitive x3
26Use earlier factsL88–97

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

  1. L88
    specialize gaussian_equal_transitive 0
  2. L89
    specialize gaussian_equal_transitive x6
  3. L90
    specialize gaussian_equal_transitive 0
  4. L91
    apply gaussian_equal_transitive
  5. L92
    specialize eisenstein_residual_conjugate_identity a
  6. L93
    specialize eisenstein_residual_conjugate_identity b
  7. L94
    specialize eisenstein_residual_conjugate_identity c
  8. L95
    specialize eisenstein_residual_conjugate_identity d
  9. L96
    specialize eisenstein_residual_conjugate_identity e
  10. L97
    specialize eisenstein_residual_conjugate_identity f
27Use earlier factsL98–107

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

  1. L98
    specialize eisenstein_residual_conjugate_identity g
  2. L99
    specialize eisenstein_residual_conjugate_identity h
  3. L100
    specialize eisenstein_residual_conjugate_identity x1
  4. L101
    specialize eisenstein_residual_conjugate_identity x2
  5. L102
    specialize eisenstein_residual_conjugate_identity x4
  6. L103
    specialize eisenstein_residual_conjugate_identity x5
  7. L104
    specialize eisenstein_residual_conjugate_identity x
  8. L105
    apply eisenstein_residual_conjugate_identity
  9. L106
    exact hdivisor_witness
  10. L107
    exact herror_equation
28Establish hproduct_normL108–117

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

  1. L108
    have hproduct_norm · expand full local formula (1,345 characters)have hproduct_norm : EisensteinCoordinateNorm((e + h) · (a + (e · x2 + f · x1 + (g · x4 + h · x5))) + (f + g) · (b + (e · x1 + f · x2 + (g · x5 + h · x4))) + (h · (d + (e · x4 + f · x5 + (g · x1 + h · x2) + (g · x5 + h · x4))) + g · (c + (e · x5 + f · x4 + (g · x2 + h · x1) + (g · x4 + h · x5)))),(e + h) · (b + (e · x1 + f · x2 + (g · x5 + h · x4))) + (f + g) · (a + (e · x2 + f · x1 + (g · x4 + h · x5))) + (h · (c + (e · x5 + f · x4 + (g · x2 + h · x1) + (g · x4 + h · x5))) + g · (d + (e · x4 + f · x5 + (g · x1 + h · x2) + (g · x5 + h · x4)))),(e + h) · (c + (e · x5 + f · x4 + (g · x2 + h · x1) + (g · x4 + h · x5))) + (f + g) · (d + (e · x4 + f · x5 + (g · x1 + h · x2) + (g · x5 + h · x4))) + (h · (a + (e · x2 + f · x1 + (g · x4 + h · x5))) + g · (b + (e · x1 + f · x2 + (g · x5 + h · x4)))) + (h · (d + (e · x4 + f · x5 + (g · x1 + h · x2) + (g · x5 + h · x4))) + g · (c + (e · x5 + f · x4 + (g · x2 + h · x1) + (g · x4 + h · x5)))),(e + h) · (d + (e · x4 + f · x5 + (g · x1 + h · x2) + (g · x5 + h · x4))) + (f + g) · (c + (e · x5 + f · x4 + (g · x2 + h · x1) + (g · x4 + h · x5))) + (h · (b + (e · x1 + f · x2 + (g · x5 + h · x4))) + g · (a + (e · x2 + f · x1 + (g · x4 + h · x5)))) + (h · (c + (e · x5 + f · x4 + (g · x2 + h · x1) + (g · x4 + h · x5))) + g · (d + (e · x4 + f · x5 + (g · x1 + h · x2) + (g · x5 + h · x4)))),x · x7)
    Definitions: EisensteinCoordinateNorm((e + h) · (a + (e · x2 + f · x1 + (g · x4 + h · x5))) + (f + g) · (b + (e · x1 + f · x2 + (g · x5 + h · x4))) + (h · (d + (e · x4 + f · x5 + (g · x1 + h · x2) + (g · x5 + h · x4))) + g · (c + (e · x5 + f · x4 + (g · x2 + h · x1) + (g · x4 + h · x5)))),(e + h) · (b + (e · x1 + f · x2 + (g · x5 + h · x4))) + (f + g) · (a + (e · x2 + f · x1 + (g · x4 + h · x5))) + (h · (c + (e · x5 + f · x4 + (g · x2 + h · x1) + (g · x4 + h · x5))) + g · (d + (e · x4 + f · x5 + (g · x1 + h · x2) + (g · x5 + h · x4)))),(e + h) · (c + (e · x5 + f · x4 + (g · x2 + h · x1) + (g · x4 + h · x5))) + (f + g) · (d + (e · x4 + f · x5 + (g · x1 + h · x2) + (g · x5 + h · x4))) + (h · (a + (e · x2 + f · x1 + (g · x4 + h · x5))) + g · (b + (e · x1 + f · x2 + (g · x5 + h · x4)))) + (h · (d + (e · x4 + f · x5 + (g · x1 + h · x2) + (g · x5 + h · x4))) + g · (c + (e · x5 + f · x4 + (g · x2 + h · x1) + (g · x4 + h · x5)))),(e + h) · (d + (e · x4 + f · x5 + (g · x1 + h · x2) + (g · x5 + h · x4))) + (f + g) · (c + (e · x5 + f · x4 + (g · x2 + h · x1) + (g · x4 + h · x5))) + (h · (b + (e · x1 + f · x2 + (g · x5 + h · x4))) + g · (a + (e · x2 + f · x1 + (g · x4 + h · x5)))) + (h · (c + (e · x5 + f · x4 + (g · x2 + h · x1) + (g · x4 + h · x5))) + g · (d + (e · x4 + f · x5 + (g · x1 + h · x2) + (g · x5 + h · x4)))),x · x7)Original native command in the exact edition
  2. L109
    specialize eisenstein_coordinate_norm_product ((e) + (h))
  3. L110
    specialize eisenstein_coordinate_norm_product ((f) + (g))
  4. L111
    specialize eisenstein_coordinate_norm_product h
  5. L112
    specialize eisenstein_coordinate_norm_product g
  6. L113
    specialize eisenstein_coordinate_norm_product ((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x4))) + (((h) * (x5))))))))
  7. L114
    specialize eisenstein_coordinate_norm_product ((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x5))) + (((h) * (x4))))))))
  8. L115
    specialize eisenstein_coordinate_norm_product ((c) + (((((((((e) * (x5))) + (((f) * (x4))))) + (((((g) * (x2))) + (((h) * (x1))))))) + (((((g) * (x4))) + (((h) * (x5))))))))
  9. L116
    specialize eisenstein_coordinate_norm_product ((d) + (((((((((e) * (x4))) + (((f) * (x5))))) + (((((g) * (x1))) + (((h) * (x2))))))) + (((((g) * (x5))) + (((h) * (x4))))))))
  10. L117
    specialize eisenstein_coordinate_norm_product x
29Use earlier factsL118–127

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

  1. L118
    specialize eisenstein_coordinate_norm_product x7
  2. L119
    apply eisenstein_coordinate_norm_product
  3. L120
    specialize eisenstein_coordinate_norm_conjugate e
  4. L121
    specialize eisenstein_coordinate_norm_conjugate f
  5. L122
    specialize eisenstein_coordinate_norm_conjugate g
  6. L123
    specialize eisenstein_coordinate_norm_conjugate h
  7. L124
    specialize eisenstein_coordinate_norm_conjugate x
  8. L125
    apply eisenstein_coordinate_norm_conjugate
  9. L126
    exact hdivisor_witness
  10. L127
    exact hremainder_witness
30Establish htransportedL128–137

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

  1. L128
    have htransported : EisensteinCoordinateNorm(x3,0,x6,0,x · x7)Definitions: EisensteinCoordinateNorm(x3,0,x6,0,x · x7)Original native command in the exact edition
  2. L129
    specialize eisenstein_coordinate_norm_transport ((((((((e) + (h))) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x4))) + (((h) * (x5))))))))))) + (((((f) + (g))) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x5))) + (((h) * (x4))))))))))))) + (((((h) * (((d) + (((((((((e) * (x4))) + (((f) * (x5))))) + (((((g) * (x1))) + (((h) * (x2))))))) + (((((g) * (x5))) + (((h) * (x4))))))))))) + (((g) * (((c) + (((((((((e) * (x5))) + (((f) * (x4))))) + (((((g) * (x2))) + (((h) * (x1))))))) + (((((g) * (x4))) + (((h) * (x5))))))))))))))
  3. L130
    specialize eisenstein_coordinate_norm_transport ((((((((e) + (h))) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x5))) + (((h) * (x4))))))))))) + (((((f) + (g))) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x4))) + (((h) * (x5))))))))))))) + (((((h) * (((c) + (((((((((e) * (x5))) + (((f) * (x4))))) + (((((g) * (x2))) + (((h) * (x1))))))) + (((((g) * (x4))) + (((h) * (x5))))))))))) + (((g) * (((d) + (((((((((e) * (x4))) + (((f) * (x5))))) + (((((g) * (x1))) + (((h) * (x2))))))) + (((((g) * (x5))) + (((h) * (x4))))))))))))))
  4. L131
    specialize eisenstein_coordinate_norm_transport ((((((((((e) + (h))) * (((c) + (((((((((e) * (x5))) + (((f) * ( · expand full local formula (851 characters)specialize eisenstein_coordinate_norm_transport ((((((((((e) + (h))) * (((c) + (((((((((e) * (x5))) + (((f) * (x4))))) + (((((g) * (x2))) + (((h) * (x1))))))) + (((((g) * (x4))) + (((h) * (x5))))))))))) + (((((f) + (g))) * (((d) + (((((((((e) * (x4))) + (((f) * (x5))))) + (((((g) * (x1))) + (((h) * (x2))))))) + (((((g) * (x5))) + (((h) * (x4))))))))))))) + (((((h) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x4))) + (((h) * (x5))))))))))) + (((g) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x5))) + (((h) * (x4))))))))))))))) + (((((h) * (((d) + (((((((((e) * (x4))) + (((f) * (x5))))) + (((((g) * (x1))) + (((h) * (x2))))))) + (((((g) * (x5))) + (((h) * (x4))))))))))) + (((g) * (((c) + (((((((((e) * (x5))) + (((f) * (x4))))) + (((((g) * (x2))) + (((h) * (x1))))))) + (((((g) * (x4))) + (((h) * (x5))))))))))))))
  5. L132
    specialize eisenstein_coordinate_norm_transport ((((((((((e) + (h))) * (((d) + (((((((((e) * (x4))) + (((f) * ( · expand full local formula (851 characters)specialize eisenstein_coordinate_norm_transport ((((((((((e) + (h))) * (((d) + (((((((((e) * (x4))) + (((f) * (x5))))) + (((((g) * (x1))) + (((h) * (x2))))))) + (((((g) * (x5))) + (((h) * (x4))))))))))) + (((((f) + (g))) * (((c) + (((((((((e) * (x5))) + (((f) * (x4))))) + (((((g) * (x2))) + (((h) * (x1))))))) + (((((g) * (x4))) + (((h) * (x5))))))))))))) + (((((h) * (((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x5))) + (((h) * (x4))))))))))) + (((g) * (((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x4))) + (((h) * (x5))))))))))))))) + (((((h) * (((c) + (((((((((e) * (x5))) + (((f) * (x4))))) + (((((g) * (x2))) + (((h) * (x1))))))) + (((((g) * (x4))) + (((h) * (x5))))))))))) + (((g) * (((d) + (((((((((e) * (x4))) + (((f) * (x5))))) + (((((g) * (x1))) + (((h) * (x2))))))) + (((((g) * (x5))) + (((h) * (x4))))))))))))))
  6. L133
    specialize eisenstein_coordinate_norm_transport x3
  7. L134
    specialize eisenstein_coordinate_norm_transport 0
  8. L135
    specialize eisenstein_coordinate_norm_transport x6
  9. L136
    specialize eisenstein_coordinate_norm_transport 0
  10. L137
    specialize eisenstein_coordinate_norm_transport (x * x7)
31Use earlier factsL138–138

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

  1. L138
    apply eisenstein_coordinate_norm_transport
32Separate the logical casesL139–139

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

  1. L139
    cases hconjugate_error
33Use earlier factsL140–140

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

  1. L140
    exact hconjugate_error_left
34Separate the logical casesL141–141

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

  1. L141
    cases hconjugate_error
35Use earlier factsL142–143

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

  1. L142
    exact hconjugate_error_right
  2. L143
    exact hproduct_norm
36Establish hnormequationL144–153

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

  1. L144
    have hnormequation : x * x7 = x8
  2. L145
    specialize eisenstein_coordinate_norm_functional x3
  3. L146
    specialize eisenstein_coordinate_norm_functional 0
  4. L147
    specialize eisenstein_coordinate_norm_functional x6
  5. L148
    specialize eisenstein_coordinate_norm_functional 0
  6. L149
    specialize eisenstein_coordinate_norm_functional (x * x7)
  7. L150
    specialize eisenstein_coordinate_norm_functional x8
  8. L151
    apply eisenstein_coordinate_norm_functional
  9. L152
    exact htransported
  10. L153
    exact herrornorm
37Establish hstrictL154–162

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein parallelogram norm strict.

  1. L154
    have hstrict : Lt(x8,x · x)Definitions: Lt(x8,x · x)Original native command in the exact edition
  2. L155
    specialize eisenstein_parallelogram_norm_strict x3
  3. L156
    specialize eisenstein_parallelogram_norm_strict x6
  4. L157
    specialize eisenstein_parallelogram_norm_strict x
  5. L158
    specialize eisenstein_parallelogram_norm_strict x8
  6. L159
    apply eisenstein_parallelogram_norm_strict
  7. L160
    exact hreal_witness_witness_witness_right
  8. L161
    exact himaginary_witness_witness_witness_right
  9. L162
    exact herror_witness
38Construct an explicit witnessL163–172

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

  1. L163
    exists x1
  2. L164
    exists x2
  3. L165
    exists x4
  4. L166
    exists x5
  5. L167
    exists ((a) + (((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x4))) + (((h) * (x5))))))))
  6. L168
    exists ((b) + (((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x5))) + (((h) * (x4))))))))
  7. L169
    exists ((c) + (((((((((e) * (x5))) + (((f) * (x4))))) + (((((g) * (x2))) + (((h) * (x1))))))) + (((((g) * (x4))) + (((h) * (x5))))))))
  8. L170
    exists ((d) + (((((((((e) * (x4))) + (((f) * (x5))))) + (((((g) * (x1))) + (((h) * (x2))))))) + (((((g) * (x5))) + (((h) * (x4))))))))
  9. L171
    exists x7
  10. L172
    exists x
39Separate the logical casesL173–173

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

  1. L173
    split
40Use earlier factsL174–182

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

  1. L174
    specialize gaussian_difference_reconstructs_dividend a
  2. L175
    specialize gaussian_difference_reconstructs_dividend b
  3. L176
    specialize gaussian_difference_reconstructs_dividend c
  4. L177
    specialize gaussian_difference_reconstructs_dividend d
  5. L178
    specialize gaussian_difference_reconstructs_dividend ((((((e) * (x1))) + (((f) * (x2))))) + (((((g) * (x5))) + (((h) * (x4))))))
  6. L179
    specialize gaussian_difference_reconstructs_dividend ((((((e) * (x2))) + (((f) * (x1))))) + (((((g) * (x4))) + (((h) * (x5))))))
  7. L180
    specialize gaussian_difference_reconstructs_dividend ((((((((e) * (x4))) + (((f) * (x5))))) + (((((g) * (x1))) + (((h) * (x2))))))) + (((((g) * (x5))) + (((h) * (x4))))))
  8. L181
    specialize gaussian_difference_reconstructs_dividend ((((((((e) * (x5))) + (((f) * (x4))))) + (((((g) * (x2))) + (((h) * (x1))))))) + (((((g) * (x4))) + (((h) * (x5))))))
  9. L182
    apply gaussian_difference_reconstructs_dividend
41Separate the logical casesL183–183

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

  1. L183
    split
42Use earlier factsL184–184

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

  1. L184
    exact hremainder_witness
43Separate the logical casesL185–185

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

  1. L185
    split
44Use earlier factsL186–192

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

  1. L186
    exact hdivisor_witness
  2. L187
    specialize four_square_descent_norm_bound_forces_smaller_multiplier x
  3. L188
    specialize four_square_descent_norm_bound_forces_smaller_multiplier x7
  4. L189
    specialize four_square_descent_norm_bound_forces_smaller_multiplier x8
  5. L190
    apply four_square_descent_norm_bound_forces_smaller_multiplier
  6. L191
    exact hnormequation
  7. L192
    exact hstrict

Library-wide reading audit

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