FS004O · theorem body

four_square_signed_natural_positive_first_blocks

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

A positive first orientation and three negative orientations make all four ordinary Hamilton quaternion blocks congruent modulo the multiplier.

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.

Statement with defined notation

∀ k. ∀ a. ∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ h. ModEq(k,e · e + f · f + g · g + h · h,0) → ModEq(k,a,e) → ModEq(k,b + f,0) → ModEq(k,c + g,0) → ModEq(k,d + h,0) → ModEq(k,a · e,b · f + c · g + d · h) ∧ (ModEq(k,a · f + b · e + c · h,d · g) ∧ (ModEq(k,a · g + c · e + d · f,b · h) ∧ ModEq(k,a · h + b · g + d · e,c · f)))

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0008 ModEq

In local proof propositions

PD0008 ModEq
Exact expanded first-order statement
forall k a b c d e f g h. (exists ftcn_left_fssbn_natural_positive_first_norm ftcn_right_fssbn_natural_positive_first_norm. (e * e + f * f + g * g + h * h) + (k) * ftcn_left_fssbn_natural_positive_first_norm = (0) + (k) * ftcn_right_fssbn_natural_positive_first_norm) -> (exists ftcn_left_fssbn_natural_positive_first_a_positive ftcn_right_fssbn_natural_positive_first_a_positive. (a) + (k) * ftcn_left_fssbn_natural_positive_first_a_positive = (e) + (k) * ftcn_right_fssbn_natural_positive_first_a_positive) -> (exists ftcn_left_fssbn_natural_positive_first_b_negative ftcn_right_fssbn_natural_positive_first_b_negative. (b + f) + (k) * ftcn_left_fssbn_natural_positive_first_b_negative = (0) + (k) * ftcn_right_fssbn_natural_positive_first_b_negative) -> (exists ftcn_left_fssbn_natural_positive_first_c_negative ftcn_right_fssbn_natural_positive_first_c_negative. (c + g) + (k) * ftcn_left_fssbn_natural_positive_first_c_negative = (0) + (k) * ftcn_right_fssbn_natural_positive_first_c_negative) -> (exists ftcn_left_fssbn_natural_positive_first_d_negative ftcn_right_fssbn_natural_positive_first_d_negative. (d + h) + (k) * ftcn_left_fssbn_natural_positive_first_d_negative = (0) + (k) * ftcn_right_fssbn_natural_positive_first_d_negative) -> ((exists ftcn_left_fssbn_natural_positive_first_block_0 ftcn_right_fssbn_natural_positive_first_block_0. (a * e) + (k) * ftcn_left_fssbn_natural_positive_first_block_0 = (b * f + c * g + d * h) + (k) * ftcn_right_fssbn_natural_positive_first_block_0) /\ ((exists ftcn_left_fssbn_natural_positive_first_block_1 ftcn_right_fssbn_natural_positive_first_block_1. (a * f + b * e + c * h) + (k) * ftcn_left_fssbn_natural_positive_first_block_1 = (d * g) + (k) * ftcn_right_fssbn_natural_positive_first_block_1) /\ ((exists ftcn_left_fssbn_natural_positive_first_block_2 ftcn_right_fssbn_natural_positive_first_block_2. (a * g + c * e + d * f) + (k) * ftcn_left_fssbn_natural_positive_first_block_2 = (b * h) + (k) * ftcn_right_fssbn_natural_positive_first_block_2) /\ (exists ftcn_left_fssbn_natural_positive_first_block_3 ftcn_right_fssbn_natural_positive_first_block_3. (a * h + b * g + d * e) + (k) * ftcn_left_fssbn_natural_positive_first_block_3 = (c * f) + (k) * ftcn_right_fssbn_natural_positive_first_block_3))))

Proof neighborhood

Direct theorem prerequisites

FS005U four_square_signed_dot_positive FS005V four_square_signed_dot_negative_zero FS005P four_square_signed_mod_zero_add add_assoc · Stable closed add_comm · Stable closed FS0006 four_square_add_swap_right_tail FS005X four_square_signed_partition_balance FS005O four_square_signed_cross_mixed_zero FS005N four_square_signed_cross_negative FS005W four_square_signed_mod_zero_plus_congruent FS002N four_square_euler_add_swap_last

