EI0018

eisenstein_weighted_norm_product

The actual positive weight-three norm is multiplicative under (x,y)(u,v)=(xu−3yv,xv+yu), for all arbitrary signed representatives.

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

∀ ap. ∀ an. ∀ bp. ∀ bn. ∀ cp. ∀ cn. ∀ dp. ∀ dn. ∀ N. ∀ M. WeightedSignedNormThree(ap,an,bp,bn,N) → WeightedSignedNormThree(cp,cn,dp,dn,M) → WeightedSignedNormThree(ap · cp + an · cn + 3 · (bp · dn + bn · dp),ap · cn + an · cp + 3 · (bp · dp + bn · dn),ap · dp + an · dn + (bp · cp + bn · cn),ap · dn + an · dp + (bp · cn + bn · cp),N · M)

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

Definition DAG

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

Actual proof prerequisites

gaussian_signed_square_exists · checked external prerequisitegaussian_signed_square_product · checked external prerequisitegaussian_signed_square_scaled · checked external prerequisitegaussian_signed_product_cross_interchange · checked external prerequisiteeisenstein_signed_product_scaled_righteisenstein_weighted_square_lagrangemul_shuffle_four · checked external prerequisiteadd_mul · checked external prerequisitemul_add · checked external prerequisitemul_assoc · checked external prerequisiteadd_assoc · checked external prerequisiteadd_comm · checked external prerequisitemul_comm · checked external prerequisitefour_square_add_swap_right_tail · checked external prerequisitenatural_mul_swap_right_tail · checked external prerequisite
Original expanded first-order statement 
forall ap an bp bn cp cn dp dn N M. (exists ee_real_square_first_product ee_imag_square_first_product. (((((ap) * (ap))) + (((an) * (an)))) = ((ee_real_square_first_product) + (((((ap) * (an))) + (((an) * (ap))))))) /\ ((((((bp) * (bp))) + (((bn) * (bn)))) = ((ee_imag_square_first_product) + (((((bp) * (bn))) + (((bn) * (bp))))))) /\ (N) = ee_real_square_first_product + 3 * ee_imag_square_first_product)) -> (exists ee_real_square_second_product ee_imag_square_second_product. (((((cp) * (cp))) + (((cn) * (cn)))) = ((ee_real_square_second_product) + (((((cp) * (cn))) + (((cn) * (cp))))))) /\ ((((((dp) * (dp))) + (((dn) * (dn)))) = ((ee_imag_square_second_product) + (((((dp) * (dn))) + (((dn) * (dp))))))) /\ (M) = ee_real_square_second_product + 3 * ee_imag_square_second_product)) -> (exists ee_real_square_product ee_imag_square_product. (((((((((((ap) * (cp))) + (((an) * (cn))))) + (((3) * (((((bp) * (dn))) + (((bn) * (dp))))))))) * (((((((ap) * (cp))) + (((an) * (cn))))) + (((3) * (((((bp) * (dn))) + (((bn) * (dp))))))))))) + (((((((((ap) * (cn))) + (((an) * (cp))))) + (((3) * (((((bp) * (dp))) + (((bn) * (dn))))))))) * (((((((ap) * (cn))) + (((an) * (cp))))) + (((3) * (((((bp) * (dp))) + (((bn) * (dn)))))))))))) = ((ee_real_square_product) + (((((((((((ap) * (cp))) + (((an) * (cn))))) + (((3) * (((((bp) * (dn))) + (((bn) * (dp))))))))) * (((((((ap) * (cn))) + (((an) * (cp))))) + (((3) * (((((bp) * (dp))) + (((bn) * (dn))))))))))) + (((((((((ap) * (cn))) + (((an) * (cp))))) + (((3) * (((((bp) * (dp))) + (((bn) * (dn))))))))) * (((((((ap) * (cp))) + (((an) * (cn))))) + (((3) * (((((bp) * (dn))) + (((bn) * (dp))))))))))))))) /\ ((((((((((((ap) * (dp))) + (((an) * (dn))))) + (((((bp) * (cp))) + (((bn) * (cn))))))) * (((((((ap) * (dp))) + (((an) * (dn))))) + (((((bp) * (cp))) + (((bn) * (cn))))))))) + (((((((((ap) * (dn))) + (((an) * (dp))))) + (((((bp) * (cn))) + (((bn) * (cp))))))) * (((((((ap) * (dn))) + (((an) * (dp))))) + (((((bp) * (cn))) + (((bn) * (cp)))))))))) = ((ee_imag_square_product) + (((((((((((ap) * (dp))) + (((an) * (dn))))) + (((((bp) * (cp))) + (((bn) * (cn))))))) * (((((((ap) * (dn))) + (((an) * (dp))))) + (((((bp) * (cn))) + (((bn) * (cp))))))))) + (((((((((ap) * (dn))) + (((an) * (dp))))) + (((((bp) * (cn))) + (((bn) * (cp))))))) * (((((((ap) * (dp))) + (((an) * (dn))))) + (((((bp) * (cp))) + (((bn) * (cn))))))))))))) /\ (N * M) = ee_real_square_product + 3 * ee_imag_square_product))

