FS0060 · theorem body

four_square_signed_natural_negative_first_blocks

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

All four canonical signed quaternion blocks balance constructively modulo the multiplier under this exact orientation pattern.

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,0) → ModEq(k,b,f) → ModEq(k,c,g) → ModEq(k,d,h) → 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_fssq_surface_four_square_signed_natural_negative_first_blocks_norm ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_norm. (e * e + f * f + g * g + h * h) + (k) * ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_norm = (0) + (k) * ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_norm) -> (exists ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_0 ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_0. (a + e) + (k) * ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_0 = (0) + (k) * ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_0) -> (exists ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_1 ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_1. (b) + (k) * ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_1 = (f) + (k) * ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_1) -> (exists ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_2 ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_2. (c) + (k) * ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_2 = (g) + (k) * ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_2) -> (exists ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_3 ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_3. (d) + (k) * ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_3 = (h) + (k) * ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_3) -> ((exists ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_block_0 ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_block_0. (a * e) + (k) * ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_block_0 = (b * f + c * g + d * h) + (k) * ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_block_0) /\ ((exists ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_block_1 ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_block_1. (a * f + b * e + c * h) + (k) * ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_block_1 = (d * g) + (k) * ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_block_1) /\ ((exists ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_block_2 ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_block_2. (a * g + c * e + d * f) + (k) * ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_block_2 = (b * h) + (k) * ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_block_2) /\ (exists ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_block_3 ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_block_3. (a * h + b * g + d * e) + (k) * ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_block_3 = (c * f) + (k) * ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_block_3))))

Proof neighborhood

Direct theorem prerequisites

FS005M four_square_signed_cross_positive FS005N four_square_signed_cross_negative FS005O four_square_signed_cross_mixed_zero FS005T four_square_signed_cross_mixed_zero_reversed FS005U four_square_signed_dot_positive FS005V four_square_signed_dot_negative_zero FS005P four_square_signed_mod_zero_add FS005Q four_square_signed_mod_zero_equivalent FS005W four_square_signed_mod_zero_plus_congruent FS005X four_square_signed_partition_balance mod_eq_add · Stable closed mod_eq_symm · Stable closed mod_eq_trans · Stable closed add_assoc · Stable closed add_comm · Stable closed FS0006 four_square_add_swap_right_tail

Direct theorem dependents

FS004R four_square_signed_orientation_mask_01 FS004S four_square_signed_orientation_mask_02 FS004U four_square_signed_orientation_mask_04 FS004Y four_square_signed_orientation_mask_08

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

201 script commands · 34 reading checkpoints · 22 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 (7)
four square signed cross positivefour square signed cross mixed zero reversedfour square signed dot positivefour square signed dot negative zerofour square signed mod zero plus congruentfour square signed partition balancefour square add swap right tail
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 horient0
  2. L12
    intro horient1
  3. L13
    intro horient2
  4. L14
    intro horient3
03Establish hpair01L15–23

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

  1. L15
    have hpair01 : ModEq(k,a · f + b · e,0)Definitions: ModEq(k,a · f + b · e,0)Original native command in the exact edition
  2. L16
    specialize four_square_signed_cross_mixed_zero_reversed k
  3. L17
    specialize four_square_signed_cross_mixed_zero_reversed a
  4. L18
    specialize four_square_signed_cross_mixed_zero_reversed b
  5. L19
    specialize four_square_signed_cross_mixed_zero_reversed e
  6. L20
    specialize four_square_signed_cross_mixed_zero_reversed f
  7. L21
    apply four_square_signed_cross_mixed_zero_reversed
  8. L22
    exact horient0
  9. L23
    exact horient1
04Establish hpair02L24–32

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

  1. L24
    have hpair02 : ModEq(k,a · g + c · e,0)Definitions: ModEq(k,a · g + c · e,0)Original native command in the exact edition
  2. L25
    specialize four_square_signed_cross_mixed_zero_reversed k
  3. L26
    specialize four_square_signed_cross_mixed_zero_reversed a
  4. L27
    specialize four_square_signed_cross_mixed_zero_reversed c
  5. L28
    specialize four_square_signed_cross_mixed_zero_reversed e
  6. L29
    specialize four_square_signed_cross_mixed_zero_reversed g
  7. L30
    apply four_square_signed_cross_mixed_zero_reversed
  8. L31
    exact horient0
  9. L32
    exact horient2