Direct theorem dependents

FS004X four_square_signed_orientation_mask_07 FS0051 four_square_signed_orientation_mask_11 FS0053 four_square_signed_orientation_mask_13 FS0054 four_square_signed_orientation_mask_14

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

167 script commands · 26 reading checkpoints · 15 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 (9)
four square signed dot positivefour square signed dot negative zerofour square signed mod zero addfour square add swap right tailfour square signed partition balancefour square signed cross mixed zerofour square signed cross negativefour square signed mod zero plus congruentfour square euler add swap last
01Fix variables and assumptionsL1–10

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

  1. L1
    intro k
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro d
  6. L6
    intro e
  7. L7
    intro f
  8. L8
    intro g
  9. L9
    intro h
  10. L10
    intro hnorm
02Fix variables and assumptionsL11–14

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

  1. L11
    intro ha
  2. L12
    intro hb
  3. L13
    intro hc
  4. L14
    intro hd
03Separate the logical casesL15–15

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

  1. L15
    split
04Establish hpositiveL16–21

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

  1. L16
    have hpositive : ModEq(k,a · e,e · e)Definitions: ModEq(k,a · e,e · e)Original native command in the exact edition
  2. L17
    specialize four_square_signed_dot_positive k
  3. L18
    specialize four_square_signed_dot_positive a
  4. L19
    specialize four_square_signed_dot_positive e
  5. L20
    apply four_square_signed_dot_positive
  6. L21
    exact ha
05Establish hdbL22–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed dot negative zero.

  1. L22
    have hdb : ModEq(k,b · f + f · f,0)Definitions: ModEq(k,b · f + f · f,0)Original native command in the exact edition
  2. L23
    specialize four_square_signed_dot_negative_zero k
  3. L24
    specialize four_square_signed_dot_negative_zero b
  4. L25
    specialize four_square_signed_dot_negative_zero f
  5. L26
    apply four_square_signed_dot_negative_zero
  6. L27
    exact hb
06Establish hdcL28–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed dot negative zero.

  1. L28
    have hdc : ModEq(k,c · g + g · g,0)Definitions: ModEq(k,c · g + g · g,0)Original native command in the exact edition
  2. L29
    specialize four_square_signed_dot_negative_zero k
  3. L30
    specialize four_square_signed_dot_negative_zero c
  4. L31
    specialize four_square_signed_dot_negative_zero g
  5. L32
    apply four_square_signed_dot_negative_zero
  6. L33
    exact hc
07Establish hddL34–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed dot negative zero.

  1. L34
    have hdd : ModEq(k,d · h + h · h,0)Definitions: ModEq(k,d · h + h · h,0)Original native command in the exact edition
  2. L35
    specialize four_square_signed_dot_negative_zero k
  3. L36
    specialize four_square_signed_dot_negative_zero d
  4. L37
    specialize four_square_signed_dot_negative_zero h
  5. L38
    apply four_square_signed_dot_negative_zero
  6. L39
    exact hd
08Establish hbczeroL40–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed mod zero add.

  1. L40
    have hbczero : ModEq(k,b · f + f · f + (c · g + g · g),0)Definitions: ModEq(k,b · f + f · f + (c · g + g · g),0)Original native command in the exact edition
  2. L41
    specialize four_square_signed_mod_zero_add k
  3. L42
    specialize four_square_signed_mod_zero_add (b * f + f * f)
  4. L43
    specialize four_square_signed_mod_zero_add (c * g + g * g)
  5. L44
    apply four_square_signed_mod_zero_add
  6. L45
    exact hdb
  7. L46
    exact hdc
09Establish hnegativeL47–53

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed mod zero add.

  1. L47
    have hnegative : ModEq(k,b · f + f · f + (c · g + g · g) + (d · h + h · h),0)Definitions: ModEq(k,b · f + f · f + (c · g + g · g) + (d · h + h · h),0)Original native command in the exact edition
  2. L48
    specialize four_square_signed_mod_zero_add k
  3. L49
    specialize four_square_signed_mod_zero_add ((b * f + f * f) + (c * g + g * g))
  4. L50
    specialize four_square_signed_mod_zero_add (d * h + h * h)
  5. L51
    apply four_square_signed_mod_zero_add
  6. L52
    exact hbczero
  7. L53
    exact hdd
