FS005Z

four_square_signed_conjugate_mixed_blocks

Alpha v34 independently verified · alpha_closed; checked-use authorized; 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.

Exact expanded first-order arithmetic statement

forall k a b c d e f g h. (exists ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_norm ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_norm. (e * e + f * f + g * g + h * h) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_norm = (0) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_norm) -> (exists ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_0 ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_0. (a + e) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_0 = (0) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_0) -> (exists ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_1 ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_1. (b + f) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_1 = (0) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_1) -> (exists ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_2 ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_2. (c) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_2 = (g) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_2) -> (exists ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_3 ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_3. (d) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_3 = (h) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_3) -> ((exists ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_0 ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_0. (a * h + b * g + c * f + d * e) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_0 = (0) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_0) /\ ((exists ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_1 ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_1. (a * g + c * e) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_1 = (b * h + d * f) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_1) /\ ((exists ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_2 ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_2. (a * f + d * g) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_2 = (c * h + b * e) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_2) /\ (exists ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_3 ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_3. (a * e + b * f) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_3 = (d * h + c * g) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_3))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 16 declared prerequisites and contains 230 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

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 theorem; checked-use authorized mod_eq_symm Stable theorem; checked-use authorized mod_eq_trans Stable theorem; checked-use authorized add_assoc Stable theorem; checked-use authorized add_comm Stable theorem; checked-use authorized FS0006 four_square_add_swap_right_tail

Direct dependents

FS004T four_square_signed_orientation_mask_03 FS004V four_square_signed_orientation_mask_05 FS004W four_square_signed_orientation_mask_06 FS004Z four_square_signed_orientation_mask_09 FS0050 four_square_signed_orientation_mask_10 FS0052 four_square_signed_orientation_mask_12

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

230 script commands · 42 reading checkpoints · 27 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.

Named ingredients (9)
four square signed cross positivefour square signed cross negativefour square signed cross mixed zero reversedfour square signed dot positivefour square signed dot negative zerofour square signed mod zero addfour square signed mod zero equivalentfour 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 negative.

  1. L15
    have hpair01 : exists ftcn_left_fssq_surface_pair_01 ftcn_right_fssq_surface_pair_01. (a * f) + (k) * ftcn_left_fssq_surface_pair_01 = (b * e) + (k) * ftcn_right_fssq_surface_pair_01
  2. L16
    specialize four_square_signed_cross_negative k
  3. L17
    specialize four_square_signed_cross_negative a
  4. L18
    specialize four_square_signed_cross_negative b
  5. L19
    specialize four_square_signed_cross_negative e
  6. L20
    specialize four_square_signed_cross_negative f
  7. L21
    apply four_square_signed_cross_negative
  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 : 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
  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 : 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
  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 mixed zero reversed.

  1. L42
    have hpair12 : exists ftcn_left_fssq_surface_pair_12 ftcn_right_fssq_surface_pair_12. (b * g + c * f) + (k) * ftcn_left_fssq_surface_pair_12 = (0) + (k) * ftcn_right_fssq_surface_pair_12
  2. L43
    specialize four_square_signed_cross_mixed_zero_reversed k
  3. L44
    specialize four_square_signed_cross_mixed_zero_reversed b
  4. L45
    specialize four_square_signed_cross_mixed_zero_reversed c
  5. L46
    specialize four_square_signed_cross_mixed_zero_reversed f
  6. L47
    specialize four_square_signed_cross_mixed_zero_reversed g
  7. L48
    apply four_square_signed_cross_mixed_zero_reversed
  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 mixed zero reversed.

  1. L51
    have hpair13 : exists ftcn_left_fssq_surface_pair_13 ftcn_right_fssq_surface_pair_13. (b * h + d * f) + (k) * ftcn_left_fssq_surface_pair_13 = (0) + (k) * ftcn_right_fssq_surface_pair_13
  2. L52
    specialize four_square_signed_cross_mixed_zero_reversed k
  3. L53
    specialize four_square_signed_cross_mixed_zero_reversed b
  4. L54
    specialize four_square_signed_cross_mixed_zero_reversed d
  5. L55
    specialize four_square_signed_cross_mixed_zero_reversed f
  6. L56
    specialize four_square_signed_cross_mixed_zero_reversed h
  7. L57
    apply four_square_signed_cross_mixed_zero_reversed
  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 : 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
  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 hdot2L69–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 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
  2. L70
    specialize four_square_signed_dot_positive k
  3. L71
    specialize four_square_signed_dot_positive c
  4. L72
    specialize four_square_signed_dot_positive g
  5. L73
    apply four_square_signed_dot_positive
  6. L74
    exact horient2
10Establish hdot3L75–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 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
  2. L76
    specialize four_square_signed_dot_positive k
  3. L77
    specialize four_square_signed_dot_positive d
  4. L78
    specialize four_square_signed_dot_positive h
  5. L79
    apply four_square_signed_dot_positive
  6. L80
    exact horient3
11Establish hpositive3L81–89

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

  1. L81
    have hpositive3 : exists ftcn_left_fssq_surface_hpositive3 ftcn_right_fssq_surface_hpositive3. ((c * g) + (d * h)) + (k) * ftcn_left_fssq_surface_hpositive3 = ((g * g) + (h * h)) + (k) * ftcn_right_fssq_surface_hpositive3
  2. L82
    specialize mod_eq_add k
  3. L83
    specialize mod_eq_add (c * g)
  4. L84
    specialize mod_eq_add (g * g)
  5. L85
    specialize mod_eq_add (d * h)
  6. L86
    specialize mod_eq_add (h * h)
  7. L87
    apply mod_eq_add
  8. L88
    exact hdot2
  9. L89
    exact hdot3
12Establish hdot0L90–95

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. L90
    have 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
  2. L91
    specialize four_square_signed_dot_negative_zero k
  3. L92
    specialize four_square_signed_dot_negative_zero a
  4. L93
    specialize four_square_signed_dot_negative_zero e
  5. L94
    apply four_square_signed_dot_negative_zero
  6. L95
    exact horient0
13Establish hdot1L96–101

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. L96
    have hdot1 : exists ftcn_left_fssq_surface_dot_1 ftcn_right_fssq_surface_dot_1. (b * f + f * f) + (k) * ftcn_left_fssq_surface_dot_1 = (0) + (k) * ftcn_right_fssq_surface_dot_1
  2. L97
    specialize four_square_signed_dot_negative_zero k
  3. L98
    specialize four_square_signed_dot_negative_zero b
  4. L99
    specialize four_square_signed_dot_negative_zero f
  5. L100
    apply four_square_signed_dot_negative_zero
  6. L101
    exact horient1
14Establish hnegative1L102–108

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. L102
    have hnegative1 : exists ftcn_left_fssq_surface_hnegative1 ftcn_right_fssq_surface_hnegative1. (((a * e) + (e * e)) + ((b * f) + (f * f))) + (k) * ftcn_left_fssq_surface_hnegative1 = (0) + (k) * ftcn_right_fssq_surface_hnegative1
  2. L103
    specialize four_square_signed_mod_zero_add k
  3. L104
    specialize four_square_signed_mod_zero_add ((a * e) + (e * e))
  4. L105
    specialize four_square_signed_mod_zero_add ((b * f) + (f * f))
  5. L106
    apply four_square_signed_mod_zero_add
  6. L107
    exact hdot0
  7. L108
    exact hdot1
15Establish hnegative_shuffleL109–118

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. L109
    have hnegative_shuffle : (((a * e) + (e * e)) + ((b * f) + (f * f))) = ((a * e + b * f) + (e * e + f * f))
  2. L110
    trans ((a * e) + ((e * e) + ((b * f) + (f * f))))
  3. L111
    simp [add_assoc]
  4. L112
    trans ((a * e) + ((b * f) + ((e * e) + (f * f))))
  5. L113
    congr
  6. L114
    refl
  7. L115
    trans ((b * f) + ((e * e) + (f * f)))
  8. L116
    apply four_square_add_swap_right_tail
  9. L117
    congr
  10. L118
    refl
16Calculate and transport equalitiesL119–122

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

  1. L119
    refl
  2. L120
    symm
  3. L121
    simp [add_assoc]
  4. L122
    rewrite hnegative_shuffle at hnegative1
17Establish hnorm_shuffleL123–132

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. L123
    have hnorm_shuffle : (((g * g) + (h * h)) + (e * e + f * f)) = (e * e + f * f + g * g + h * h)
  2. L124
    trans ((g * g) + ((h * h) + ((e * e) + (f * f))))
  3. L125
    simp [add_assoc]
  4. L126
    trans ((e * e) + ((f * f) + ((g * g) + (h * h))))
  5. L127
    trans ((e * e) + ((g * g) + ((h * h) + (f * f))))
  6. L128
    trans ((g * g) + ((e * e) + ((h * h) + (f * f))))
  7. L129
    congr
  8. L130
    refl
  9. L131
    apply four_square_add_swap_right_tail
  10. L132
    apply four_square_add_swap_right_tail
18Calculate and transport equalitiesL133–138

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

  1. L133
    congr
  2. L134
    refl
  3. L135
    trans ((f * f) + ((g * g) + (h * h)))
  4. L136
    trans ((g * g) + ((f * f) + (h * h)))
  5. L137
    congr
  6. L138
    refl
19Use earlier factsL139–140

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

  1. L139
    apply add_comm
  2. L140
    apply four_square_add_swap_right_tail
20Calculate and transport equalitiesL141–145

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

  1. L141
    congr
  2. L142
    refl
  3. L143
    refl
  4. L144
    symm
  5. L145
    simp [add_assoc]
21Establish hordered_normL146–148

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

  1. L146
    have hordered_norm : exists ftcn_left_fssq_surface_ordered_norm ftcn_right_fssq_surface_ordered_norm. (((g * g) + (h * h)) + (e * e + f * f)) + (k) * ftcn_left_fssq_surface_ordered_norm = (0) + (k) * ftcn_right_fssq_surface_ordered_norm
  2. L147
    rewrite hnorm_shuffle
  3. L148
    exact hnorm
22Establish hpartitionL149–158

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

  1. L149
    have hpartition : exists ftcn_left_fssq_surface_partition ftcn_right_fssq_surface_partition. ((c * g) + (d * h)) + (k) * ftcn_left_fssq_surface_partition = (a * e + b * f) + (k) * ftcn_right_fssq_surface_partition
  2. L150
    specialize four_square_signed_partition_balance k
  3. L151
    specialize four_square_signed_partition_balance ((c * g) + (d * h))
  4. L152
    specialize four_square_signed_partition_balance ((g * g) + (h * h))
  5. L153
    specialize four_square_signed_partition_balance (a * e + b * f)
  6. L154
    specialize four_square_signed_partition_balance (e * e + f * f)
  7. L155
    apply four_square_signed_partition_balance
  8. L156
    exact hpositive3
  9. L157
    exact hnegative1
  10. L158
    exact hordered_norm
23Establish hblock0_reorderedL159–165

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. L159
    have hblock0_reordered : exists ftcn_left_fssq_surface_hblock0_reordered ftcn_right_fssq_surface_hblock0_reordered. ((a * h + d * e) + (b * g + c * f)) + (k) * ftcn_left_fssq_surface_hblock0_reordered = (0) + (k) * ftcn_right_fssq_surface_hblock0_reordered
  2. L160
    specialize four_square_signed_mod_zero_add k
  3. L161
    specialize four_square_signed_mod_zero_add (a * h + d * e)
  4. L162
    specialize four_square_signed_mod_zero_add (b * g + c * f)
  5. L163
    apply four_square_signed_mod_zero_add
  6. L164
    exact hpair03
  7. L165
    exact hpair12
24Establish hblock0_shuffleL166–175

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. L166
    have hblock0_shuffle : (a * h + d * e) + (b * g + c * f) = a * h + b * g + c * f + d * e
  2. L167
    trans ((a * h) + ((d * e) + ((b * g) + (c * f))))
  3. L168
    simp [add_assoc]
  4. L169
    trans ((a * h) + ((b * g) + ((c * f) + (d * e))))
  5. L170
    congr
  6. L171
    refl
  7. L172
    trans ((b * g) + ((d * e) + (c * f)))
  8. L173
    apply four_square_add_swap_right_tail
  9. L174
    congr
  10. L175
    refl
25Calculate and transport equalitiesL176–176

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

  1. L176
    trans ((c * f) + (d * e))
26Use earlier factsL177–177

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

  1. L177
    apply add_comm
27Calculate and transport equalitiesL178–183

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

  1. L178
    congr
  2. L179
    refl
  3. L180
    refl
  4. L181
    symm
  5. L182
    simp [add_assoc]
  6. L183
    rewrite hblock0_shuffle at hblock0_reordered
28Establish hblock0L184–185

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

  1. L184
    have hblock0 : exists ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_0 ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_0. (a * h + b * g + c * f + d * e) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_0 = (0) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_0
  2. L185
    exact hblock0_reordered
29Establish hblock1L186–192

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

  1. L186
    have hblock1 : exists ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_1 ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_1. (a * g + c * e) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_1 = (b * h + d * f) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_1
  2. L187
    specialize four_square_signed_mod_zero_equivalent k
  3. L188
    specialize four_square_signed_mod_zero_equivalent (a * g + c * e)
  4. L189
    specialize four_square_signed_mod_zero_equivalent (b * h + d * f)
  5. L190
    apply four_square_signed_mod_zero_equivalent
  6. L191
    exact hpair02
  7. L192
    exact hpair13
30Establish hpair23_reverseL193–198

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

  1. L193
    have hpair23_reverse : exists ftcn_left_fssq_surface_hpair23_reverse ftcn_right_fssq_surface_hpair23_reverse. (d * g) + (k) * ftcn_left_fssq_surface_hpair23_reverse = (c * h) + (k) * ftcn_right_fssq_surface_hpair23_reverse
  2. L194
    specialize mod_eq_symm k
  3. L195
    specialize mod_eq_symm (c * h)
  4. L196
    specialize mod_eq_symm (d * g)
  5. L197
    apply mod_eq_symm
  6. L198
    exact hpair23
31Establish hblock2_reorderedL199–207

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

  1. L199
    have hblock2_reordered : exists ftcn_left_fssq_surface_hblock2_reordered ftcn_right_fssq_surface_hblock2_reordered. ((a * f) + (d * g)) + (k) * ftcn_left_fssq_surface_hblock2_reordered = ((b * e) + (c * h)) + (k) * ftcn_right_fssq_surface_hblock2_reordered
  2. L200
    specialize mod_eq_add k
  3. L201
    specialize mod_eq_add (a * f)
  4. L202
    specialize mod_eq_add (b * e)
  5. L203
    specialize mod_eq_add (d * g)
  6. L204
    specialize mod_eq_add (c * h)
  7. L205
    apply mod_eq_add
  8. L206
    exact hpair01
  9. L207
    exact hpair23_reverse
32Establish hblock2_swapL208–210

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

  1. L208
    have hblock2_swap : b * e + c * h = c * h + b * e
  2. L209
    apply add_comm
  3. L210
    rewrite hblock2_swap at hblock2_reordered
33Establish hblock2L211–212

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

  1. L211
    have hblock2 : exists ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_2 ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_2. (a * f + d * g) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_2 = (c * h + b * e) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_2
  2. L212
    exact hblock2_reordered
34Establish hblock3_reorderedL213–218

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

  1. L213
    have hblock3_reordered : exists ftcn_left_fssq_surface_hblock3_reordered ftcn_right_fssq_surface_hblock3_reordered. (a * e + b * f) + (k) * ftcn_left_fssq_surface_hblock3_reordered = ((c * g) + (d * h)) + (k) * ftcn_right_fssq_surface_hblock3_reordered
  2. L214
    specialize mod_eq_symm k
  3. L215
    specialize mod_eq_symm ((c * g) + (d * h))
  4. L216
    specialize mod_eq_symm (a * e + b * f)
  5. L217
    apply mod_eq_symm
  6. L218
    exact hpartition
35Establish hblock3_swapL219–221

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

  1. L219
    have hblock3_swap : c * g + d * h = d * h + c * g
  2. L220
    apply add_comm
  3. L221
    rewrite hblock3_swap at hblock3_reordered
36Establish hblock3L222–223

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

  1. L222
    have hblock3 : exists ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_3 ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_3. (a * e + b * f) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_3 = (d * h + c * g) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_3
  2. L223
    exact hblock3_reordered
37Separate the logical casesL224–224

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

  1. L224
    split
38Use earlier factsL225–225

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

  1. L225
    exact hblock0
39Separate the logical casesL226–226

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

  1. L226
    split
40Use earlier factsL227–227

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

  1. L227
    exact hblock1
41Separate the logical casesL228–228

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

  1. L228
    split
42Use earlier factsL229–230

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

  1. L229
    exact hblock2
  2. L230
    exact hblock3

Library-wide reading audit

Original exact command ledger · 230 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 : exists ftcn_left_fssq_surface_pair_01 ftcn_right_fssq_surface_pair_01. (a * f) + (k) * ftcn_left_fssq_surface_pair_01 = (b * e) + (k) * ftcn_right_fssq_surface_pair_01
  16. 0016specialize four_square_signed_cross_negative k
  17. 0017specialize four_square_signed_cross_negative a
  18. 0018specialize four_square_signed_cross_negative b
  19. 0019specialize four_square_signed_cross_negative e
  20. 0020specialize four_square_signed_cross_negative f
  21. 0021apply four_square_signed_cross_negative
  22. 0022exact horient0
  23. 0023exact horient1
  24. 0024have 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 : 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 : exists ftcn_left_fssq_surface_pair_12 ftcn_right_fssq_surface_pair_12. (b * g + c * f) + (k) * ftcn_left_fssq_surface_pair_12 = (0) + (k) * ftcn_right_fssq_surface_pair_12
  43. 0043specialize four_square_signed_cross_mixed_zero_reversed k
  44. 0044specialize four_square_signed_cross_mixed_zero_reversed b
  45. 0045specialize four_square_signed_cross_mixed_zero_reversed c
  46. 0046specialize four_square_signed_cross_mixed_zero_reversed f
  47. 0047specialize four_square_signed_cross_mixed_zero_reversed g
  48. 0048apply four_square_signed_cross_mixed_zero_reversed
  49. 0049exact horient1
  50. 0050exact horient2
  51. 0051have hpair13 : exists ftcn_left_fssq_surface_pair_13 ftcn_right_fssq_surface_pair_13. (b * h + d * f) + (k) * ftcn_left_fssq_surface_pair_13 = (0) + (k) * ftcn_right_fssq_surface_pair_13
  52. 0052specialize four_square_signed_cross_mixed_zero_reversed k
  53. 0053specialize four_square_signed_cross_mixed_zero_reversed b
  54. 0054specialize four_square_signed_cross_mixed_zero_reversed d
  55. 0055specialize four_square_signed_cross_mixed_zero_reversed f
  56. 0056specialize four_square_signed_cross_mixed_zero_reversed h
  57. 0057apply four_square_signed_cross_mixed_zero_reversed
  58. 0058exact horient1
  59. 0059exact horient3
  60. 0060have 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 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
  70. 0070specialize four_square_signed_dot_positive k
  71. 0071specialize four_square_signed_dot_positive c
  72. 0072specialize four_square_signed_dot_positive g
  73. 0073apply four_square_signed_dot_positive
  74. 0074exact horient2
  75. 0075have 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
  76. 0076specialize four_square_signed_dot_positive k
  77. 0077specialize four_square_signed_dot_positive d
  78. 0078specialize four_square_signed_dot_positive h
  79. 0079apply four_square_signed_dot_positive
  80. 0080exact horient3
  81. 0081have hpositive3 : exists ftcn_left_fssq_surface_hpositive3 ftcn_right_fssq_surface_hpositive3. ((c * g) + (d * h)) + (k) * ftcn_left_fssq_surface_hpositive3 = ((g * g) + (h * h)) + (k) * ftcn_right_fssq_surface_hpositive3
  82. 0082specialize mod_eq_add k
  83. 0083specialize mod_eq_add (c * g)
  84. 0084specialize mod_eq_add (g * g)
  85. 0085specialize mod_eq_add (d * h)
  86. 0086specialize mod_eq_add (h * h)
  87. 0087apply mod_eq_add
  88. 0088exact hdot2
  89. 0089exact hdot3
  90. 0090have 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
  91. 0091specialize four_square_signed_dot_negative_zero k
  92. 0092specialize four_square_signed_dot_negative_zero a
  93. 0093specialize four_square_signed_dot_negative_zero e
  94. 0094apply four_square_signed_dot_negative_zero
  95. 0095exact horient0
  96. 0096have hdot1 : exists ftcn_left_fssq_surface_dot_1 ftcn_right_fssq_surface_dot_1. (b * f + f * f) + (k) * ftcn_left_fssq_surface_dot_1 = (0) + (k) * ftcn_right_fssq_surface_dot_1
  97. 0097specialize four_square_signed_dot_negative_zero k
  98. 0098specialize four_square_signed_dot_negative_zero b
  99. 0099specialize four_square_signed_dot_negative_zero f
  100. 0100apply four_square_signed_dot_negative_zero
  101. 0101exact horient1
  102. 0102have hnegative1 : exists ftcn_left_fssq_surface_hnegative1 ftcn_right_fssq_surface_hnegative1. (((a * e) + (e * e)) + ((b * f) + (f * f))) + (k) * ftcn_left_fssq_surface_hnegative1 = (0) + (k) * ftcn_right_fssq_surface_hnegative1
  103. 0103specialize four_square_signed_mod_zero_add k
  104. 0104specialize four_square_signed_mod_zero_add ((a * e) + (e * e))
  105. 0105specialize four_square_signed_mod_zero_add ((b * f) + (f * f))
  106. 0106apply four_square_signed_mod_zero_add
  107. 0107exact hdot0
  108. 0108exact hdot1
  109. 0109have hnegative_shuffle : (((a * e) + (e * e)) + ((b * f) + (f * f))) = ((a * e + b * f) + (e * e + f * f))
  110. 0110trans ((a * e) + ((e * e) + ((b * f) + (f * f))))
  111. 0111simp [add_assoc]
  112. 0112trans ((a * e) + ((b * f) + ((e * e) + (f * f))))
  113. 0113congr
  114. 0114refl
  115. 0115trans ((b * f) + ((e * e) + (f * f)))
  116. 0116apply four_square_add_swap_right_tail
  117. 0117congr
  118. 0118refl
  119. 0119refl
  120. 0120symm
  121. 0121simp [add_assoc]
  122. 0122rewrite hnegative_shuffle at hnegative1
  123. 0123have hnorm_shuffle : (((g * g) + (h * h)) + (e * e + f * f)) = (e * e + f * f + g * g + h * h)
  124. 0124trans ((g * g) + ((h * h) + ((e * e) + (f * f))))
  125. 0125simp [add_assoc]
  126. 0126trans ((e * e) + ((f * f) + ((g * g) + (h * h))))
  127. 0127trans ((e * e) + ((g * g) + ((h * h) + (f * f))))
  128. 0128trans ((g * g) + ((e * e) + ((h * h) + (f * f))))
  129. 0129congr
  130. 0130refl
  131. 0131apply four_square_add_swap_right_tail
  132. 0132apply four_square_add_swap_right_tail
  133. 0133congr
  134. 0134refl
  135. 0135trans ((f * f) + ((g * g) + (h * h)))
  136. 0136trans ((g * g) + ((f * f) + (h * h)))
  137. 0137congr
  138. 0138refl
  139. 0139apply add_comm
  140. 0140apply four_square_add_swap_right_tail
  141. 0141congr
  142. 0142refl
  143. 0143refl
  144. 0144symm
  145. 0145simp [add_assoc]
  146. 0146have hordered_norm : exists ftcn_left_fssq_surface_ordered_norm ftcn_right_fssq_surface_ordered_norm. (((g * g) + (h * h)) + (e * e + f * f)) + (k) * ftcn_left_fssq_surface_ordered_norm = (0) + (k) * ftcn_right_fssq_surface_ordered_norm
  147. 0147rewrite hnorm_shuffle
  148. 0148exact hnorm
  149. 0149have hpartition : exists ftcn_left_fssq_surface_partition ftcn_right_fssq_surface_partition. ((c * g) + (d * h)) + (k) * ftcn_left_fssq_surface_partition = (a * e + b * f) + (k) * ftcn_right_fssq_surface_partition
  150. 0150specialize four_square_signed_partition_balance k
  151. 0151specialize four_square_signed_partition_balance ((c * g) + (d * h))
  152. 0152specialize four_square_signed_partition_balance ((g * g) + (h * h))
  153. 0153specialize four_square_signed_partition_balance (a * e + b * f)
  154. 0154specialize four_square_signed_partition_balance (e * e + f * f)
  155. 0155apply four_square_signed_partition_balance
  156. 0156exact hpositive3
  157. 0157exact hnegative1
  158. 0158exact hordered_norm
  159. 0159have hblock0_reordered : exists ftcn_left_fssq_surface_hblock0_reordered ftcn_right_fssq_surface_hblock0_reordered. ((a * h + d * e) + (b * g + c * f)) + (k) * ftcn_left_fssq_surface_hblock0_reordered = (0) + (k) * ftcn_right_fssq_surface_hblock0_reordered
  160. 0160specialize four_square_signed_mod_zero_add k
  161. 0161specialize four_square_signed_mod_zero_add (a * h + d * e)
  162. 0162specialize four_square_signed_mod_zero_add (b * g + c * f)
  163. 0163apply four_square_signed_mod_zero_add
  164. 0164exact hpair03
  165. 0165exact hpair12
  166. 0166have hblock0_shuffle : (a * h + d * e) + (b * g + c * f) = a * h + b * g + c * f + d * e
  167. 0167trans ((a * h) + ((d * e) + ((b * g) + (c * f))))
  168. 0168simp [add_assoc]
  169. 0169trans ((a * h) + ((b * g) + ((c * f) + (d * e))))
  170. 0170congr
  171. 0171refl
  172. 0172trans ((b * g) + ((d * e) + (c * f)))
  173. 0173apply four_square_add_swap_right_tail
  174. 0174congr
  175. 0175refl
  176. 0176trans ((c * f) + (d * e))
  177. 0177apply add_comm
  178. 0178congr
  179. 0179refl
  180. 0180refl
  181. 0181symm
  182. 0182simp [add_assoc]
  183. 0183rewrite hblock0_shuffle at hblock0_reordered
  184. 0184have hblock0 : exists ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_0 ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_0. (a * h + b * g + c * f + d * e) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_0 = (0) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_0
  185. 0185exact hblock0_reordered
  186. 0186have hblock1 : exists ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_1 ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_1. (a * g + c * e) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_1 = (b * h + d * f) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_1
  187. 0187specialize four_square_signed_mod_zero_equivalent k
  188. 0188specialize four_square_signed_mod_zero_equivalent (a * g + c * e)
  189. 0189specialize four_square_signed_mod_zero_equivalent (b * h + d * f)
  190. 0190apply four_square_signed_mod_zero_equivalent
  191. 0191exact hpair02
  192. 0192exact hpair13
  193. 0193have hpair23_reverse : exists ftcn_left_fssq_surface_hpair23_reverse ftcn_right_fssq_surface_hpair23_reverse. (d * g) + (k) * ftcn_left_fssq_surface_hpair23_reverse = (c * h) + (k) * ftcn_right_fssq_surface_hpair23_reverse
  194. 0194specialize mod_eq_symm k
  195. 0195specialize mod_eq_symm (c * h)
  196. 0196specialize mod_eq_symm (d * g)
  197. 0197apply mod_eq_symm
  198. 0198exact hpair23
  199. 0199have hblock2_reordered : exists ftcn_left_fssq_surface_hblock2_reordered ftcn_right_fssq_surface_hblock2_reordered. ((a * f) + (d * g)) + (k) * ftcn_left_fssq_surface_hblock2_reordered = ((b * e) + (c * h)) + (k) * ftcn_right_fssq_surface_hblock2_reordered
  200. 0200specialize mod_eq_add k
  201. 0201specialize mod_eq_add (a * f)
  202. 0202specialize mod_eq_add (b * e)
  203. 0203specialize mod_eq_add (d * g)
  204. 0204specialize mod_eq_add (c * h)
  205. 0205apply mod_eq_add
  206. 0206exact hpair01
  207. 0207exact hpair23_reverse
  208. 0208have hblock2_swap : b * e + c * h = c * h + b * e
  209. 0209apply add_comm
  210. 0210rewrite hblock2_swap at hblock2_reordered
  211. 0211have hblock2 : exists ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_2 ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_2. (a * f + d * g) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_2 = (c * h + b * e) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_2
  212. 0212exact hblock2_reordered
  213. 0213have hblock3_reordered : exists ftcn_left_fssq_surface_hblock3_reordered ftcn_right_fssq_surface_hblock3_reordered. (a * e + b * f) + (k) * ftcn_left_fssq_surface_hblock3_reordered = ((c * g) + (d * h)) + (k) * ftcn_right_fssq_surface_hblock3_reordered
  214. 0214specialize mod_eq_symm k
  215. 0215specialize mod_eq_symm ((c * g) + (d * h))
  216. 0216specialize mod_eq_symm (a * e + b * f)
  217. 0217apply mod_eq_symm
  218. 0218exact hpartition
  219. 0219have hblock3_swap : c * g + d * h = d * h + c * g
  220. 0220apply add_comm
  221. 0221rewrite hblock3_swap at hblock3_reordered
  222. 0222have hblock3 : exists ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_3 ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_3. (a * e + b * f) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_3 = (d * h + c * g) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_mixed_blocks_block_3
  223. 0223exact hblock3_reordered
  224. 0224split
  225. 0225exact hblock0
  226. 0226split
  227. 0227exact hblock1
  228. 0228split
  229. 0229exact hblock2
  230. 0230exact hblock3