Complete tactic proof in conservative notation

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

127 script commands · 26 reading checkpoints · 6 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 (2)
eisenstein signed product scaled righteisenstein weighted square lagrange
01Fix variables and assumptionsL1–10

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

  1. L1
    intro ap
  2. L2
    intro an
  3. L3
    intro bp
  4. L4
    intro bn
  5. L5
    intro cp
  6. L6
    intro cn
  7. L7
    intro dp
  8. L8
    intro dn
  9. L9
    intro N
  10. L10
    intro M
02Fix variables and assumptionsL11–12

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

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

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

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

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

  1. L21
    have hreal : ∃ R. SignedDifferenceSquare(ap · cp + an · cn + 3 · (bp · dn + bn · dp),ap · cn + an · cp + 3 · (bp · dp + bn · dn),R)Definitions: SignedDifferenceSquare(ap · cp + an · cn + 3 · (bp · dn + bn · dp),ap · cn + an · cp + 3 · (bp · dp + bn · dn),R)Original native command in the exact edition
  2. L22
    specialize gaussian_signed_square_exists ((((((ap) * (cp))) + (((an) * (cn))))) + (((3) * (((((bp) * (dn))) + (((bn) * (dp))))))))
  3. L23
    specialize gaussian_signed_square_exists ((((((ap) * (cn))) + (((an) * (cp))))) + (((3) * (((((bp) * (dp))) + (((bn) * (dn))))))))
  4. L24
    apply gaussian_signed_square_exists
05Separate the logical casesL25–25

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

  1. L25
    cases hreal
06Establish himagL26–29

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

  1. L26
    have himag : ∃ I. SignedDifferenceSquare(ap · dp + an · dn + (bp · cp + bn · cn),ap · dn + an · dp + (bp · cn + bn · cp),I)Definitions: SignedDifferenceSquare(ap · dp + an · dn + (bp · cp + bn · cn),ap · dn + an · dp + (bp · cn + bn · cp),I)Original native command in the exact edition
  2. L27
    specialize gaussian_signed_square_exists ((((((ap) * (dp))) + (((an) * (dn))))) + (((((bp) * (cp))) + (((bn) * (cn))))))
  3. L28
    specialize gaussian_signed_square_exists ((((((ap) * (dn))) + (((an) * (dp))))) + (((((bp) * (cn))) + (((bn) * (cp))))))
  4. L29
    apply gaussian_signed_square_exists
07Separate the logical casesL30–30

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

  1. L30
    cases himag
