FS0050 · theorem body

four_square_signed_orientation_mask_10

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

Constructive signed quaternion quotient for centered orientation mask 1010, using the exact four_square_signed_conjugate_mixed_blocks surface.

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

∀ p. ∀ k. ∀ h. ∀ a. ∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ j. ∀ r. ¬k = 0 → k = 2 · h + 1 → p · k = a · a + b · b + c · c + d · d → ModEq(k,a,e) → ModEq(k,b + f,0) → ModEq(k,c,g) → ModEq(k,d + j,0) → k · r = e · e + f · f + g · g + j · j → ∃ x. ∃ y. ∃ z. ∃ n. p · r = x · x + y · y + z · z + n · n

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 p k h a b c d e f g j r. ~(k = 0) -> k = 2 * h + 1 -> p * k = a * a + b * b + c * c + d * d -> (exists ftcn_left_mask_10_0 ftcn_right_mask_10_0. (a) + (k) * ftcn_left_mask_10_0 = (e) + (k) * ftcn_right_mask_10_0) -> (exists ftcn_left_mask_10_1 ftcn_right_mask_10_1. (b + f) + (k) * ftcn_left_mask_10_1 = (0) + (k) * ftcn_right_mask_10_1) -> (exists ftcn_left_mask_10_2 ftcn_right_mask_10_2. (c) + (k) * ftcn_left_mask_10_2 = (g) + (k) * ftcn_right_mask_10_2) -> (exists ftcn_left_mask_10_3 ftcn_right_mask_10_3. (d + j) + (k) * ftcn_left_mask_10_3 = (0) + (k) * ftcn_right_mask_10_3) -> k * r = e * e + f * f + g * g + j * j -> (exists fsl_a_fssc_mask_10 fsl_b_fssc_mask_10 fsl_c_fssc_mask_10 fsl_d_fssc_mask_10. (p * r) = fsl_a_fssc_mask_10 * fsl_a_fssc_mask_10 + fsl_b_fssc_mask_10 * fsl_b_fssc_mask_10 + fsl_c_fssc_mask_10 * fsl_c_fssc_mask_10 + fsl_d_fssc_mask_10 * fsl_d_fssc_mask_10)

Proof neighborhood

Direct theorem prerequisites

FS004P four_square_signed_cases_norm_quotient_zero_congruence FS005Z four_square_signed_conjugate_mixed_blocks FS0057 four_square_signed_absolute_block_representation add_assoc · Stable closed add_comm · Stable closed FS0006 four_square_add_swap_right_tail FS0013 four_square_conjugate_absolute_coordinates_total

Direct theorem dependents

FS0058 four_square_signed_centered_representation

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

177 script commands · 30 reading checkpoints · 9 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 (5)
four square signed cases norm quotient zero congruencefour square signed conjugate mixed blocksfour square signed absolute block representationfour square add swap right tailfour square conjugate absolute coordinates total
01Fix variables and assumptionsL1–10

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

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

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

  1. L11
    intro j
  2. L12
    intro r
  3. L13
    intro hnonzero
  4. L14
    intro hodd
  5. L15
    intro hfirst
  6. L16
    intro horientation0
  7. L17
    intro horientation1
  8. L18
    intro horientation2
  9. L19
    intro horientation3
  10. L20
    intro hcenter
03Establish hfirst_permutedL21–30

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. L21
    have hfirst_permuted : p * k = b * b + d * d + a * a + c * c
  2. L22
    trans a * a + b * b + c * c + d * d
  3. L23
    exact hfirst
  4. L24
    trans ((a * a) + ((b * b) + ((c * c) + (d * d))))
  5. L25
    simp [add_assoc]
  6. L26
    trans ((b * b) + ((d * d) + ((a * a) + (c * c))))
  7. L27
    trans ((b * b) + ((a * a) + ((c * c) + (d * d))))
  8. L28
    apply four_square_add_swap_right_tail
  9. L29
    congr
  10. L30
    refl