05Establish hpair03L33–41

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

  1. L33
    have hpair03 : ModEq(k,a · h + d · e,0)Definitions: ModEq(k,a · h + d · e,0)Original native command in the exact edition
  2. L34
    specialize four_square_signed_cross_mixed_zero_reversed k
  3. L35
    specialize four_square_signed_cross_mixed_zero_reversed a
  4. L36
    specialize four_square_signed_cross_mixed_zero_reversed d
  5. L37
    specialize four_square_signed_cross_mixed_zero_reversed e
  6. L38
    specialize four_square_signed_cross_mixed_zero_reversed h
  7. L39
    apply four_square_signed_cross_mixed_zero_reversed
  8. L40
    exact horient0
  9. L41
    exact horient3
06Establish hpair12L42–50

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

  1. L42
    have hpair12 : ModEq(k,b · g,c · f)Definitions: ModEq(k,b · g,c · f)Original native command in the exact edition
  2. L43
    specialize four_square_signed_cross_positive k
  3. L44
    specialize four_square_signed_cross_positive b
  4. L45
    specialize four_square_signed_cross_positive c
  5. L46
    specialize four_square_signed_cross_positive f
  6. L47
    specialize four_square_signed_cross_positive g
  7. L48
    apply four_square_signed_cross_positive
  8. L49
    exact horient1
  9. L50
    exact horient2
07Establish hpair13L51–59

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

  1. L51
    have hpair13 : ModEq(k,b · h,d · f)Definitions: ModEq(k,b · h,d · f)Original native command in the exact edition
  2. L52
    specialize four_square_signed_cross_positive k
  3. L53
    specialize four_square_signed_cross_positive b
  4. L54
    specialize four_square_signed_cross_positive d
  5. L55
    specialize four_square_signed_cross_positive f
  6. L56
    specialize four_square_signed_cross_positive h
  7. L57
    apply four_square_signed_cross_positive
  8. L58
    exact horient1
  9. L59
    exact horient3
08Establish hpair23L60–68

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

  1. L60
    have hpair23 : ModEq(k,c · h,d · g)Definitions: ModEq(k,c · h,d · g)Original native command in the exact edition
  2. L61
    specialize four_square_signed_cross_positive k
  3. L62
    specialize four_square_signed_cross_positive c
  4. L63
    specialize four_square_signed_cross_positive d
  5. L64
    specialize four_square_signed_cross_positive g
  6. L65
    specialize four_square_signed_cross_positive h
  7. L66
    apply four_square_signed_cross_positive
  8. L67
    exact horient2
  9. L68
    exact horient3
09Establish hdot1L69–74

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

  1. L69
    have hdot1 : ModEq(k,b · f,f · f)Definitions: ModEq(k,b · f,f · f)Original native command in the exact edition
  2. L70
    specialize four_square_signed_dot_positive k
  3. L71
    specialize four_square_signed_dot_positive b
  4. L72
    specialize four_square_signed_dot_positive f
  5. L73
    apply four_square_signed_dot_positive
  6. L74
    exact horient1
10Establish hdot2L75–80

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

  1. L75
    have hdot2 : ModEq(k,c · g,g · g)Definitions: ModEq(k,c · g,g · g)Original native command in the exact edition
  2. L76
    specialize four_square_signed_dot_positive k
  3. L77
    specialize four_square_signed_dot_positive c
  4. L78
    specialize four_square_signed_dot_positive g
  5. L79
    apply four_square_signed_dot_positive
  6. L80
    exact horient2
11Establish hdot3L81–86

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

  1. L81
    have hdot3 : ModEq(k,d · h,h · h)Definitions: ModEq(k,d · h,h · h)Original native command in the exact edition
  2. L82
    specialize four_square_signed_dot_positive k
  3. L83
    specialize four_square_signed_dot_positive d
  4. L84
    specialize four_square_signed_dot_positive h
  5. L85
    apply four_square_signed_dot_positive
  6. L86
    exact horient3
