FS005Y · theorem body

four_square_signed_conjugate_positive_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) → ModEq(k,b,f) → ModEq(k,c,g) → ModEq(k,d,h) → ModEq(k,a · e + b · f + c · g + d · h,0) ∧ (ModEq(k,a · f + c · h,b · e + d · g) ∧ (ModEq(k,a · g + d · f,c · e + 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_conjugate_positive_blocks_norm ftcn_right_fssq_surface_four_square_signed_conjugate_positive_blocks_norm. (e * e + f * f + g * g + h * h) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_positive_blocks_norm = (0) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_positive_blocks_norm) -> (exists ftcn_left_fssq_surface_four_square_signed_conjugate_positive_blocks_0 ftcn_right_fssq_surface_four_square_signed_conjugate_positive_blocks_0. (a) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_positive_blocks_0 = (e) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_positive_blocks_0) -> (exists ftcn_left_fssq_surface_four_square_signed_conjugate_positive_blocks_1 ftcn_right_fssq_surface_four_square_signed_conjugate_positive_blocks_1. (b) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_positive_blocks_1 = (f) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_positive_blocks_1) -> (exists ftcn_left_fssq_surface_four_square_signed_conjugate_positive_blocks_2 ftcn_right_fssq_surface_four_square_signed_conjugate_positive_blocks_2. (c) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_positive_blocks_2 = (g) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_positive_blocks_2) -> (exists ftcn_left_fssq_surface_four_square_signed_conjugate_positive_blocks_3 ftcn_right_fssq_surface_four_square_signed_conjugate_positive_blocks_3. (d) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_positive_blocks_3 = (h) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_positive_blocks_3) -> ((exists ftcn_left_fssq_surface_four_square_signed_conjugate_positive_blocks_block_0 ftcn_right_fssq_surface_four_square_signed_conjugate_positive_blocks_block_0. (a * e + b * f + c * g + d * h) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_positive_blocks_block_0 = (0) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_positive_blocks_block_0) /\ ((exists ftcn_left_fssq_surface_four_square_signed_conjugate_positive_blocks_block_1 ftcn_right_fssq_surface_four_square_signed_conjugate_positive_blocks_block_1. (a * f + c * h) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_positive_blocks_block_1 = (b * e + d * g) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_positive_blocks_block_1) /\ ((exists ftcn_left_fssq_surface_four_square_signed_conjugate_positive_blocks_block_2 ftcn_right_fssq_surface_four_square_signed_conjugate_positive_blocks_block_2. (a * g + d * f) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_positive_blocks_block_2 = (c * e + b * h) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_positive_blocks_block_2) /\ (exists ftcn_left_fssq_surface_four_square_signed_conjugate_positive_blocks_block_3 ftcn_right_fssq_surface_four_square_signed_conjugate_positive_blocks_block_3. (a * h + b * g) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_positive_blocks_block_3 = (d * e + c * f) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_positive_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

FS004Q four_square_signed_orientation_mask_00

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 · 18 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
four square signed cross positivefour square signed dot positive
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 positive.

  1. L15
    have hpair01 : ModEq(k,a · f,b · e)Definitions: ModEq(k,a · f,b · e)Original native command in the exact edition
  2. L16
    specialize four_square_signed_cross_positive k
  3. L17
    specialize four_square_signed_cross_positive a
  4. L18
    specialize four_square_signed_cross_positive b
  5. L19
    specialize four_square_signed_cross_positive e
  6. L20
    specialize four_square_signed_cross_positive f
  7. L21
    apply four_square_signed_cross_positive
  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 positive.

  1. L24
    have hpair02 : ModEq(k,a · g,c · e)Definitions: ModEq(k,a · g,c · e)Original native command in the exact edition
  2. L25
    specialize four_square_signed_cross_positive k
  3. L26
    specialize four_square_signed_cross_positive a
  4. L27
    specialize four_square_signed_cross_positive c
  5. L28
    specialize four_square_signed_cross_positive e
  6. L29
    specialize four_square_signed_cross_positive g
  7. L30
    apply four_square_signed_cross_positive
  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 positive.

  1. L33
    have hpair03 : ModEq(k,a · h,d · e)Definitions: ModEq(k,a · h,d · e)Original native command in the exact edition
  2. L34
    specialize four_square_signed_cross_positive k
  3. L35
    specialize four_square_signed_cross_positive a
  4. L36
    specialize four_square_signed_cross_positive d
  5. L37
    specialize four_square_signed_cross_positive e
  6. L38
    specialize four_square_signed_cross_positive h
  7. L39
    apply four_square_signed_cross_positive
  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 hdot0L69–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 hdot0 : ModEq(k,a · e,e · e)Definitions: ModEq(k,a · e,e · e)Original native command in the exact edition
  2. L70
    specialize four_square_signed_dot_positive k
  3. L71
    specialize four_square_signed_dot_positive a
  4. L72
    specialize four_square_signed_dot_positive e
  5. L73
    apply four_square_signed_dot_positive
  6. L74
    exact horient0
10Establish hdot1L75–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 hdot1 : ModEq(k,b · f,f · f)Definitions: ModEq(k,b · f,f · f)Original native command in the exact edition
  2. L76
    specialize four_square_signed_dot_positive k
  3. L77
    specialize four_square_signed_dot_positive b
  4. L78
    specialize four_square_signed_dot_positive f
  5. L79
    apply four_square_signed_dot_positive
  6. L80
    exact horient1
11Establish hdot2L81–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 hdot2 : ModEq(k,c · g,g · g)Definitions: ModEq(k,c · g,g · g)Original native command in the exact edition
  2. L82
    specialize four_square_signed_dot_positive k
  3. L83
    specialize four_square_signed_dot_positive c
  4. L84
    specialize four_square_signed_dot_positive g
  5. L85
    apply four_square_signed_dot_positive
  6. L86
    exact horient2
12Establish hdot3L87–92

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

  1. L87
    have hdot3 : ModEq(k,d · h,h · h)Definitions: ModEq(k,d · h,h · h)Original native command in the exact edition
  2. L88
    specialize four_square_signed_dot_positive k
  3. L89
    specialize four_square_signed_dot_positive d
  4. L90
    specialize four_square_signed_dot_positive h
  5. L91
    apply four_square_signed_dot_positive
  6. L92
    exact horient3
13Establish hpositive1L93–101

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

  1. L93
    have hpositive1 : ModEq(k,a · e + b · f,e · e + f · f)Definitions: ModEq(k,a · e + b · f,e · e + f · f)Original native command in the exact edition
  2. L94
    specialize mod_eq_add k
  3. L95
    specialize mod_eq_add (a * e)
  4. L96
    specialize mod_eq_add (e * e)
  5. L97
    specialize mod_eq_add (b * f)
  6. L98
    specialize mod_eq_add (f * f)
  7. L99
    apply mod_eq_add
  8. L100
    exact hdot0
  9. L101
    exact hdot1
14Establish hpositive2L102–110

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

  1. L102
    have hpositive2 : ModEq(k,a · e + b · f + c · g,e · e + f · f + g · g)Definitions: ModEq(k,a · e + b · f + c · g,e · e + f · f + g · g)Original native command in the exact edition
  2. L103
    specialize mod_eq_add k
  3. L104
    specialize mod_eq_add ((a * e) + (b * f))
  4. L105
    specialize mod_eq_add ((e * e) + (f * f))
  5. L106
    specialize mod_eq_add (c * g)
  6. L107
    specialize mod_eq_add (g * g)
  7. L108
    apply mod_eq_add
  8. L109
    exact hpositive1
  9. L110
    exact hdot2
15Establish hpositive3L111–119

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

  1. L111
    have hpositive3 : ModEq(k,a · e + b · f + c · g + d · h,e · e + f · f + g · g + h · h)Definitions: ModEq(k,a · e + b · f + c · g + d · h,e · e + f · f + g · g + h · h)Original native command in the exact edition
  2. L112
    specialize mod_eq_add k
  3. L113
    specialize mod_eq_add (((a * e) + (b * f)) + (c * g))
  4. L114
    specialize mod_eq_add (((e * e) + (f * f)) + (g * g))
  5. L115
    specialize mod_eq_add (d * h)
  6. L116
    specialize mod_eq_add (h * h)
  7. L117
    apply mod_eq_add
  8. L118
    exact hpositive2
  9. L119
    exact hdot3
16Establish hblock0L120–127

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

  1. L120
    have hblock0 : ModEq(k,a · e + b · f + c · g + d · h,0)Definitions: ModEq(k,a · e + b · f + c · g + d · h,0)Original native command in the exact edition
  2. L121
    specialize mod_eq_trans k
  3. L122
    specialize mod_eq_trans (a * e + b * f + c * g + d * h)
  4. L123
    specialize mod_eq_trans (e * e + f * f + g * g + h * h)
  5. L124
    specialize mod_eq_trans 0
  6. L125
    apply mod_eq_trans
  7. L126
    exact hpositive3
  8. L127
    exact hnorm
17Establish hblock1L128–136

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

  1. L128
    have hblock1 : ModEq(k,a · f + c · h,b · e + d · g)Definitions: ModEq(k,a · f + c · h,b · e + d · g)Original native command in the exact edition
  2. L129
    specialize mod_eq_add k
  3. L130
    specialize mod_eq_add (a * f)
  4. L131
    specialize mod_eq_add (b * e)
  5. L132
    specialize mod_eq_add (c * h)
  6. L133
    specialize mod_eq_add (d * g)
  7. L134
    apply mod_eq_add
  8. L135
    exact hpair01
  9. L136
    exact hpair23
18Establish hpair13_reverseL137–142

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

  1. L137
    have hpair13_reverse : ModEq(k,d · f,b · h)Definitions: ModEq(k,d · f,b · h)Original native command in the exact edition
  2. L138
    specialize mod_eq_symm k
  3. L139
    specialize mod_eq_symm (b * h)
  4. L140
    specialize mod_eq_symm (d * f)
  5. L141
    apply mod_eq_symm
  6. L142
    exact hpair13
19Establish hblock2L143–151

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

  1. L143
    have hblock2 : ModEq(k,a · g + d · f,c · e + b · h)Definitions: ModEq(k,a · g + d · f,c · e + b · h)Original native command in the exact edition
  2. L144
    specialize mod_eq_add k
  3. L145
    specialize mod_eq_add (a * g)
  4. L146
    specialize mod_eq_add (c * e)
  5. L147
    specialize mod_eq_add (d * f)
  6. L148
    specialize mod_eq_add (b * h)
  7. L149
    apply mod_eq_add
  8. L150
    exact hpair02
  9. L151
    exact hpair13_reverse
20Establish hblock3L152–160

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

  1. L152
    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. L153
    specialize mod_eq_add k
  3. L154
    specialize mod_eq_add (a * h)
  4. L155
    specialize mod_eq_add (d * e)
  5. L156
    specialize mod_eq_add (b * g)
  6. L157
    specialize mod_eq_add (c * f)
  7. L158
    apply mod_eq_add
  8. L159
    exact hpair03
  9. L160
    exact hpair12
21Separate the logical casesL161–161

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

  1. L161
    split
22Use earlier factsL162–162

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

  1. L162
    exact hblock0
23Separate the logical casesL163–163

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

  1. L163
    split
24Use earlier factsL164–164

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

  1. L164
    exact hblock1
25Separate the logical casesL165–165

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

  1. L165
    split
26Use earlier factsL166–167

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

  1. L166
    exact hblock2
  2. L167
    exact hblock3

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 horient0
  12. 0012intro horient1
  13. 0013intro horient2
  14. 0014intro horient3
  15. 0015have hpair01 : ModEq(k,a · f,b · e)
    Exact native replay linehave 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_positive k
  17. 0017specialize four_square_signed_cross_positive a
  18. 0018specialize four_square_signed_cross_positive b
  19. 0019specialize four_square_signed_cross_positive e
  20. 0020specialize four_square_signed_cross_positive f
  21. 0021apply four_square_signed_cross_positive
  22. 0022exact horient0
  23. 0023exact horient1
  24. 0024have hpair02 : ModEq(k,a · g,c · e)
    Exact native replay linehave hpair02 : exists ftcn_left_fssq_surface_pair_02 ftcn_right_fssq_surface_pair_02. (a * g) + (k) * ftcn_left_fssq_surface_pair_02 = (c * e) + (k) * ftcn_right_fssq_surface_pair_02
  25. 0025specialize four_square_signed_cross_positive k
  26. 0026specialize four_square_signed_cross_positive a
  27. 0027specialize four_square_signed_cross_positive c
  28. 0028specialize four_square_signed_cross_positive e
  29. 0029specialize four_square_signed_cross_positive g
  30. 0030apply four_square_signed_cross_positive
  31. 0031exact horient0
  32. 0032exact horient2
  33. 0033have hpair03 : ModEq(k,a · h,d · e)
    Exact native replay linehave hpair03 : exists ftcn_left_fssq_surface_pair_03 ftcn_right_fssq_surface_pair_03. (a * h) + (k) * ftcn_left_fssq_surface_pair_03 = (d * e) + (k) * ftcn_right_fssq_surface_pair_03
  34. 0034specialize four_square_signed_cross_positive k
  35. 0035specialize four_square_signed_cross_positive a
  36. 0036specialize four_square_signed_cross_positive d
  37. 0037specialize four_square_signed_cross_positive e
  38. 0038specialize four_square_signed_cross_positive h
  39. 0039apply four_square_signed_cross_positive
  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 hdot0 : ModEq(k,a · e,e · e)
    Exact native replay linehave hdot0 : exists ftcn_left_fssq_surface_dot_0 ftcn_right_fssq_surface_dot_0. (a * e) + (k) * ftcn_left_fssq_surface_dot_0 = (e * e) + (k) * ftcn_right_fssq_surface_dot_0
  70. 0070specialize four_square_signed_dot_positive k
  71. 0071specialize four_square_signed_dot_positive a
  72. 0072specialize four_square_signed_dot_positive e
  73. 0073apply four_square_signed_dot_positive
  74. 0074exact horient0
  75. 0075have 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
  76. 0076specialize four_square_signed_dot_positive k
  77. 0077specialize four_square_signed_dot_positive b
  78. 0078specialize four_square_signed_dot_positive f
  79. 0079apply four_square_signed_dot_positive
  80. 0080exact horient1
  81. 0081have 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
  82. 0082specialize four_square_signed_dot_positive k
  83. 0083specialize four_square_signed_dot_positive c
  84. 0084specialize four_square_signed_dot_positive g
  85. 0085apply four_square_signed_dot_positive
  86. 0086exact horient2
  87. 0087have 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
  88. 0088specialize four_square_signed_dot_positive k
  89. 0089specialize four_square_signed_dot_positive d
  90. 0090specialize four_square_signed_dot_positive h
  91. 0091apply four_square_signed_dot_positive
  92. 0092exact horient3
  93. 0093have hpositive1 : ModEq(k,a · e + b · f,e · e + f · f)
    Exact native replay linehave hpositive1 : exists ftcn_left_fssq_surface_hpositive1 ftcn_right_fssq_surface_hpositive1. ((a * e) + (b * f)) + (k) * ftcn_left_fssq_surface_hpositive1 = ((e * e) + (f * f)) + (k) * ftcn_right_fssq_surface_hpositive1
  94. 0094specialize mod_eq_add k
  95. 0095specialize mod_eq_add (a * e)
  96. 0096specialize mod_eq_add (e * e)
  97. 0097specialize mod_eq_add (b * f)
  98. 0098specialize mod_eq_add (f * f)
  99. 0099apply mod_eq_add
  100. 0100exact hdot0
  101. 0101exact hdot1
  102. 0102have hpositive2 : ModEq(k,a · e + b · f + c · g,e · e + f · f + g · g)
    Exact native replay linehave hpositive2 : exists ftcn_left_fssq_surface_hpositive2 ftcn_right_fssq_surface_hpositive2. (((a * e) + (b * f)) + (c * g)) + (k) * ftcn_left_fssq_surface_hpositive2 = (((e * e) + (f * f)) + (g * g)) + (k) * ftcn_right_fssq_surface_hpositive2
  103. 0103specialize mod_eq_add k
  104. 0104specialize mod_eq_add ((a * e) + (b * f))
  105. 0105specialize mod_eq_add ((e * e) + (f * f))
  106. 0106specialize mod_eq_add (c * g)
  107. 0107specialize mod_eq_add (g * g)
  108. 0108apply mod_eq_add
  109. 0109exact hpositive1
  110. 0110exact hdot2
  111. 0111have hpositive3 : ModEq(k,a · e + b · f + c · g + d · h,e · e + f · f + g · g + h · h)
    Exact native replay linehave hpositive3 : exists ftcn_left_fssq_surface_hpositive3 ftcn_right_fssq_surface_hpositive3. ((((a * e) + (b * f)) + (c * g)) + (d * h)) + (k) * ftcn_left_fssq_surface_hpositive3 = ((((e * e) + (f * f)) + (g * g)) + (h * h)) + (k) * ftcn_right_fssq_surface_hpositive3
  112. 0112specialize mod_eq_add k
  113. 0113specialize mod_eq_add (((a * e) + (b * f)) + (c * g))
  114. 0114specialize mod_eq_add (((e * e) + (f * f)) + (g * g))
  115. 0115specialize mod_eq_add (d * h)
  116. 0116specialize mod_eq_add (h * h)
  117. 0117apply mod_eq_add
  118. 0118exact hpositive2
  119. 0119exact hdot3
  120. 0120have hblock0 : ModEq(k,a · e + b · f + c · g + d · h,0)
    Exact native replay linehave hblock0 : exists ftcn_left_fssq_surface_four_square_signed_conjugate_positive_blocks_block_0 ftcn_right_fssq_surface_four_square_signed_conjugate_positive_blocks_block_0. (a * e + b * f + c * g + d * h) + (k) * ftcn_left_fssq_surface_four_square_signed_conjugate_positive_blocks_block_0 = (0) + (k) * ftcn_right_fssq_surface_four_square_signed_conjugate_positive_blocks_block_0
  121. 0121specialize mod_eq_trans k
  122. 0122specialize mod_eq_trans (a * e + b * f + c * g + d * h)
  123. 0123specialize mod_eq_trans (e * e + f * f + g * g + h * h)
  124. 0124specialize mod_eq_trans 0
  125. 0125apply mod_eq_trans
  126. 0126exact hpositive3
  127. 0127exact hnorm
  128. 0128have hblock1 : ModEq(k,a · f + c · h,b · e + d · g)
    Exact native replay linehave hblock1 : exists ftcn_left_fssq_surface_hblock1 ftcn_right_fssq_surface_hblock1. ((a * f) + (c * h)) + (k) * ftcn_left_fssq_surface_hblock1 = ((b * e) + (d * g)) + (k) * ftcn_right_fssq_surface_hblock1
  129. 0129specialize mod_eq_add k
  130. 0130specialize mod_eq_add (a * f)
  131. 0131specialize mod_eq_add (b * e)
  132. 0132specialize mod_eq_add (c * h)
  133. 0133specialize mod_eq_add (d * g)
  134. 0134apply mod_eq_add
  135. 0135exact hpair01
  136. 0136exact hpair23
  137. 0137have 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
  138. 0138specialize mod_eq_symm k
  139. 0139specialize mod_eq_symm (b * h)
  140. 0140specialize mod_eq_symm (d * f)
  141. 0141apply mod_eq_symm
  142. 0142exact hpair13
  143. 0143have hblock2 : ModEq(k,a · g + d · f,c · e + b · h)
    Exact native replay linehave hblock2 : exists ftcn_left_fssq_surface_hblock2 ftcn_right_fssq_surface_hblock2. ((a * g) + (d * f)) + (k) * ftcn_left_fssq_surface_hblock2 = ((c * e) + (b * h)) + (k) * ftcn_right_fssq_surface_hblock2
  144. 0144specialize mod_eq_add k
  145. 0145specialize mod_eq_add (a * g)
  146. 0146specialize mod_eq_add (c * e)
  147. 0147specialize mod_eq_add (d * f)
  148. 0148specialize mod_eq_add (b * h)
  149. 0149apply mod_eq_add
  150. 0150exact hpair02
  151. 0151exact hpair13_reverse
  152. 0152have hblock3 : ModEq(k,a · h + b · g,d · e + c · f)
    Exact native replay linehave hblock3 : exists ftcn_left_fssq_surface_hblock3 ftcn_right_fssq_surface_hblock3. ((a * h) + (b * g)) + (k) * ftcn_left_fssq_surface_hblock3 = ((d * e) + (c * f)) + (k) * ftcn_right_fssq_surface_hblock3
  153. 0153specialize mod_eq_add k
  154. 0154specialize mod_eq_add (a * h)
  155. 0155specialize mod_eq_add (d * e)
  156. 0156specialize mod_eq_add (b * g)
  157. 0157specialize mod_eq_add (c * f)
  158. 0158apply mod_eq_add
  159. 0159exact hpair03
  160. 0160exact hpair12
  161. 0161split
  162. 0162exact hblock0
  163. 0163split
  164. 0164exact hblock1
  165. 0165split
  166. 0166exact hblock2
  167. 0167exact hblock3