04Calculate and transport equalitiesL31–34

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

  1. L31
    trans ((d * d) + ((a * a) + (c * c)))
  2. L32
    trans ((a * a) + ((d * d) + (c * c)))
  3. L33
    congr
  4. L34
    refl
05Use earlier factsL35–36

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

  1. L35
    apply add_comm
  2. L36
    apply four_square_add_swap_right_tail
06Calculate and transport equalitiesL37–41

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

  1. L37
    congr
  2. L38
    refl
  3. L39
    refl
  4. L40
    symm
  5. L41
    simp [add_assoc]
07Establish hcenter_permutedL42–51

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. L42
    have hcenter_permuted : k * r = f * f + j * j + e * e + g * g
  2. L43
    trans e * e + f * f + g * g + j * j
  3. L44
    exact hcenter
  4. L45
    trans ((e * e) + ((f * f) + ((g * g) + (j * j))))
  5. L46
    simp [add_assoc]
  6. L47
    trans ((f * f) + ((j * j) + ((e * e) + (g * g))))
  7. L48
    trans ((f * f) + ((e * e) + ((g * g) + (j * j))))
  8. L49
    apply four_square_add_swap_right_tail
  9. L50
    congr
  10. L51
    refl
08Calculate and transport equalitiesL52–55

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

  1. L52
    trans ((j * j) + ((e * e) + (g * g)))
  2. L53
    trans ((e * e) + ((j * j) + (g * g)))
  3. L54
    congr
  4. L55
    refl
09Use earlier factsL56–57

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

  1. L56
    apply add_comm
  2. L57
    apply four_square_add_swap_right_tail
10Calculate and transport equalitiesL58–62

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

  1. L58
    congr
  2. L59
    refl
  3. L60
    refl
  4. L61
    symm
  5. L62
    simp [add_assoc]
11Establish hzeroL63–71

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed cases norm quotient zero congruence.

  1. L63
    have hzero : ModEq(k,f · f + j · j + e · e + g · g,0)Definitions: ModEq(k,f · f + j · j + e · e + g · g,0)Original native command in the exact edition
  2. L64
    specialize four_square_signed_cases_norm_quotient_zero_congruence k
  3. L65
    specialize four_square_signed_cases_norm_quotient_zero_congruence r
  4. L66
    specialize four_square_signed_cases_norm_quotient_zero_congruence f
  5. L67
    specialize four_square_signed_cases_norm_quotient_zero_congruence j
  6. L68
    specialize four_square_signed_cases_norm_quotient_zero_congruence e
  7. L69
    specialize four_square_signed_cases_norm_quotient_zero_congruence g
  8. L70
    apply four_square_signed_cases_norm_quotient_zero_congruence
  9. L71
    exact hcenter_permuted
12Establish hblocksL72–81

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

  1. L72
    have hblocks : ModEq(k,b · g + d · e + a · j + c · f,0) ∧ (ModEq(k,b · e + a · f,d · g + c · j) ∧ (ModEq(k,b · j + c · e,a · g + d · f) ∧ ModEq(k,b · f + d · j,c · g + a · e)))Definitions: ModEq(k,b · g + d · e + a · j + c · f,0)ModEq(k,b · e + a · f,d · g + c · j)ModEq(k,b · j + c · e,a · g + d · f)ModEq(k,b · f + d · j,c · g + a · e)Original native command in the exact edition
  2. L73
    specialize four_square_signed_conjugate_mixed_blocks k
  3. L74
    specialize four_square_signed_conjugate_mixed_blocks b
  4. L75
    specialize four_square_signed_conjugate_mixed_blocks d
  5. L76
    specialize four_square_signed_conjugate_mixed_blocks a
  6. L77
    specialize four_square_signed_conjugate_mixed_blocks c
  7. L78
    specialize four_square_signed_conjugate_mixed_blocks f
  8. L79
    specialize four_square_signed_conjugate_mixed_blocks j
  9. L80
    specialize four_square_signed_conjugate_mixed_blocks e
  10. L81
    specialize four_square_signed_conjugate_mixed_blocks g