08Establish hcrossL31–40

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

  1. L31
    have hcross · expand full local formula (696 characters)have hcross : (((((((((ap) * (cp))) + (((an) * (cn))))) * (((((bp) * (dp))) + (((bn) * (dn))))))) + (((((((ap) * (cn))) + (((an) * (cp))))) * (((((bp) * (dn))) + (((bn) * (dp)))))))) = ((((((((ap) * (dp))) + (((an) * (dn))))) * (((((bp) * (cp))) + (((bn) * (cn))))))) + (((((((ap) * (dn))) + (((an) * (dp))))) * (((((bp) * (cn))) + (((bn) * (cp))))))))) /\ (((((((((ap) * (cp))) + (((an) * (cn))))) * (((((bp) * (dn))) + (((bn) * (dp))))))) + (((((((ap) * (cn))) + (((an) * (cp))))) * (((((bp) * (dp))) + (((bn) * (dn)))))))) = ((((((((ap) * (dp))) + (((an) * (dn))))) * (((((bp) * (cn))) + (((bn) * (cp))))))) + (((((((ap) * (dn))) + (((an) * (dp))))) * (((((bp) * (cp))) + (((bn) * (cn)))))))))
  2. L32
    specialize gaussian_signed_product_cross_interchange ap
  3. L33
    specialize gaussian_signed_product_cross_interchange an
  4. L34
    specialize gaussian_signed_product_cross_interchange bp
  5. L35
    specialize gaussian_signed_product_cross_interchange bn
  6. L36
    specialize gaussian_signed_product_cross_interchange cp
  7. L37
    specialize gaussian_signed_product_cross_interchange cn
  8. L38
    specialize gaussian_signed_product_cross_interchange dp
  9. L39
    specialize gaussian_signed_product_cross_interchange dn
  10. L40
    apply gaussian_signed_product_cross_interchange
09Separate the logical casesL41–41

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

  1. L41
    cases hcross
10Establish hscaleL42–48

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein signed product scaled right.

  1. L42
    have hscale · expand full local formula (748 characters)have hscale : (((((((((ap) * (cp))) + (((an) * (cn))))) * (((3) * (((((bp) * (dp))) + (((bn) * (dn))))))))) + (((((((ap) * (cn))) + (((an) * (cp))))) * (((3) * (((((bp) * (dn))) + (((bn) * (dp)))))))))) = 3 * (((((((((ap) * (cp))) + (((an) * (cn))))) * (((((bp) * (dp))) + (((bn) * (dn))))))) + (((((((ap) * (cn))) + (((an) * (cp))))) * (((((bp) * (dn))) + (((bn) * (dp)))))))))) /\ (((((((((ap) * (cp))) + (((an) * (cn))))) * (((3) * (((((bp) * (dn))) + (((bn) * (dp))))))))) + (((((((ap) * (cn))) + (((an) * (cp))))) * (((3) * (((((bp) * (dp))) + (((bn) * (dn)))))))))) = 3 * (((((((((ap) * (cp))) + (((an) * (cn))))) * (((((bp) * (dn))) + (((bn) * (dp))))))) + (((((((ap) * (cn))) + (((an) * (cp))))) * (((((bp) * (dp))) + (((bn) * (dn))))))))))
  2. L43
    specialize eisenstein_signed_product_scaled_right ((((ap) * (cp))) + (((an) * (cn))))
  3. L44
    specialize eisenstein_signed_product_scaled_right ((((ap) * (cn))) + (((an) * (cp))))
  4. L45
    specialize eisenstein_signed_product_scaled_right ((((bp) * (dp))) + (((bn) * (dn))))
  5. L46
    specialize eisenstein_signed_product_scaled_right ((((bp) * (dn))) + (((bn) * (dp))))
  6. L47
    specialize eisenstein_signed_product_scaled_right 3
  7. L48
    apply eisenstein_signed_product_scaled_right
11Separate the logical casesL49–49

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

  1. L49
    cases hscale
12Calculate and transport equalitiesL50–51

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

  1. L50
    rewrite hcross_left at hscale_left
  2. L51
    rewrite hcross_right at hscale_right