10Establish hshuffleL54–63

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square add swap right tail.

  1. L54
    have hshuffle : (((b * f + f * f) + (c * g + g * g)) + (d * h + h * h)) = ((b * f + c * g + d * h) + (f * f + g * g + h * h))
  2. L55
    trans ((b * f) + ((f * f) + ((c * g) + ((g * g) + ((d * h) + (h * h))))))
  3. L56
    simp [add_assoc]
  4. L57
    trans ((b * f) + ((c * g) + ((d * h) + ((f * f) + ((g * g) + (h * h))))))
  5. L58
    congr
  6. L59
    refl
  7. L60
    trans ((c * g) + ((f * f) + ((g * g) + ((d * h) + (h * h)))))
  8. L61
    apply four_square_add_swap_right_tail
  9. L62
    congr
  10. L63
    refl
11Calculate and transport equalitiesL64–67

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

  1. L64
    trans ((d * h) + ((f * f) + ((g * g) + (h * h))))
  2. L65
    trans ((f * f) + ((d * h) + ((g * g) + (h * h))))
  3. L66
    congr
  4. L67
    refl
12Use earlier factsL68–69

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

  1. L68
    apply four_square_add_swap_right_tail
  2. L69
    apply four_square_add_swap_right_tail
13Calculate and transport equalitiesL70–75

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

  1. L70
    congr
  2. L71
    refl
  3. L72
    refl
  4. L73
    symm
  5. L74
    simp [add_assoc]
  6. L75
    rewrite hshuffle at hnegative
14Establish hnormshapeL76–85

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

  1. L76
    have hnormshape : (e * e + f * f + g * g + h * h) = ((e * e) + (f * f + g * g + h * h))
  2. L77
    simp [add_assoc]
  3. L78
    rewrite hnormshape at hnorm
  4. L79
    specialize four_square_signed_partition_balance k
  5. L80
    specialize four_square_signed_partition_balance (a * e)
  6. L81
    specialize four_square_signed_partition_balance (e * e)
  7. L82
    specialize four_square_signed_partition_balance (b * f + c * g + d * h)
  8. L83
    specialize four_square_signed_partition_balance (f * f + g * g + h * h)
  9. L84
    apply four_square_signed_partition_balance
  10. L85
    exact hpositive
15Use earlier factsL86–87

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

  1. L86
    exact hnegative
  2. L87
    exact hnorm
16Separate the logical casesL88–88

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

  1. L88
    split
17Establish hfirst_zeroL89–97

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed cross mixed zero.

  1. L89
    have hfirst_zero : ModEq(k,a · f + b · e,0)Definitions: ModEq(k,a · f + b · e,0)Original native command in the exact edition
  2. L90
    specialize four_square_signed_cross_mixed_zero k
  3. L91
    specialize four_square_signed_cross_mixed_zero a
  4. L92
    specialize four_square_signed_cross_mixed_zero b
  5. L93
    specialize four_square_signed_cross_mixed_zero e
  6. L94
    specialize four_square_signed_cross_mixed_zero f
  7. L95
    apply four_square_signed_cross_mixed_zero
  8. L96
    exact ha
  9. L97
    exact hb
18Establish hfirst_crossL98–107

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

  1. L98
    have hfirst_cross : ModEq(k,c · h,d · g)Definitions: ModEq(k,c · h,d · g)Original native command in the exact edition
  2. L99
    specialize four_square_signed_cross_negative k
  3. L100
    specialize four_square_signed_cross_negative c
  4. L101
    specialize four_square_signed_cross_negative d
  5. L102
    specialize four_square_signed_cross_negative g
  6. L103
    specialize four_square_signed_cross_negative h
  7. L104
    apply four_square_signed_cross_negative
  8. L105
    exact hc
  9. L106
    exact hd
  10. L107
    specialize four_square_signed_mod_zero_plus_congruent k
19Use earlier factsL108–113

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

  1. L108
    specialize four_square_signed_mod_zero_plus_congruent (a * f + b * e)
  2. L109
    specialize four_square_signed_mod_zero_plus_congruent (c * h)
  3. L110
    specialize four_square_signed_mod_zero_plus_congruent (d * g)
  4. L111
    apply four_square_signed_mod_zero_plus_congruent
  5. L112
    exact hfirst_zero
  6. L113
    exact hfirst_cross