13Use earlier factsL82–87

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

  1. L82
    apply four_square_signed_conjugate_mixed_blocks
  2. L83
    exact hzero
  3. L84
    exact horientation1
  4. L85
    exact horientation3
  5. L86
    exact horientation0
  6. L87
    exact horientation2
14Establish hcoordinatesL88–97

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

  1. L88
    have hcoordinates : exists m0 m1 m2 m3. (((((b * g + d * e + a * j + c * f) = (0) + m0) \/ ((0) = (b * g + d * e + a * j + c * f) + m0)) /\ ((((b * e + a * f) = (d * g + c * j) + m1) \/ ((d * g + c * j) = (b * e + a * f) + m1)) /\ ((((b * j + c * e) = (a * g + d * f) + m2) \/ ((a * g + d * f) = (b * j + c * e) + m2)) /\ (((b * f + d * j) = (c * g + a * e) + m3) \/ ((c * g + a * e) = (b * f + d * j) + m3))))) /\ ((b * b + d * d + a * a + c * c) * (g * g + e * e + j * j + f * f) = m0 * m0 + m1 * m1 + m2 * m2 + m3 * m3))
  2. L89
    specialize four_square_conjugate_absolute_coordinates_total b
  3. L90
    specialize four_square_conjugate_absolute_coordinates_total d
  4. L91
    specialize four_square_conjugate_absolute_coordinates_total a
  5. L92
    specialize four_square_conjugate_absolute_coordinates_total c
  6. L93
    specialize four_square_conjugate_absolute_coordinates_total g
  7. L94
    specialize four_square_conjugate_absolute_coordinates_total e
  8. L95
    specialize four_square_conjugate_absolute_coordinates_total j
  9. L96
    specialize four_square_conjugate_absolute_coordinates_total f
  10. L97
    exact four_square_conjugate_absolute_coordinates_total
15Separate the logical casesL98–102

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

  1. L98
    cases hcoordinates
  2. L99
    cases hcoordinates_witness
  3. L100
    cases hcoordinates_witness_witness
  4. L101
    cases hcoordinates_witness_witness_witness
  5. L102
    cases hcoordinates_witness_witness_witness_witness
16Establish habsoluteL103–104

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

  1. L103
    have habsolute : ((((b * g + d * e + a * j + c * f) = (0) + x) \/ ((0) = (b * g + d * e + a * j + c * f) + x)) /\ ((((b * e + a * f) = (d * g + c * j) + x1) \/ ((d * g + c * j) = (b * e + a * f) + x1)) /\ ((((b * j + c * e) = (a * g + d * f) + x2) \/ ((a * g + d * f) = (b * j + c * e) + x2)) /\ (((b * f + d * j) = (c * g + a * e) + x3) \/ ((c * g + a * e) = (b * f + d * j) + x3)))))
  2. L104
    exact hcoordinates_witness_witness_witness_witness_left
17Establish hidentityL105–106

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

  1. L105
    have hidentity : (b * b + d * d + a * a + c * c) * (g * g + e * e + j * j + f * f) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  2. L106
    exact hcoordinates_witness_witness_witness_witness_right
18Establish hcenter_identityL107–116

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

  1. L107
    have hcenter_identity : k * r = g * g + e * e + j * j + f * f
  2. L108
    trans f * f + j * j + e * e + g * g
  3. L109
    exact hcenter_permuted
  4. L110
    trans ((f * f) + ((j * j) + ((e * e) + (g * g))))
  5. L111
    simp [add_assoc]
  6. L112
    trans ((g * g) + ((e * e) + ((j * j) + (f * f))))
  7. L113
    trans ((g * g) + ((f * f) + ((j * j) + (e * e))))
  8. L114
    trans ((f * f) + ((g * g) + ((j * j) + (e * e))))
  9. L115
    congr
  10. L116
    refl