13Establish hnormL52–61

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

  1. L52
    have hnorm : x4 + 3 * x5 = (x * x2 + (3 * x1) * (3 * x3)) + 3 * (x * x3 + x1 * x2)
  2. L53
    specialize eisenstein_weighted_square_lagrange ((((ap) * (cp))) + (((an) * (cn))))
  3. L54
    specialize eisenstein_weighted_square_lagrange ((((ap) * (cn))) + (((an) * (cp))))
  4. L55
    specialize eisenstein_weighted_square_lagrange ((3) * (((((bp) * (dp))) + (((bn) * (dn))))))
  5. L56
    specialize eisenstein_weighted_square_lagrange ((3) * (((((bp) * (dn))) + (((bn) * (dp))))))
  6. L57
    specialize eisenstein_weighted_square_lagrange ((((ap) * (dp))) + (((an) * (dn))))
  7. L58
    specialize eisenstein_weighted_square_lagrange ((((ap) * (dn))) + (((an) * (dp))))
  8. L59
    specialize eisenstein_weighted_square_lagrange ((((bp) * (cp))) + (((bn) * (cn))))
  9. L60
    specialize eisenstein_weighted_square_lagrange ((((bp) * (cn))) + (((bn) * (cp))))
  10. L61
    specialize eisenstein_weighted_square_lagrange x * x2
14Use earlier factsL62–71

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

  1. L62
    specialize eisenstein_weighted_square_lagrange (3 * x1) * (3 * x3)
  2. L63
    specialize eisenstein_weighted_square_lagrange x * x3
  3. L64
    specialize eisenstein_weighted_square_lagrange x1 * x2
  4. L65
    specialize eisenstein_weighted_square_lagrange x4
  5. L66
    specialize eisenstein_weighted_square_lagrange x5
  6. L67
    apply eisenstein_weighted_square_lagrange
  7. L68
    specialize gaussian_signed_square_product ap
  8. L69
    specialize gaussian_signed_square_product an
  9. L70
    specialize gaussian_signed_square_product cp
  10. L71
    specialize gaussian_signed_square_product cn
15Use earlier factsL72–76

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

  1. L72
    specialize gaussian_signed_square_product x
  2. L73
    specialize gaussian_signed_square_product x2
  3. L74
    apply gaussian_signed_square_product
  4. L75
    exact hfirst_witness_witness_left
  5. L76
    exact hsecond_witness_witness_left
16Establish hscalarL77–86

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul shuffle four.

  1. L77
    have hscalar : (3 * 3) * (x1 * x3) = (3 * x1) * (3 * x3)
  2. L78
    apply mul_shuffle_four
  3. L79
    rewrite <- hscalar
  4. L80
    specialize gaussian_signed_square_scaled ((((bp) * (dp))) + (((bn) * (dn))))
  5. L81
    specialize gaussian_signed_square_scaled ((((bp) * (dn))) + (((bn) * (dp))))
  6. L82
    specialize gaussian_signed_square_scaled (x1 * x3)
  7. L83
    specialize gaussian_signed_square_scaled 3
  8. L84
    apply gaussian_signed_square_scaled
  9. L85
    specialize gaussian_signed_square_product bp
  10. L86
    specialize gaussian_signed_square_product bn
17Use earlier factsL87–96

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

  1. L87
    specialize gaussian_signed_square_product dp
  2. L88
    specialize gaussian_signed_square_product dn
  3. L89
    specialize gaussian_signed_square_product x1
  4. L90
    specialize gaussian_signed_square_product x3
  5. L91
    apply gaussian_signed_square_product
  6. L92
    exact hfirst_witness_witness_right_left
  7. L93
    exact hsecond_witness_witness_right_left
  8. L94
    specialize gaussian_signed_square_product ap
  9. L95
    specialize gaussian_signed_square_product an
  10. L96
    specialize gaussian_signed_square_product dp
18Use earlier factsL97–106

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

  1. L97
    specialize gaussian_signed_square_product dn
  2. L98
    specialize gaussian_signed_square_product x
  3. L99
    specialize gaussian_signed_square_product x3
  4. L100
    apply gaussian_signed_square_product
  5. L101
    exact hfirst_witness_witness_left
  6. L102
    exact hsecond_witness_witness_right_left
  7. L103
    specialize gaussian_signed_square_product bp
  8. L104
    specialize gaussian_signed_square_product bn
  9. L105
    specialize gaussian_signed_square_product cp
  10. L106
    specialize gaussian_signed_square_product cn