20Separate the logical casesL114–114

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

  1. L114
    split
21Establish hsecond_zeroL115–123

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed cross mixed zero.

  1. L115
    have hsecond_zero : ModEq(k,a · g + c · e,0)Definitions: ModEq(k,a · g + c · e,0)Original native command in the exact edition
  2. L116
    specialize four_square_signed_cross_mixed_zero k
  3. L117
    specialize four_square_signed_cross_mixed_zero a
  4. L118
    specialize four_square_signed_cross_mixed_zero c
  5. L119
    specialize four_square_signed_cross_mixed_zero e
  6. L120
    specialize four_square_signed_cross_mixed_zero g
  7. L121
    apply four_square_signed_cross_mixed_zero
  8. L122
    exact ha
  9. L123
    exact hc
22Establish hsecond_crossL124–133

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

  1. L124
    have hsecond_cross : ModEq(k,d · f,b · h)Definitions: ModEq(k,d · f,b · h)Original native command in the exact edition
  2. L125
    specialize four_square_signed_cross_negative k
  3. L126
    specialize four_square_signed_cross_negative d
  4. L127
    specialize four_square_signed_cross_negative b
  5. L128
    specialize four_square_signed_cross_negative h
  6. L129
    specialize four_square_signed_cross_negative f
  7. L130
    apply four_square_signed_cross_negative
  8. L131
    exact hd
  9. L132
    exact hb
  10. L133
    specialize four_square_signed_mod_zero_plus_congruent k
23Use earlier factsL134–139

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

  1. L134
    specialize four_square_signed_mod_zero_plus_congruent (a * g + c * e)
  2. L135
    specialize four_square_signed_mod_zero_plus_congruent (d * f)
  3. L136
    specialize four_square_signed_mod_zero_plus_congruent (b * h)
  4. L137
    apply four_square_signed_mod_zero_plus_congruent
  5. L138
    exact hsecond_zero
  6. L139
    exact hsecond_cross
24Establish hthird_zeroL140–148

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed cross mixed zero.

  1. L140
    have hthird_zero : ModEq(k,a · h + d · e,0)Definitions: ModEq(k,a · h + d · e,0)Original native command in the exact edition
  2. L141
    specialize four_square_signed_cross_mixed_zero k
  3. L142
    specialize four_square_signed_cross_mixed_zero a
  4. L143
    specialize four_square_signed_cross_mixed_zero d
  5. L144
    specialize four_square_signed_cross_mixed_zero e
  6. L145
    specialize four_square_signed_cross_mixed_zero h
  7. L146
    apply four_square_signed_cross_mixed_zero
  8. L147
    exact ha
  9. L148
    exact hd
25Establish hthird_crossL149–157

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

  1. L149
    have hthird_cross : ModEq(k,b · g,c · f)Definitions: ModEq(k,b · g,c · f)Original native command in the exact edition
  2. L150
    specialize four_square_signed_cross_negative k
  3. L151
    specialize four_square_signed_cross_negative b
  4. L152
    specialize four_square_signed_cross_negative c
  5. L153
    specialize four_square_signed_cross_negative f
  6. L154
    specialize four_square_signed_cross_negative g
  7. L155
    apply four_square_signed_cross_negative
  8. L156
    exact hb
  9. L157
    exact hc
26Establish hswapL158–167

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square euler add swap last.

  1. L158
    have hswap : (a * h + b * g) + d * e = (a * h + d * e) + b * g
  2. L159
    apply four_square_euler_add_swap_last
  3. L160
    rewrite hswap
  4. L161
    specialize four_square_signed_mod_zero_plus_congruent k
  5. L162
    specialize four_square_signed_mod_zero_plus_congruent (a * h + d * e)
  6. L163
    specialize four_square_signed_mod_zero_plus_congruent (b * g)
  7. L164
    specialize four_square_signed_mod_zero_plus_congruent (c * f)
  8. L165
    apply four_square_signed_mod_zero_plus_congruent
  9. L166
    exact hthird_zero
  10. L167
    exact hthird_cross

Library-wide reading audit