19Calculate and transport equalitiesL117–119

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

  1. L117
    trans ((j * j) + ((g * g) + (e * e)))
  2. L118
    congr
  3. L119
    refl
20Use earlier factsL120–122

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

  1. L120
    apply add_comm
  2. L121
    apply four_square_add_swap_right_tail
  3. L122
    apply four_square_add_swap_right_tail
21Calculate and transport equalitiesL123–128

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

  1. L123
    congr
  2. L124
    refl
  3. L125
    trans ((e * e) + ((f * f) + (j * j)))
  4. L126
    trans ((f * f) + ((e * e) + (j * j)))
  5. L127
    congr
  6. L128
    refl
22Use earlier factsL129–130

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

  1. L129
    apply add_comm
  2. L130
    apply four_square_add_swap_right_tail
23Calculate and transport equalitiesL131–133

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

  1. L131
    congr
  2. L132
    refl
  3. L133
    trans ((j * j) + (f * f))
24Use earlier factsL134–134

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

  1. L134
    apply add_comm
25Calculate and transport equalitiesL135–139

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

  1. L135
    congr
  2. L136
    refl
  3. L137
    refl
  4. L138
    symm
  5. L139
    simp [add_assoc]
26Establish hproductL140–145

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

  1. L140
    have hproduct : (p * k) * (k * r) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  2. L141
    trans (b * b + d * d + a * a + c * c) * (g * g + e * e + j * j + f * f)
  3. L142
    congr
  4. L143
    exact hfirst_permuted
  5. L144
    exact hcenter_identity
  6. L145
    exact hidentity
27Separate the logical casesL146–151

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

  1. L146
    cases hblocks
  2. L147
    cases hblocks_right
  3. L148
    cases hblocks_right_right
  4. L149
    cases habsolute
  5. L150
    cases habsolute_right
  6. L151
    cases habsolute_right_right
28Use earlier factsL152–161

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

  1. L152
    specialize four_square_signed_absolute_block_representation p
  2. L153
    specialize four_square_signed_absolute_block_representation k
  3. L154
    specialize four_square_signed_absolute_block_representation r
  4. L155
    specialize four_square_signed_absolute_block_representation (b * g + d * e + a * j + c * f)
  5. L156
    specialize four_square_signed_absolute_block_representation (b * e + a * f)
  6. L157
    specialize four_square_signed_absolute_block_representation (b * j + c * e)
  7. L158
    specialize four_square_signed_absolute_block_representation (b * f + d * j)
  8. L159
    specialize four_square_signed_absolute_block_representation (0)
  9. L160
    specialize four_square_signed_absolute_block_representation (d * g + c * j)
  10. L161
    specialize four_square_signed_absolute_block_representation (a * g + d * f)
29Use earlier factsL162–171

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

  1. L162
    specialize four_square_signed_absolute_block_representation (c * g + a * e)
  2. L163
    specialize four_square_signed_absolute_block_representation x
  3. L164
    specialize four_square_signed_absolute_block_representation x1
  4. L165
    specialize four_square_signed_absolute_block_representation x2
  5. L166
    specialize four_square_signed_absolute_block_representation x3
  6. L167
    apply four_square_signed_absolute_block_representation
  7. L168
    exact hnonzero
  8. L169
    exact hproduct
  9. L170
    exact hblocks_left
  10. L171
    exact habsolute_left
30Use earlier factsL172–177

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

  1. L172
    exact hblocks_right_left
  2. L173
    exact habsolute_right_left
  3. L174
    exact hblocks_right_right_left
  4. L175
    exact habsolute_right_right_left
  5. L176
    exact hblocks_right_right_right
  6. L177
    exact habsolute_right_right_right

Library-wide reading audit