19Use earlier factsL107–115

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

  1. L107
    specialize gaussian_signed_square_product x1
  2. L108
    specialize gaussian_signed_square_product x2
  3. L109
    apply gaussian_signed_square_product
  4. L110
    exact hfirst_witness_witness_right_left
  5. L111
    exact hsecond_witness_witness_left
  6. L112
    exact hscale_left
  7. L113
    exact hscale_right
  8. L114
    exact hreal_witness
  9. L115
    exact himag_witness
20Construct an explicit witnessL116–117

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

  1. L116
    exists x4
  2. L117
    exists x5
21Separate the logical casesL118–118

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

  1. L118
    split
22Use earlier factsL119–119

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

  1. L119
    exact hreal_witness
23Separate the logical casesL120–120

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

  1. L120
    split
24Use earlier factsL121–121

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

  1. L121
    exact himag_witness
25Calculate and transport equalitiesL122–126

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

  1. L122
    rewrite hfirst_witness_witness_right_right
  2. L123
    rewrite hsecond_witness_witness_right_right
  3. L124
    trans (x * x2 + (3 * x1) * (3 * x3)) + 3 * (x * x3 + x1 * x2)
  4. L125
    simp [add_mul, mul_add, mul_assoc, add_assoc, add_comm, mul_comm, four_square_add_swap_right_tail, natural_mul_swap_right_tail]
  5. L126
    symm
26Use earlier factsL127–127

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

  1. L127
    exact hnorm

Library-wide reading audit