12Establish hpositive2L87–95

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

  1. L87
    have hpositive2 : ModEq(k,b · f + c · g,f · f + g · g)Definitions: ModEq(k,b · f + c · g,f · f + g · g)Original native command in the exact edition
  2. L88
    specialize mod_eq_add k
  3. L89
    specialize mod_eq_add (b * f)
  4. L90
    specialize mod_eq_add (f * f)
  5. L91
    specialize mod_eq_add (c * g)
  6. L92
    specialize mod_eq_add (g * g)
  7. L93
    apply mod_eq_add
  8. L94
    exact hdot1
  9. L95
    exact hdot2
13Establish hpositive3L96–104

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

  1. L96
    have hpositive3 : ModEq(k,b · f + c · g + d · h,f · f + g · g + h · h)Definitions: ModEq(k,b · f + c · g + d · h,f · f + g · g + h · h)Original native command in the exact edition
  2. L97
    specialize mod_eq_add k
  3. L98
    specialize mod_eq_add ((b * f) + (c * g))
  4. L99
    specialize mod_eq_add ((f * f) + (g * g))
  5. L100
    specialize mod_eq_add (d * h)
  6. L101
    specialize mod_eq_add (h * h)
  7. L102
    apply mod_eq_add
  8. L103
    exact hpositive2
  9. L104
    exact hdot3
14Establish hdot0L105–110

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. L105
    have hdot0 : ModEq(k,a · e + e · e,0)Definitions: ModEq(k,a · e + e · e,0)Original native command in the exact edition
  2. L106
    specialize four_square_signed_dot_negative_zero k
  3. L107
    specialize four_square_signed_dot_negative_zero a
  4. L108
    specialize four_square_signed_dot_negative_zero e
  5. L109
    apply four_square_signed_dot_negative_zero
  6. L110
    exact horient0
15Establish hnorm_shuffleL111–120

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

  1. L111
    have hnorm_shuffle : ((((f * f) + (g * g)) + (h * h)) + (e * e)) = (e * e + f * f + g * g + h * h)
  2. L112
    trans ((f * f) + ((g * g) + ((h * h) + (e * e))))
  3. L113
    simp [add_assoc]
  4. L114
    trans ((e * e) + ((f * f) + ((g * g) + (h * h))))
  5. L115
    trans ((e * e) + ((f * f) + ((g * g) + (h * h))))
  6. L116
    trans ((f * f) + ((e * e) + ((g * g) + (h * h))))
  7. L117
    congr
  8. L118
    refl
  9. L119
    trans ((g * g) + ((e * e) + (h * h)))
  10. L120
    congr
16Calculate and transport equalitiesL121–121

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

  1. L121
    refl
17Use earlier factsL122–124

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

  1. L122
    apply add_comm
  2. L123
    apply four_square_add_swap_right_tail
  3. L124
    apply four_square_add_swap_right_tail
18Calculate and transport equalitiesL125–129

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

  1. L125
    congr
  2. L126
    refl
  3. L127
    refl
  4. L128
    symm
  5. L129
    simp [add_assoc]
19Establish hordered_normL130–132

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

  1. L130
    have hordered_norm : ModEq(k,f · f + g · g + h · h + e · e,0)Definitions: ModEq(k,f · f + g · g + h · h + e · e,0)Original native command in the exact edition
  2. L131
    rewrite hnorm_shuffle
  3. L132
    exact hnorm
20Establish hpartitionL133–142

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

  1. L133
    have hpartition : ModEq(k,b · f + c · g + d · h,a · e)Definitions: ModEq(k,b · f + c · g + d · h,a · e)Original native command in the exact edition
  2. L134
    specialize four_square_signed_partition_balance k
  3. L135
    specialize four_square_signed_partition_balance (((b * f) + (c * g)) + (d * h))
  4. L136
    specialize four_square_signed_partition_balance (((f * f) + (g * g)) + (h * h))
  5. L137
    specialize four_square_signed_partition_balance (a * e)
  6. L138
    specialize four_square_signed_partition_balance (e * e)
  7. L139
    apply four_square_signed_partition_balance
  8. L140
    exact hpositive3
  9. L141
    exact hdot0
  10. L142
    exact hordered_norm
21Establish hblock0L143–148

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq symm.

  1. L143
    have hblock0 : ModEq(k,a · e,b · f + c · g + d · h)Definitions: ModEq(k,a · e,b · f + c · g + d · h)Original native command in the exact edition
  2. L144
    specialize mod_eq_symm k
  3. L145
    specialize mod_eq_symm (((b * f) + (c * g)) + (d * h))
  4. L146
    specialize mod_eq_symm (a * e)
  5. L147
    apply mod_eq_symm
  6. L148
    exact hpartition