Original defined command ledger · 177 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro h
  4. 0004intro a
  5. 0005intro b
  6. 0006intro c
  7. 0007intro d
  8. 0008intro e
  9. 0009intro f
  10. 0010intro g
  11. 0011intro j
  12. 0012intro r
  13. 0013intro hnonzero
  14. 0014intro hodd
  15. 0015intro hfirst
  16. 0016intro horientation0
  17. 0017intro horientation1
  18. 0018intro horientation2
  19. 0019intro horientation3
  20. 0020intro hcenter
  21. 0021have hfirst_permuted : p * k = b * b + d * d + a * a + c * c
  22. 0022trans a * a + b * b + c * c + d * d
  23. 0023exact hfirst
  24. 0024trans ((a * a) + ((b * b) + ((c * c) + (d * d))))
  25. 0025simp [add_assoc]
  26. 0026trans ((b * b) + ((d * d) + ((a * a) + (c * c))))
  27. 0027trans ((b * b) + ((a * a) + ((c * c) + (d * d))))
  28. 0028apply four_square_add_swap_right_tail
  29. 0029congr
  30. 0030refl
  31. 0031trans ((d * d) + ((a * a) + (c * c)))
  32. 0032trans ((a * a) + ((d * d) + (c * c)))
  33. 0033congr
  34. 0034refl
  35. 0035apply add_comm
  36. 0036apply four_square_add_swap_right_tail
  37. 0037congr
  38. 0038refl
  39. 0039refl
  40. 0040symm
  41. 0041simp [add_assoc]
  42. 0042have hcenter_permuted : k * r = f * f + j * j + e * e + g * g
  43. 0043trans e * e + f * f + g * g + j * j
  44. 0044exact hcenter
  45. 0045trans ((e * e) + ((f * f) + ((g * g) + (j * j))))
  46. 0046simp [add_assoc]
  47. 0047trans ((f * f) + ((j * j) + ((e * e) + (g * g))))
  48. 0048trans ((f * f) + ((e * e) + ((g * g) + (j * j))))
  49. 0049apply four_square_add_swap_right_tail
  50. 0050congr
  51. 0051refl
  52. 0052trans ((j * j) + ((e * e) + (g * g)))
  53. 0053trans ((e * e) + ((j * j) + (g * g)))
  54. 0054congr
  55. 0055refl
  56. 0056apply add_comm
  57. 0057apply four_square_add_swap_right_tail
  58. 0058congr
  59. 0059refl
  60. 0060refl
  61. 0061symm
  62. 0062simp [add_assoc]
  63. 0063have hzero : ModEq(k,f · f + j · j + e · e + g · g,0)
    Exact native replay linehave hzero : (exists ftcn_left_case_10_zero ftcn_right_case_10_zero. (f * f + j * j + e * e + g * g) + (k) * ftcn_left_case_10_zero = (0) + (k) * ftcn_right_case_10_zero)
  64. 0064specialize four_square_signed_cases_norm_quotient_zero_congruence k
  65. 0065specialize four_square_signed_cases_norm_quotient_zero_congruence r
  66. 0066specialize four_square_signed_cases_norm_quotient_zero_congruence f
  67. 0067specialize four_square_signed_cases_norm_quotient_zero_congruence j
  68. 0068specialize four_square_signed_cases_norm_quotient_zero_congruence e
  69. 0069specialize four_square_signed_cases_norm_quotient_zero_congruence g
  70. 0070apply four_square_signed_cases_norm_quotient_zero_congruence
  71. 0071exact hcenter_permuted
  72. 0072have hblocks : ModEq(k,b · g + d · e + a · j + c · f,0) ∧ (ModEq(k,b · e + a · f,d · g + c · j) ∧ (ModEq(k,b · j + c · e,a · g + d · f) ∧ ModEq(k,b · f + d · j,c · g + a · e)))
    Exact native replay linehave hblocks : ((exists ftcn_left_case_10_block_0 ftcn_right_case_10_block_0. (b * g + d * e + a * j + c * f) + (k) * ftcn_left_case_10_block_0 = (0) + (k) * ftcn_right_case_10_block_0) /\ ((exists ftcn_left_case_10_block_1 ftcn_right_case_10_block_1. (b * e + a * f) + (k) * ftcn_left_case_10_block_1 = (d * g + c * j) + (k) * ftcn_right_case_10_block_1) /\ ((exists ftcn_left_case_10_block_2 ftcn_right_case_10_block_2. (b * j + c * e) + (k) * ftcn_left_case_10_block_2 = (a * g + d * f) + (k) * ftcn_right_case_10_block_2) /\ (exists ftcn_left_case_10_block_3 ftcn_right_case_10_block_3. (b * f + d * j) + (k) * ftcn_left_case_10_block_3 = (c * g + a * e) + (k) * ftcn_right_case_10_block_3))))
  73. 0073specialize four_square_signed_conjugate_mixed_blocks k
  74. 0074specialize four_square_signed_conjugate_mixed_blocks b
  75. 0075specialize four_square_signed_conjugate_mixed_blocks d
  76. 0076specialize four_square_signed_conjugate_mixed_blocks a
  77. 0077specialize four_square_signed_conjugate_mixed_blocks c
  78. 0078specialize four_square_signed_conjugate_mixed_blocks f
  79. 0079specialize four_square_signed_conjugate_mixed_blocks j
  80. 0080specialize four_square_signed_conjugate_mixed_blocks e
  81. 0081specialize four_square_signed_conjugate_mixed_blocks g
  82. 0082apply four_square_signed_conjugate_mixed_blocks
  83. 0083exact hzero
  84. 0084exact horientation1
  85. 0085exact horientation3
  86. 0086exact horientation0
  87. 0087exact horientation2
  88. 0088have hcoordinates : exists m0 m1 m2 m3. (((((b * g + d * e + a * j + c * f) = (0) + m0) \/ ((0) = (b * g + d * e + a * j + c * f) + m0)) /\ ((((b * e + a * f) = (d * g + c * j) + m1) \/ ((d * g + c * j) = (b * e + a * f) + m1)) /\ ((((b * j + c * e) = (a * g + d * f) + m2) \/ ((a * g + d * f) = (b * j + c * e) + m2)) /\ (((b * f + d * j) = (c * g + a * e) + m3) \/ ((c * g + a * e) = (b * f + d * j) + m3))))) /\ ((b * b + d * d + a * a + c * c) * (g * g + e * e + j * j + f * f) = m0 * m0 + m1 * m1 + m2 * m2 + m3 * m3))
  89. 0089specialize four_square_conjugate_absolute_coordinates_total b
  90. 0090specialize four_square_conjugate_absolute_coordinates_total d
  91. 0091specialize four_square_conjugate_absolute_coordinates_total a
  92. 0092specialize four_square_conjugate_absolute_coordinates_total c
  93. 0093specialize four_square_conjugate_absolute_coordinates_total g
  94. 0094specialize four_square_conjugate_absolute_coordinates_total e
  95. 0095specialize four_square_conjugate_absolute_coordinates_total j
  96. 0096specialize four_square_conjugate_absolute_coordinates_total f
  97. 0097exact four_square_conjugate_absolute_coordinates_total
  98. 0098cases hcoordinates
  99. 0099cases hcoordinates_witness
  100. 0100cases hcoordinates_witness_witness
  101. 0101cases hcoordinates_witness_witness_witness
  102. 0102cases hcoordinates_witness_witness_witness_witness
  103. 0103have habsolute : ((((b * g + d * e + a * j + c * f) = (0) + x) \/ ((0) = (b * g + d * e + a * j + c * f) + x)) /\ ((((b * e + a * f) = (d * g + c * j) + x1) \/ ((d * g + c * j) = (b * e + a * f) + x1)) /\ ((((b * j + c * e) = (a * g + d * f) + x2) \/ ((a * g + d * f) = (b * j + c * e) + x2)) /\ (((b * f + d * j) = (c * g + a * e) + x3) \/ ((c * g + a * e) = (b * f + d * j) + x3)))))
  104. 0104exact hcoordinates_witness_witness_witness_witness_left
  105. 0105have hidentity : (b * b + d * d + a * a + c * c) * (g * g + e * e + j * j + f * f) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  106. 0106exact hcoordinates_witness_witness_witness_witness_right
  107. 0107have hcenter_identity : k * r = g * g + e * e + j * j + f * f
  108. 0108trans f * f + j * j + e * e + g * g
  109. 0109exact hcenter_permuted
  110. 0110trans ((f * f) + ((j * j) + ((e * e) + (g * g))))
  111. 0111simp [add_assoc]
  112. 0112trans ((g * g) + ((e * e) + ((j * j) + (f * f))))
  113. 0113trans ((g * g) + ((f * f) + ((j * j) + (e * e))))
  114. 0114trans ((f * f) + ((g * g) + ((j * j) + (e * e))))
  115. 0115congr
  116. 0116refl
  117. 0117trans ((j * j) + ((g * g) + (e * e)))
  118. 0118congr
  119. 0119refl
  120. 0120apply add_comm
  121. 0121apply four_square_add_swap_right_tail
  122. 0122apply four_square_add_swap_right_tail
  123. 0123congr
  124. 0124refl
  125. 0125trans ((e * e) + ((f * f) + (j * j)))
  126. 0126trans ((f * f) + ((e * e) + (j * j)))
  127. 0127congr
  128. 0128refl
  129. 0129apply add_comm
  130. 0130apply four_square_add_swap_right_tail
  131. 0131congr
  132. 0132refl
  133. 0133trans ((j * j) + (f * f))
  134. 0134apply add_comm
  135. 0135congr
  136. 0136refl
  137. 0137refl
  138. 0138symm
  139. 0139simp [add_assoc]
  140. 0140have hproduct : (p * k) * (k * r) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  141. 0141trans (b * b + d * d + a * a + c * c) * (g * g + e * e + j * j + f * f)
  142. 0142congr
  143. 0143exact hfirst_permuted
  144. 0144exact hcenter_identity
  145. 0145exact hidentity
  146. 0146cases hblocks
  147. 0147cases hblocks_right
  148. 0148cases hblocks_right_right
  149. 0149cases habsolute
  150. 0150cases habsolute_right
  151. 0151cases habsolute_right_right
  152. 0152specialize four_square_signed_absolute_block_representation p
  153. 0153specialize four_square_signed_absolute_block_representation k
  154. 0154specialize four_square_signed_absolute_block_representation r
  155. 0155specialize four_square_signed_absolute_block_representation (b * g + d * e + a * j + c * f)
  156. 0156specialize four_square_signed_absolute_block_representation (b * e + a * f)
  157. 0157specialize four_square_signed_absolute_block_representation (b * j + c * e)
  158. 0158specialize four_square_signed_absolute_block_representation (b * f + d * j)
  159. 0159specialize four_square_signed_absolute_block_representation (0)
  160. 0160specialize four_square_signed_absolute_block_representation (d * g + c * j)
  161. 0161specialize four_square_signed_absolute_block_representation (a * g + d * f)
  162. 0162specialize four_square_signed_absolute_block_representation (c * g + a * e)
  163. 0163specialize four_square_signed_absolute_block_representation x
  164. 0164specialize four_square_signed_absolute_block_representation x1
  165. 0165specialize four_square_signed_absolute_block_representation x2
  166. 0166specialize four_square_signed_absolute_block_representation x3
  167. 0167apply four_square_signed_absolute_block_representation
  168. 0168exact hnonzero
  169. 0169exact hproduct
  170. 0170exact hblocks_left
  171. 0171exact habsolute_left
  172. 0172exact hblocks_right_left
  173. 0173exact habsolute_right_left
  174. 0174exact hblocks_right_right_left
  175. 0175exact habsolute_right_right_left
  176. 0176exact hblocks_right_right_right
  177. 0177exact habsolute_right_right_right