Original defined command ledger · 167 lines
  1. 0001intro k
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro e
  7. 0007intro f
  8. 0008intro g
  9. 0009intro h
  10. 0010intro hnorm
  11. 0011intro ha
  12. 0012intro hb
  13. 0013intro hc
  14. 0014intro hd
  15. 0015split
  16. 0016have hpositive : ModEq(k,a · e,e · e)
    Exact native replay linehave hpositive : exists ftcn_left_fssbn_positive_first_dot ftcn_right_fssbn_positive_first_dot. (a * e) + (k) * ftcn_left_fssbn_positive_first_dot = (e * e) + (k) * ftcn_right_fssbn_positive_first_dot
  17. 0017specialize four_square_signed_dot_positive k
  18. 0018specialize four_square_signed_dot_positive a
  19. 0019specialize four_square_signed_dot_positive e
  20. 0020apply four_square_signed_dot_positive
  21. 0021exact ha
  22. 0022have hdb : ModEq(k,b · f + f · f,0)
    Exact native replay linehave hdb : exists ftcn_left_fssbn_hdb ftcn_right_fssbn_hdb. (b * f + f * f) + (k) * ftcn_left_fssbn_hdb = (0) + (k) * ftcn_right_fssbn_hdb
  23. 0023specialize four_square_signed_dot_negative_zero k
  24. 0024specialize four_square_signed_dot_negative_zero b
  25. 0025specialize four_square_signed_dot_negative_zero f
  26. 0026apply four_square_signed_dot_negative_zero
  27. 0027exact hb
  28. 0028have hdc : ModEq(k,c · g + g · g,0)
    Exact native replay linehave hdc : exists ftcn_left_fssbn_hdc ftcn_right_fssbn_hdc. (c * g + g * g) + (k) * ftcn_left_fssbn_hdc = (0) + (k) * ftcn_right_fssbn_hdc
  29. 0029specialize four_square_signed_dot_negative_zero k
  30. 0030specialize four_square_signed_dot_negative_zero c
  31. 0031specialize four_square_signed_dot_negative_zero g
  32. 0032apply four_square_signed_dot_negative_zero
  33. 0033exact hc
  34. 0034have hdd : ModEq(k,d · h + h · h,0)
    Exact native replay linehave hdd : exists ftcn_left_fssbn_hdd ftcn_right_fssbn_hdd. (d * h + h * h) + (k) * ftcn_left_fssbn_hdd = (0) + (k) * ftcn_right_fssbn_hdd
  35. 0035specialize four_square_signed_dot_negative_zero k
  36. 0036specialize four_square_signed_dot_negative_zero d
  37. 0037specialize four_square_signed_dot_negative_zero h
  38. 0038apply four_square_signed_dot_negative_zero
  39. 0039exact hd
  40. 0040have hbczero : ModEq(k,b · f + f · f + (c · g + g · g),0)
    Exact native replay linehave hbczero : exists ftcn_left_fssbn_hbczero ftcn_right_fssbn_hbczero. ((b * f + f * f) + (c * g + g * g)) + (k) * ftcn_left_fssbn_hbczero = (0) + (k) * ftcn_right_fssbn_hbczero
  41. 0041specialize four_square_signed_mod_zero_add k
  42. 0042specialize four_square_signed_mod_zero_add (b * f + f * f)
  43. 0043specialize four_square_signed_mod_zero_add (c * g + g * g)
  44. 0044apply four_square_signed_mod_zero_add
  45. 0045exact hdb
  46. 0046exact hdc
  47. 0047have hnegative : ModEq(k,b · f + f · f + (c · g + g · g) + (d · h + h · h),0)
    Exact native replay linehave hnegative : exists ftcn_left_fssbn_hnegative ftcn_right_fssbn_hnegative. (((b * f + f * f) + (c * g + g * g)) + (d * h + h * h)) + (k) * ftcn_left_fssbn_hnegative = (0) + (k) * ftcn_right_fssbn_hnegative
  48. 0048specialize four_square_signed_mod_zero_add k
  49. 0049specialize four_square_signed_mod_zero_add ((b * f + f * f) + (c * g + g * g))
  50. 0050specialize four_square_signed_mod_zero_add (d * h + h * h)
  51. 0051apply four_square_signed_mod_zero_add
  52. 0052exact hbczero
  53. 0053exact hdd
  54. 0054have hshuffle : (((b * f + f * f) + (c * g + g * g)) + (d * h + h * h)) = ((b * f + c * g + d * h) + (f * f + g * g + h * h))
  55. 0055trans ((b * f) + ((f * f) + ((c * g) + ((g * g) + ((d * h) + (h * h))))))
  56. 0056simp [add_assoc]
  57. 0057trans ((b * f) + ((c * g) + ((d * h) + ((f * f) + ((g * g) + (h * h))))))
  58. 0058congr
  59. 0059refl
  60. 0060trans ((c * g) + ((f * f) + ((g * g) + ((d * h) + (h * h)))))
  61. 0061apply four_square_add_swap_right_tail
  62. 0062congr
  63. 0063refl
  64. 0064trans ((d * h) + ((f * f) + ((g * g) + (h * h))))
  65. 0065trans ((f * f) + ((d * h) + ((g * g) + (h * h))))
  66. 0066congr
  67. 0067refl
  68. 0068apply four_square_add_swap_right_tail
  69. 0069apply four_square_add_swap_right_tail
  70. 0070congr
  71. 0071refl
  72. 0072refl
  73. 0073symm
  74. 0074simp [add_assoc]
  75. 0075rewrite hshuffle at hnegative
  76. 0076have hnormshape : (e * e + f * f + g * g + h * h) = ((e * e) + (f * f + g * g + h * h))
  77. 0077simp [add_assoc]
  78. 0078rewrite hnormshape at hnorm
  79. 0079specialize four_square_signed_partition_balance k
  80. 0080specialize four_square_signed_partition_balance (a * e)
  81. 0081specialize four_square_signed_partition_balance (e * e)
  82. 0082specialize four_square_signed_partition_balance (b * f + c * g + d * h)
  83. 0083specialize four_square_signed_partition_balance (f * f + g * g + h * h)
  84. 0084apply four_square_signed_partition_balance
  85. 0085exact hpositive
  86. 0086exact hnegative
  87. 0087exact hnorm
  88. 0088split
  89. 0089have hfirst_zero : ModEq(k,a · f + b · e,0)
    Exact native replay linehave hfirst_zero : exists ftcn_left_fssbn_hfirst_zero ftcn_right_fssbn_hfirst_zero. (a * f + b * e) + (k) * ftcn_left_fssbn_hfirst_zero = (0) + (k) * ftcn_right_fssbn_hfirst_zero
  90. 0090specialize four_square_signed_cross_mixed_zero k
  91. 0091specialize four_square_signed_cross_mixed_zero a
  92. 0092specialize four_square_signed_cross_mixed_zero b
  93. 0093specialize four_square_signed_cross_mixed_zero e
  94. 0094specialize four_square_signed_cross_mixed_zero f
  95. 0095apply four_square_signed_cross_mixed_zero
  96. 0096exact ha
  97. 0097exact hb
  98. 0098have hfirst_cross : ModEq(k,c · h,d · g)
    Exact native replay linehave hfirst_cross : exists ftcn_left_fssbn_hfirst_cross ftcn_right_fssbn_hfirst_cross. (c * h) + (k) * ftcn_left_fssbn_hfirst_cross = (d * g) + (k) * ftcn_right_fssbn_hfirst_cross
  99. 0099specialize four_square_signed_cross_negative k
  100. 0100specialize four_square_signed_cross_negative c
  101. 0101specialize four_square_signed_cross_negative d
  102. 0102specialize four_square_signed_cross_negative g
  103. 0103specialize four_square_signed_cross_negative h
  104. 0104apply four_square_signed_cross_negative
  105. 0105exact hc
  106. 0106exact hd
  107. 0107specialize four_square_signed_mod_zero_plus_congruent k
  108. 0108specialize four_square_signed_mod_zero_plus_congruent (a * f + b * e)
  109. 0109specialize four_square_signed_mod_zero_plus_congruent (c * h)
  110. 0110specialize four_square_signed_mod_zero_plus_congruent (d * g)
  111. 0111apply four_square_signed_mod_zero_plus_congruent
  112. 0112exact hfirst_zero
  113. 0113exact hfirst_cross
  114. 0114split
  115. 0115have hsecond_zero : ModEq(k,a · g + c · e,0)
    Exact native replay linehave hsecond_zero : exists ftcn_left_fssbn_hsecond_zero ftcn_right_fssbn_hsecond_zero. (a * g + c * e) + (k) * ftcn_left_fssbn_hsecond_zero = (0) + (k) * ftcn_right_fssbn_hsecond_zero
  116. 0116specialize four_square_signed_cross_mixed_zero k
  117. 0117specialize four_square_signed_cross_mixed_zero a
  118. 0118specialize four_square_signed_cross_mixed_zero c
  119. 0119specialize four_square_signed_cross_mixed_zero e
  120. 0120specialize four_square_signed_cross_mixed_zero g
  121. 0121apply four_square_signed_cross_mixed_zero
  122. 0122exact ha
  123. 0123exact hc
  124. 0124have hsecond_cross : ModEq(k,d · f,b · h)
    Exact native replay linehave hsecond_cross : exists ftcn_left_fssbn_hsecond_cross ftcn_right_fssbn_hsecond_cross. (d * f) + (k) * ftcn_left_fssbn_hsecond_cross = (b * h) + (k) * ftcn_right_fssbn_hsecond_cross
  125. 0125specialize four_square_signed_cross_negative k
  126. 0126specialize four_square_signed_cross_negative d
  127. 0127specialize four_square_signed_cross_negative b
  128. 0128specialize four_square_signed_cross_negative h
  129. 0129specialize four_square_signed_cross_negative f
  130. 0130apply four_square_signed_cross_negative
  131. 0131exact hd
  132. 0132exact hb
  133. 0133specialize four_square_signed_mod_zero_plus_congruent k
  134. 0134specialize four_square_signed_mod_zero_plus_congruent (a * g + c * e)
  135. 0135specialize four_square_signed_mod_zero_plus_congruent (d * f)
  136. 0136specialize four_square_signed_mod_zero_plus_congruent (b * h)
  137. 0137apply four_square_signed_mod_zero_plus_congruent
  138. 0138exact hsecond_zero
  139. 0139exact hsecond_cross
  140. 0140have hthird_zero : ModEq(k,a · h + d · e,0)
    Exact native replay linehave hthird_zero : exists ftcn_left_fssbn_hthird_zero ftcn_right_fssbn_hthird_zero. (a * h + d * e) + (k) * ftcn_left_fssbn_hthird_zero = (0) + (k) * ftcn_right_fssbn_hthird_zero
  141. 0141specialize four_square_signed_cross_mixed_zero k
  142. 0142specialize four_square_signed_cross_mixed_zero a
  143. 0143specialize four_square_signed_cross_mixed_zero d
  144. 0144specialize four_square_signed_cross_mixed_zero e
  145. 0145specialize four_square_signed_cross_mixed_zero h
  146. 0146apply four_square_signed_cross_mixed_zero
  147. 0147exact ha
  148. 0148exact hd
  149. 0149have hthird_cross : ModEq(k,b · g,c · f)
    Exact native replay linehave hthird_cross : exists ftcn_left_fssbn_hthird_cross ftcn_right_fssbn_hthird_cross. (b * g) + (k) * ftcn_left_fssbn_hthird_cross = (c * f) + (k) * ftcn_right_fssbn_hthird_cross
  150. 0150specialize four_square_signed_cross_negative k
  151. 0151specialize four_square_signed_cross_negative b
  152. 0152specialize four_square_signed_cross_negative c
  153. 0153specialize four_square_signed_cross_negative f
  154. 0154specialize four_square_signed_cross_negative g
  155. 0155apply four_square_signed_cross_negative
  156. 0156exact hb
  157. 0157exact hc
  158. 0158have hswap : (a * h + b * g) + d * e = (a * h + d * e) + b * g
  159. 0159apply four_square_euler_add_swap_last
  160. 0160rewrite hswap
  161. 0161specialize four_square_signed_mod_zero_plus_congruent k
  162. 0162specialize four_square_signed_mod_zero_plus_congruent (a * h + d * e)
  163. 0163specialize four_square_signed_mod_zero_plus_congruent (b * g)
  164. 0164specialize four_square_signed_mod_zero_plus_congruent (c * f)
  165. 0165apply four_square_signed_mod_zero_plus_congruent
  166. 0166exact hthird_zero
  167. 0167exact hthird_cross