22Establish hblock1L149–156

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

  1. L149
    have hblock1 : ModEq(k,a · f + b · e + c · h,d · g)Definitions: ModEq(k,a · f + b · e + c · h,d · g)Original native command in the exact edition
  2. L150
    specialize four_square_signed_mod_zero_plus_congruent k
  3. L151
    specialize four_square_signed_mod_zero_plus_congruent (a * f + b * e)
  4. L152
    specialize four_square_signed_mod_zero_plus_congruent (c * h)
  5. L153
    specialize four_square_signed_mod_zero_plus_congruent (d * g)
  6. L154
    apply four_square_signed_mod_zero_plus_congruent
  7. L155
    exact hpair01
  8. L156
    exact hpair23
23Establish hpair13_reverseL157–162

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq symm.

  1. L157
    have hpair13_reverse : ModEq(k,d · f,b · h)Definitions: ModEq(k,d · f,b · h)Original native command in the exact edition
  2. L158
    specialize mod_eq_symm k
  3. L159
    specialize mod_eq_symm (b * h)
  4. L160
    specialize mod_eq_symm (d * f)
  5. L161
    apply mod_eq_symm
  6. L162
    exact hpair13
24Establish hblock2L163–170

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

  1. L163
    have hblock2 : ModEq(k,a · g + c · e + d · f,b · h)Definitions: ModEq(k,a · g + c · e + d · f,b · h)Original native command in the exact edition
  2. L164
    specialize four_square_signed_mod_zero_plus_congruent k
  3. L165
    specialize four_square_signed_mod_zero_plus_congruent (a * g + c * e)
  4. L166
    specialize four_square_signed_mod_zero_plus_congruent (d * f)
  5. L167
    specialize four_square_signed_mod_zero_plus_congruent (b * h)
  6. L168
    apply four_square_signed_mod_zero_plus_congruent
  7. L169
    exact hpair02
  8. L170
    exact hpair13_reverse
25Establish hblock3_reorderedL171–178

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

  1. L171
    have hblock3_reordered : ModEq(k,a · h + d · e + b · g,c · f)Definitions: ModEq(k,a · h + d · e + b · g,c · f)Original native command in the exact edition
  2. L172
    specialize four_square_signed_mod_zero_plus_congruent k
  3. L173
    specialize four_square_signed_mod_zero_plus_congruent (a * h + d * e)
  4. L174
    specialize four_square_signed_mod_zero_plus_congruent (b * g)
  5. L175
    specialize four_square_signed_mod_zero_plus_congruent (c * f)
  6. L176
    apply four_square_signed_mod_zero_plus_congruent
  7. L177
    exact hpair03
  8. L178
    exact hpair12
26Establish hblock3_shuffleL179–188

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add comm.

  1. L179
    have hblock3_shuffle : (a * h + d * e) + b * g = a * h + b * g + d * e
  2. L180
    trans ((a * h) + ((d * e) + (b * g)))
  3. L181
    simp [add_assoc]
  4. L182
    trans ((a * h) + ((b * g) + (d * e)))
  5. L183
    congr
  6. L184
    refl
  7. L185
    trans ((b * g) + (d * e))
  8. L186
    apply add_comm
  9. L187
    congr
  10. L188
    refl
27Calculate and transport equalitiesL189–192

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

  1. L189
    refl
  2. L190
    symm
  3. L191
    simp [add_assoc]
  4. L192
    rewrite hblock3_shuffle at hblock3_reordered
28Establish hblock3L193–194

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

  1. L193
    have hblock3 : ModEq(k,a · h + b · g + d · e,c · f)Definitions: ModEq(k,a · h + b · g + d · e,c · f)Original native command in the exact edition
  2. L194
    exact hblock3_reordered
29Separate the logical casesL195–195

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

  1. L195
    split
30Use earlier factsL196–196

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

  1. L196
    exact hblock0
31Separate the logical casesL197–197

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

  1. L197
    split
32Use earlier factsL198–198

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

  1. L198
    exact hblock1
33Separate the logical casesL199–199

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

  1. L199
    split