Original defined command ledger · 127 lines
  1. 0001intro ap
  2. 0002intro an
  3. 0003intro bp
  4. 0004intro bn
  5. 0005intro cp
  6. 0006intro cn
  7. 0007intro dp
  8. 0008intro dn
  9. 0009intro N
  10. 0010intro M
  11. 0011intro hfirst
  12. 0012intro hsecond
  13. 0013cases hfirst
  14. 0014cases hfirst_witness
  15. 0015cases hfirst_witness_witness
  16. 0016cases hfirst_witness_witness_right
  17. 0017cases hsecond
  18. 0018cases hsecond_witness
  19. 0019cases hsecond_witness_witness
  20. 0020cases hsecond_witness_witness_right
  21. 0021have hreal : ∃ R. SignedDifferenceSquare(ap · cp + an · cn + 3 · (bp · dn + bn · dp),ap · cn + an · cp + 3 · (bp · dp + bn · dn),R)
  22. 0022specialize gaussian_signed_square_exists ((((((ap) * (cp))) + (((an) * (cn))))) + (((3) * (((((bp) * (dn))) + (((bn) * (dp))))))))
  23. 0023specialize gaussian_signed_square_exists ((((((ap) * (cn))) + (((an) * (cp))))) + (((3) * (((((bp) * (dp))) + (((bn) * (dn))))))))
  24. 0024apply gaussian_signed_square_exists
  25. 0025cases hreal
  26. 0026have himag : ∃ I. SignedDifferenceSquare(ap · dp + an · dn + (bp · cp + bn · cn),ap · dn + an · dp + (bp · cn + bn · cp),I)
  27. 0027specialize gaussian_signed_square_exists ((((((ap) * (dp))) + (((an) * (dn))))) + (((((bp) * (cp))) + (((bn) * (cn))))))
  28. 0028specialize gaussian_signed_square_exists ((((((ap) * (dn))) + (((an) * (dp))))) + (((((bp) * (cn))) + (((bn) * (cp))))))
  29. 0029apply gaussian_signed_square_exists
  30. 0030cases himag
  31. 0031have hcross : (((((((((ap) * (cp))) + (((an) * (cn))))) * (((((bp) * (dp))) + (((bn) * (dn))))))) + (((((((ap) * (cn))) + (((an) * (cp))))) * (((((bp) * (dn))) + (((bn) * (dp)))))))) = ((((((((ap) * (dp))) + (((an) * (dn))))) * (((((bp) * (cp))) + (((bn) * (cn))))))) + (((((((ap) * (dn))) + (((an) * (dp))))) * (((((bp) * (cn))) + (((bn) * (cp))))))))) /\ (((((((((ap) * (cp))) + (((an) * (cn))))) * (((((bp) * (dn))) + (((bn) * (dp))))))) + (((((((ap) * (cn))) + (((an) * (cp))))) * (((((bp) * (dp))) + (((bn) * (dn)))))))) = ((((((((ap) * (dp))) + (((an) * (dn))))) * (((((bp) * (cn))) + (((bn) * (cp))))))) + (((((((ap) * (dn))) + (((an) * (dp))))) * (((((bp) * (cp))) + (((bn) * (cn)))))))))
  32. 0032specialize gaussian_signed_product_cross_interchange ap
  33. 0033specialize gaussian_signed_product_cross_interchange an
  34. 0034specialize gaussian_signed_product_cross_interchange bp
  35. 0035specialize gaussian_signed_product_cross_interchange bn
  36. 0036specialize gaussian_signed_product_cross_interchange cp
  37. 0037specialize gaussian_signed_product_cross_interchange cn
  38. 0038specialize gaussian_signed_product_cross_interchange dp
  39. 0039specialize gaussian_signed_product_cross_interchange dn
  40. 0040apply gaussian_signed_product_cross_interchange
  41. 0041cases hcross
  42. 0042have hscale : (((((((((ap) * (cp))) + (((an) * (cn))))) * (((3) * (((((bp) * (dp))) + (((bn) * (dn))))))))) + (((((((ap) * (cn))) + (((an) * (cp))))) * (((3) * (((((bp) * (dn))) + (((bn) * (dp)))))))))) = 3 * (((((((((ap) * (cp))) + (((an) * (cn))))) * (((((bp) * (dp))) + (((bn) * (dn))))))) + (((((((ap) * (cn))) + (((an) * (cp))))) * (((((bp) * (dn))) + (((bn) * (dp)))))))))) /\ (((((((((ap) * (cp))) + (((an) * (cn))))) * (((3) * (((((bp) * (dn))) + (((bn) * (dp))))))))) + (((((((ap) * (cn))) + (((an) * (cp))))) * (((3) * (((((bp) * (dp))) + (((bn) * (dn)))))))))) = 3 * (((((((((ap) * (cp))) + (((an) * (cn))))) * (((((bp) * (dn))) + (((bn) * (dp))))))) + (((((((ap) * (cn))) + (((an) * (cp))))) * (((((bp) * (dp))) + (((bn) * (dn))))))))))
  43. 0043specialize eisenstein_signed_product_scaled_right ((((ap) * (cp))) + (((an) * (cn))))
  44. 0044specialize eisenstein_signed_product_scaled_right ((((ap) * (cn))) + (((an) * (cp))))
  45. 0045specialize eisenstein_signed_product_scaled_right ((((bp) * (dp))) + (((bn) * (dn))))
  46. 0046specialize eisenstein_signed_product_scaled_right ((((bp) * (dn))) + (((bn) * (dp))))
  47. 0047specialize eisenstein_signed_product_scaled_right 3
  48. 0048apply eisenstein_signed_product_scaled_right
  49. 0049cases hscale
  50. 0050rewrite hcross_left at hscale_left
  51. 0051rewrite hcross_right at hscale_right
  52. 0052have hnorm : x4 + 3 * x5 = (x * x2 + (3 * x1) * (3 * x3)) + 3 * (x * x3 + x1 * x2)
  53. 0053specialize eisenstein_weighted_square_lagrange ((((ap) * (cp))) + (((an) * (cn))))
  54. 0054specialize eisenstein_weighted_square_lagrange ((((ap) * (cn))) + (((an) * (cp))))
  55. 0055specialize eisenstein_weighted_square_lagrange ((3) * (((((bp) * (dp))) + (((bn) * (dn))))))
  56. 0056specialize eisenstein_weighted_square_lagrange ((3) * (((((bp) * (dn))) + (((bn) * (dp))))))
  57. 0057specialize eisenstein_weighted_square_lagrange ((((ap) * (dp))) + (((an) * (dn))))
  58. 0058specialize eisenstein_weighted_square_lagrange ((((ap) * (dn))) + (((an) * (dp))))
  59. 0059specialize eisenstein_weighted_square_lagrange ((((bp) * (cp))) + (((bn) * (cn))))
  60. 0060specialize eisenstein_weighted_square_lagrange ((((bp) * (cn))) + (((bn) * (cp))))
  61. 0061specialize eisenstein_weighted_square_lagrange x * x2
  62. 0062specialize eisenstein_weighted_square_lagrange (3 * x1) * (3 * x3)
  63. 0063specialize eisenstein_weighted_square_lagrange x * x3
  64. 0064specialize eisenstein_weighted_square_lagrange x1 * x2
  65. 0065specialize eisenstein_weighted_square_lagrange x4
  66. 0066specialize eisenstein_weighted_square_lagrange x5
  67. 0067apply eisenstein_weighted_square_lagrange
  68. 0068specialize gaussian_signed_square_product ap
  69. 0069specialize gaussian_signed_square_product an
  70. 0070specialize gaussian_signed_square_product cp
  71. 0071specialize gaussian_signed_square_product cn
  72. 0072specialize gaussian_signed_square_product x
  73. 0073specialize gaussian_signed_square_product x2
  74. 0074apply gaussian_signed_square_product
  75. 0075exact hfirst_witness_witness_left
  76. 0076exact hsecond_witness_witness_left
  77. 0077have hscalar : (3 * 3) * (x1 * x3) = (3 * x1) * (3 * x3)
  78. 0078apply mul_shuffle_four
  79. 0079rewrite <- hscalar
  80. 0080specialize gaussian_signed_square_scaled ((((bp) * (dp))) + (((bn) * (dn))))
  81. 0081specialize gaussian_signed_square_scaled ((((bp) * (dn))) + (((bn) * (dp))))
  82. 0082specialize gaussian_signed_square_scaled (x1 * x3)
  83. 0083specialize gaussian_signed_square_scaled 3
  84. 0084apply gaussian_signed_square_scaled
  85. 0085specialize gaussian_signed_square_product bp
  86. 0086specialize gaussian_signed_square_product bn
  87. 0087specialize gaussian_signed_square_product dp
  88. 0088specialize gaussian_signed_square_product dn
  89. 0089specialize gaussian_signed_square_product x1
  90. 0090specialize gaussian_signed_square_product x3
  91. 0091apply gaussian_signed_square_product
  92. 0092exact hfirst_witness_witness_right_left
  93. 0093exact hsecond_witness_witness_right_left
  94. 0094specialize gaussian_signed_square_product ap
  95. 0095specialize gaussian_signed_square_product an
  96. 0096specialize gaussian_signed_square_product dp
  97. 0097specialize gaussian_signed_square_product dn
  98. 0098specialize gaussian_signed_square_product x
  99. 0099specialize gaussian_signed_square_product x3
  100. 0100apply gaussian_signed_square_product
  101. 0101exact hfirst_witness_witness_left
  102. 0102exact hsecond_witness_witness_right_left
  103. 0103specialize gaussian_signed_square_product bp
  104. 0104specialize gaussian_signed_square_product bn
  105. 0105specialize gaussian_signed_square_product cp
  106. 0106specialize gaussian_signed_square_product cn
  107. 0107specialize gaussian_signed_square_product x1
  108. 0108specialize gaussian_signed_square_product x2
  109. 0109apply gaussian_signed_square_product
  110. 0110exact hfirst_witness_witness_right_left
  111. 0111exact hsecond_witness_witness_left
  112. 0112exact hscale_left
  113. 0113exact hscale_right
  114. 0114exact hreal_witness
  115. 0115exact himag_witness
  116. 0116exists x4
  117. 0117exists x5
  118. 0118split
  119. 0119exact hreal_witness
  120. 0120split
  121. 0121exact himag_witness
  122. 0122rewrite hfirst_witness_witness_right_right
  123. 0123rewrite hsecond_witness_witness_right_right
  124. 0124trans (x * x2 + (3 * x1) * (3 * x3)) + 3 * (x * x3 + x1 * x2)
  125. 0125simp [add_mul, mul_add, mul_assoc, add_assoc, add_comm, mul_comm, four_square_add_swap_right_tail, natural_mul_swap_right_tail]
  126. 0126symm
  127. 0127exact hnorm