34Use earlier factsL200–201

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

  1. L200
    exact hblock2
  2. L201
    exact hblock3

Library-wide reading audit

Original defined command ledger · 201 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 horient0
  12. 0012intro horient1
  13. 0013intro horient2
  14. 0014intro horient3
  15. 0015have hpair01 : ModEq(k,a · f + b · e,0)
    Exact native replay linehave hpair01 : exists ftcn_left_fssq_surface_pair_01 ftcn_right_fssq_surface_pair_01. (a * f + b * e) + (k) * ftcn_left_fssq_surface_pair_01 = (0) + (k) * ftcn_right_fssq_surface_pair_01
  16. 0016specialize four_square_signed_cross_mixed_zero_reversed k
  17. 0017specialize four_square_signed_cross_mixed_zero_reversed a
  18. 0018specialize four_square_signed_cross_mixed_zero_reversed b
  19. 0019specialize four_square_signed_cross_mixed_zero_reversed e
  20. 0020specialize four_square_signed_cross_mixed_zero_reversed f
  21. 0021apply four_square_signed_cross_mixed_zero_reversed
  22. 0022exact horient0
  23. 0023exact horient1
  24. 0024have hpair02 : ModEq(k,a · g + c · e,0)
    Exact native replay linehave hpair02 : exists ftcn_left_fssq_surface_pair_02 ftcn_right_fssq_surface_pair_02. (a * g + c * e) + (k) * ftcn_left_fssq_surface_pair_02 = (0) + (k) * ftcn_right_fssq_surface_pair_02
  25. 0025specialize four_square_signed_cross_mixed_zero_reversed k
  26. 0026specialize four_square_signed_cross_mixed_zero_reversed a
  27. 0027specialize four_square_signed_cross_mixed_zero_reversed c
  28. 0028specialize four_square_signed_cross_mixed_zero_reversed e
  29. 0029specialize four_square_signed_cross_mixed_zero_reversed g
  30. 0030apply four_square_signed_cross_mixed_zero_reversed
  31. 0031exact horient0
  32. 0032exact horient2
  33. 0033have hpair03 : ModEq(k,a · h + d · e,0)
    Exact native replay linehave hpair03 : exists ftcn_left_fssq_surface_pair_03 ftcn_right_fssq_surface_pair_03. (a * h + d * e) + (k) * ftcn_left_fssq_surface_pair_03 = (0) + (k) * ftcn_right_fssq_surface_pair_03
  34. 0034specialize four_square_signed_cross_mixed_zero_reversed k
  35. 0035specialize four_square_signed_cross_mixed_zero_reversed a
  36. 0036specialize four_square_signed_cross_mixed_zero_reversed d
  37. 0037specialize four_square_signed_cross_mixed_zero_reversed e
  38. 0038specialize four_square_signed_cross_mixed_zero_reversed h
  39. 0039apply four_square_signed_cross_mixed_zero_reversed
  40. 0040exact horient0
  41. 0041exact horient3
  42. 0042have hpair12 : ModEq(k,b · g,c · f)
    Exact native replay linehave hpair12 : exists ftcn_left_fssq_surface_pair_12 ftcn_right_fssq_surface_pair_12. (b * g) + (k) * ftcn_left_fssq_surface_pair_12 = (c * f) + (k) * ftcn_right_fssq_surface_pair_12
  43. 0043specialize four_square_signed_cross_positive k
  44. 0044specialize four_square_signed_cross_positive b
  45. 0045specialize four_square_signed_cross_positive c
  46. 0046specialize four_square_signed_cross_positive f
  47. 0047specialize four_square_signed_cross_positive g
  48. 0048apply four_square_signed_cross_positive
  49. 0049exact horient1
  50. 0050exact horient2
  51. 0051have hpair13 : ModEq(k,b · h,d · f)
    Exact native replay linehave hpair13 : exists ftcn_left_fssq_surface_pair_13 ftcn_right_fssq_surface_pair_13. (b * h) + (k) * ftcn_left_fssq_surface_pair_13 = (d * f) + (k) * ftcn_right_fssq_surface_pair_13
  52. 0052specialize four_square_signed_cross_positive k
  53. 0053specialize four_square_signed_cross_positive b
  54. 0054specialize four_square_signed_cross_positive d
  55. 0055specialize four_square_signed_cross_positive f
  56. 0056specialize four_square_signed_cross_positive h
  57. 0057apply four_square_signed_cross_positive
  58. 0058exact horient1
  59. 0059exact horient3
  60. 0060have hpair23 : ModEq(k,c · h,d · g)
    Exact native replay linehave hpair23 : exists ftcn_left_fssq_surface_pair_23 ftcn_right_fssq_surface_pair_23. (c * h) + (k) * ftcn_left_fssq_surface_pair_23 = (d * g) + (k) * ftcn_right_fssq_surface_pair_23
  61. 0061specialize four_square_signed_cross_positive k
  62. 0062specialize four_square_signed_cross_positive c
  63. 0063specialize four_square_signed_cross_positive d
  64. 0064specialize four_square_signed_cross_positive g
  65. 0065specialize four_square_signed_cross_positive h
  66. 0066apply four_square_signed_cross_positive
  67. 0067exact horient2
  68. 0068exact horient3
  69. 0069have hdot1 : ModEq(k,b · f,f · f)
    Exact native replay linehave hdot1 : exists ftcn_left_fssq_surface_dot_1 ftcn_right_fssq_surface_dot_1. (b * f) + (k) * ftcn_left_fssq_surface_dot_1 = (f * f) + (k) * ftcn_right_fssq_surface_dot_1
  70. 0070specialize four_square_signed_dot_positive k
  71. 0071specialize four_square_signed_dot_positive b
  72. 0072specialize four_square_signed_dot_positive f
  73. 0073apply four_square_signed_dot_positive
  74. 0074exact horient1
  75. 0075have hdot2 : ModEq(k,c · g,g · g)
    Exact native replay linehave hdot2 : exists ftcn_left_fssq_surface_dot_2 ftcn_right_fssq_surface_dot_2. (c * g) + (k) * ftcn_left_fssq_surface_dot_2 = (g * g) + (k) * ftcn_right_fssq_surface_dot_2
  76. 0076specialize four_square_signed_dot_positive k
  77. 0077specialize four_square_signed_dot_positive c
  78. 0078specialize four_square_signed_dot_positive g
  79. 0079apply four_square_signed_dot_positive
  80. 0080exact horient2
  81. 0081have hdot3 : ModEq(k,d · h,h · h)
    Exact native replay linehave hdot3 : exists ftcn_left_fssq_surface_dot_3 ftcn_right_fssq_surface_dot_3. (d * h) + (k) * ftcn_left_fssq_surface_dot_3 = (h * h) + (k) * ftcn_right_fssq_surface_dot_3
  82. 0082specialize four_square_signed_dot_positive k
  83. 0083specialize four_square_signed_dot_positive d
  84. 0084specialize four_square_signed_dot_positive h
  85. 0085apply four_square_signed_dot_positive
  86. 0086exact horient3
  87. 0087have hpositive2 : ModEq(k,b · f + c · g,f · f + g · g)
    Exact native replay linehave hpositive2 : exists ftcn_left_fssq_surface_hpositive2 ftcn_right_fssq_surface_hpositive2. ((b * f) + (c * g)) + (k) * ftcn_left_fssq_surface_hpositive2 = ((f * f) + (g * g)) + (k) * ftcn_right_fssq_surface_hpositive2
  88. 0088specialize mod_eq_add k
  89. 0089specialize mod_eq_add (b * f)
  90. 0090specialize mod_eq_add (f * f)
  91. 0091specialize mod_eq_add (c * g)
  92. 0092specialize mod_eq_add (g * g)
  93. 0093apply mod_eq_add
  94. 0094exact hdot1
  95. 0095exact hdot2
  96. 0096have hpositive3 : ModEq(k,b · f + c · g + d · h,f · f + g · g + h · h)
    Exact native replay linehave hpositive3 : exists ftcn_left_fssq_surface_hpositive3 ftcn_right_fssq_surface_hpositive3. (((b * f) + (c * g)) + (d * h)) + (k) * ftcn_left_fssq_surface_hpositive3 = (((f * f) + (g * g)) + (h * h)) + (k) * ftcn_right_fssq_surface_hpositive3
  97. 0097specialize mod_eq_add k
  98. 0098specialize mod_eq_add ((b * f) + (c * g))
  99. 0099specialize mod_eq_add ((f * f) + (g * g))
  100. 0100specialize mod_eq_add (d * h)
  101. 0101specialize mod_eq_add (h * h)
  102. 0102apply mod_eq_add
  103. 0103exact hpositive2
  104. 0104exact hdot3
  105. 0105have hdot0 : ModEq(k,a · e + e · e,0)
    Exact native replay linehave hdot0 : exists ftcn_left_fssq_surface_dot_0 ftcn_right_fssq_surface_dot_0. (a * e + e * e) + (k) * ftcn_left_fssq_surface_dot_0 = (0) + (k) * ftcn_right_fssq_surface_dot_0
  106. 0106specialize four_square_signed_dot_negative_zero k
  107. 0107specialize four_square_signed_dot_negative_zero a
  108. 0108specialize four_square_signed_dot_negative_zero e
  109. 0109apply four_square_signed_dot_negative_zero
  110. 0110exact horient0
  111. 0111have hnorm_shuffle : ((((f * f) + (g * g)) + (h * h)) + (e * e)) = (e * e + f * f + g * g + h * h)
  112. 0112trans ((f * f) + ((g * g) + ((h * h) + (e * e))))
  113. 0113simp [add_assoc]
  114. 0114trans ((e * e) + ((f * f) + ((g * g) + (h * h))))
  115. 0115trans ((e * e) + ((f * f) + ((g * g) + (h * h))))
  116. 0116trans ((f * f) + ((e * e) + ((g * g) + (h * h))))
  117. 0117congr
  118. 0118refl
  119. 0119trans ((g * g) + ((e * e) + (h * h)))
  120. 0120congr
  121. 0121refl
  122. 0122apply add_comm
  123. 0123apply four_square_add_swap_right_tail
  124. 0124apply four_square_add_swap_right_tail
  125. 0125congr
  126. 0126refl
  127. 0127refl
  128. 0128symm
  129. 0129simp [add_assoc]
  130. 0130have hordered_norm : ModEq(k,f · f + g · g + h · h + e · e,0)
    Exact native replay linehave hordered_norm : exists ftcn_left_fssq_surface_ordered_norm ftcn_right_fssq_surface_ordered_norm. ((((f * f) + (g * g)) + (h * h)) + (e * e)) + (k) * ftcn_left_fssq_surface_ordered_norm = (0) + (k) * ftcn_right_fssq_surface_ordered_norm
  131. 0131rewrite hnorm_shuffle
  132. 0132exact hnorm
  133. 0133have hpartition : ModEq(k,b · f + c · g + d · h,a · e)
    Exact native replay linehave hpartition : exists ftcn_left_fssq_surface_partition ftcn_right_fssq_surface_partition. (((b * f) + (c * g)) + (d * h)) + (k) * ftcn_left_fssq_surface_partition = (a * e) + (k) * ftcn_right_fssq_surface_partition
  134. 0134specialize four_square_signed_partition_balance k
  135. 0135specialize four_square_signed_partition_balance (((b * f) + (c * g)) + (d * h))
  136. 0136specialize four_square_signed_partition_balance (((f * f) + (g * g)) + (h * h))
  137. 0137specialize four_square_signed_partition_balance (a * e)
  138. 0138specialize four_square_signed_partition_balance (e * e)
  139. 0139apply four_square_signed_partition_balance
  140. 0140exact hpositive3
  141. 0141exact hdot0
  142. 0142exact hordered_norm
  143. 0143have hblock0 : ModEq(k,a · e,b · f + c · g + d · h)
    Exact native replay linehave hblock0 : exists ftcn_left_fssq_surface_hblock0 ftcn_right_fssq_surface_hblock0. (a * e) + (k) * ftcn_left_fssq_surface_hblock0 = (((b * f) + (c * g)) + (d * h)) + (k) * ftcn_right_fssq_surface_hblock0
  144. 0144specialize mod_eq_symm k
  145. 0145specialize mod_eq_symm (((b * f) + (c * g)) + (d * h))
  146. 0146specialize mod_eq_symm (a * e)
  147. 0147apply mod_eq_symm
  148. 0148exact hpartition
  149. 0149have hblock1 : ModEq(k,a · f + b · e + c · h,d · g)
    Exact native replay linehave hblock1 : exists ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_block_1 ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_block_1. (a * f + b * e + c * h) + (k) * ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_block_1 = (d * g) + (k) * ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_block_1
  150. 0150specialize four_square_signed_mod_zero_plus_congruent k
  151. 0151specialize four_square_signed_mod_zero_plus_congruent (a * f + b * e)
  152. 0152specialize four_square_signed_mod_zero_plus_congruent (c * h)
  153. 0153specialize four_square_signed_mod_zero_plus_congruent (d * g)
  154. 0154apply four_square_signed_mod_zero_plus_congruent
  155. 0155exact hpair01
  156. 0156exact hpair23
  157. 0157have hpair13_reverse : ModEq(k,d · f,b · h)
    Exact native replay linehave hpair13_reverse : exists ftcn_left_fssq_surface_hpair13_reverse ftcn_right_fssq_surface_hpair13_reverse. (d * f) + (k) * ftcn_left_fssq_surface_hpair13_reverse = (b * h) + (k) * ftcn_right_fssq_surface_hpair13_reverse
  158. 0158specialize mod_eq_symm k
  159. 0159specialize mod_eq_symm (b * h)
  160. 0160specialize mod_eq_symm (d * f)
  161. 0161apply mod_eq_symm
  162. 0162exact hpair13
  163. 0163have hblock2 : ModEq(k,a · g + c · e + d · f,b · h)
    Exact native replay linehave hblock2 : exists ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_block_2 ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_block_2. (a * g + c * e + d * f) + (k) * ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_block_2 = (b * h) + (k) * ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_block_2
  164. 0164specialize four_square_signed_mod_zero_plus_congruent k
  165. 0165specialize four_square_signed_mod_zero_plus_congruent (a * g + c * e)
  166. 0166specialize four_square_signed_mod_zero_plus_congruent (d * f)
  167. 0167specialize four_square_signed_mod_zero_plus_congruent (b * h)
  168. 0168apply four_square_signed_mod_zero_plus_congruent
  169. 0169exact hpair02
  170. 0170exact hpair13_reverse
  171. 0171have hblock3_reordered : ModEq(k,a · h + d · e + b · g,c · f)
    Exact native replay linehave hblock3_reordered : exists ftcn_left_fssq_surface_natural_reordered ftcn_right_fssq_surface_natural_reordered. ((a * h + d * e) + b * g) + (k) * ftcn_left_fssq_surface_natural_reordered = (c * f) + (k) * ftcn_right_fssq_surface_natural_reordered
  172. 0172specialize four_square_signed_mod_zero_plus_congruent k
  173. 0173specialize four_square_signed_mod_zero_plus_congruent (a * h + d * e)
  174. 0174specialize four_square_signed_mod_zero_plus_congruent (b * g)
  175. 0175specialize four_square_signed_mod_zero_plus_congruent (c * f)
  176. 0176apply four_square_signed_mod_zero_plus_congruent
  177. 0177exact hpair03
  178. 0178exact hpair12
  179. 0179have hblock3_shuffle : (a * h + d * e) + b * g = a * h + b * g + d * e
  180. 0180trans ((a * h) + ((d * e) + (b * g)))
  181. 0181simp [add_assoc]
  182. 0182trans ((a * h) + ((b * g) + (d * e)))
  183. 0183congr
  184. 0184refl
  185. 0185trans ((b * g) + (d * e))
  186. 0186apply add_comm
  187. 0187congr
  188. 0188refl
  189. 0189refl
  190. 0190symm
  191. 0191simp [add_assoc]
  192. 0192rewrite hblock3_shuffle at hblock3_reordered
  193. 0193have hblock3 : ModEq(k,a · h + b · g + d · e,c · f)
    Exact native replay linehave hblock3 : exists ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_block_3 ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_block_3. (a * h + b * g + d * e) + (k) * ftcn_left_fssq_surface_four_square_signed_natural_negative_first_blocks_block_3 = (c * f) + (k) * ftcn_right_fssq_surface_four_square_signed_natural_negative_first_blocks_block_3
  194. 0194exact hblock3_reordered
  195. 0195split
  196. 0196exact hblock0
  197. 0197split
  198. 0198exact hblock1
  199. 0199split
  200. 0200exact hblock2
  201. 0201exact hblock3