FS0052 · theorem body

four_square_signed_orientation_mask_12

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

Constructive signed quaternion quotient for centered orientation mask 1100, 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) → ModEq(k,c + g,0) → 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_12_0 ftcn_right_mask_12_0. (a) + (k) * ftcn_left_mask_12_0 = (e) + (k) * ftcn_right_mask_12_0) -> (exists ftcn_left_mask_12_1 ftcn_right_mask_12_1. (b) + (k) * ftcn_left_mask_12_1 = (f) + (k) * ftcn_right_mask_12_1) -> (exists ftcn_left_mask_12_2 ftcn_right_mask_12_2. (c + g) + (k) * ftcn_left_mask_12_2 = (0) + (k) * ftcn_right_mask_12_2) -> (exists ftcn_left_mask_12_3 ftcn_right_mask_12_3. (d + j) + (k) * ftcn_left_mask_12_3 = (0) + (k) * ftcn_right_mask_12_3) -> k * r = e * e + f * f + g * g + j * j -> (exists fsl_a_fssc_mask_12 fsl_b_fssc_mask_12 fsl_c_fssc_mask_12 fsl_d_fssc_mask_12. (p * r) = fsl_a_fssc_mask_12 * fsl_a_fssc_mask_12 + fsl_b_fssc_mask_12 * fsl_b_fssc_mask_12 + fsl_c_fssc_mask_12 * fsl_c_fssc_mask_12 + fsl_d_fssc_mask_12 * fsl_d_fssc_mask_12)

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

185 script commands · 32 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.

  1. L21
    have hfirst_permuted : p * k = c * c + d * d + a * a + b * b
  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 ((c * c) + ((d * d) + ((a * a) + (b * b))))
  7. L27
    trans ((c * c) + ((a * a) + ((b * b) + (d * d))))
  8. L28
    trans ((a * a) + ((c * c) + ((b * b) + (d * d))))
  9. L29
    congr
  10. L30
    refl
04Use earlier factsL31–32

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

  1. L31
    apply four_square_add_swap_right_tail
  2. L32
    apply four_square_add_swap_right_tail
05Calculate and transport equalitiesL33–38

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

  1. L33
    congr
  2. L34
    refl
  3. L35
    trans ((d * d) + ((a * a) + (b * b)))
  4. L36
    trans ((a * a) + ((d * d) + (b * b)))
  5. L37
    congr
  6. L38
    refl
06Use earlier factsL39–40

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

  1. L39
    apply add_comm
  2. L40
    apply four_square_add_swap_right_tail
07Calculate and transport equalitiesL41–45

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

  1. L41
    congr
  2. L42
    refl
  3. L43
    refl
  4. L44
    symm
  5. L45
    simp [add_assoc]
08Establish hcenter_permutedL46–55

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

  1. L46
    have hcenter_permuted : k * r = g * g + j * j + e * e + f * f
  2. L47
    trans e * e + f * f + g * g + j * j
  3. L48
    exact hcenter
  4. L49
    trans ((e * e) + ((f * f) + ((g * g) + (j * j))))
  5. L50
    simp [add_assoc]
  6. L51
    trans ((g * g) + ((j * j) + ((e * e) + (f * f))))
  7. L52
    trans ((g * g) + ((e * e) + ((f * f) + (j * j))))
  8. L53
    trans ((e * e) + ((g * g) + ((f * f) + (j * j))))
  9. L54
    congr
  10. L55
    refl
09Use earlier factsL56–57

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

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

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
    trans ((j * j) + ((e * e) + (f * f)))
  4. L61
    trans ((e * e) + ((j * j) + (f * f)))
  5. L62
    congr
  6. L63
    refl
11Use earlier factsL64–65

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

  1. L64
    apply add_comm
  2. L65
    apply four_square_add_swap_right_tail
12Calculate and transport equalitiesL66–70

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

  1. L66
    congr
  2. L67
    refl
  3. L68
    refl
  4. L69
    symm
  5. L70
    simp [add_assoc]
13Establish hzeroL71–79

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. L71
    have hzero : ModEq(k,g · g + j · j + e · e + f · f,0)Definitions: ModEq(k,g · g + j · j + e · e + f · f,0)Original native command in the exact edition
  2. L72
    specialize four_square_signed_cases_norm_quotient_zero_congruence k
  3. L73
    specialize four_square_signed_cases_norm_quotient_zero_congruence r
  4. L74
    specialize four_square_signed_cases_norm_quotient_zero_congruence g
  5. L75
    specialize four_square_signed_cases_norm_quotient_zero_congruence j
  6. L76
    specialize four_square_signed_cases_norm_quotient_zero_congruence e
  7. L77
    specialize four_square_signed_cases_norm_quotient_zero_congruence f
  8. L78
    apply four_square_signed_cases_norm_quotient_zero_congruence
  9. L79
    exact hcenter_permuted
14Establish hblocksL80–89

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

  1. L80
    have hblocks : ModEq(k,c · f + d · e + a · j + b · g,0) ∧ (ModEq(k,c · e + a · g,d · f + b · j) ∧ (ModEq(k,c · j + b · e,a · f + d · g) ∧ ModEq(k,c · g + d · j,b · f + a · e)))Definitions: ModEq(k,c · f + d · e + a · j + b · g,0)ModEq(k,c · e + a · g,d · f + b · j)ModEq(k,c · j + b · e,a · f + d · g)ModEq(k,c · g + d · j,b · f + a · e)Original native command in the exact edition
  2. L81
    specialize four_square_signed_conjugate_mixed_blocks k
  3. L82
    specialize four_square_signed_conjugate_mixed_blocks c
  4. L83
    specialize four_square_signed_conjugate_mixed_blocks d
  5. L84
    specialize four_square_signed_conjugate_mixed_blocks a
  6. L85
    specialize four_square_signed_conjugate_mixed_blocks b
  7. L86
    specialize four_square_signed_conjugate_mixed_blocks g
  8. L87
    specialize four_square_signed_conjugate_mixed_blocks j
  9. L88
    specialize four_square_signed_conjugate_mixed_blocks e
  10. L89
    specialize four_square_signed_conjugate_mixed_blocks f
15Use earlier factsL90–95

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

  1. L90
    apply four_square_signed_conjugate_mixed_blocks
  2. L91
    exact hzero
  3. L92
    exact horientation2
  4. L93
    exact horientation3
  5. L94
    exact horientation0
  6. L95
    exact horientation1
16Establish hcoordinatesL96–105

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

  1. L96
    have hcoordinates : exists m0 m1 m2 m3. (((((c * f + d * e + a * j + b * g) = (0) + m0) \/ ((0) = (c * f + d * e + a * j + b * g) + m0)) /\ ((((c * e + a * g) = (d * f + b * j) + m1) \/ ((d * f + b * j) = (c * e + a * g) + m1)) /\ ((((c * j + b * e) = (a * f + d * g) + m2) \/ ((a * f + d * g) = (c * j + b * e) + m2)) /\ (((c * g + d * j) = (b * f + a * e) + m3) \/ ((b * f + a * e) = (c * g + d * j) + m3))))) /\ ((c * c + d * d + a * a + b * b) * (f * f + e * e + j * j + g * g) = m0 * m0 + m1 * m1 + m2 * m2 + m3 * m3))
  2. L97
    specialize four_square_conjugate_absolute_coordinates_total c
  3. L98
    specialize four_square_conjugate_absolute_coordinates_total d
  4. L99
    specialize four_square_conjugate_absolute_coordinates_total a
  5. L100
    specialize four_square_conjugate_absolute_coordinates_total b
  6. L101
    specialize four_square_conjugate_absolute_coordinates_total f
  7. L102
    specialize four_square_conjugate_absolute_coordinates_total e
  8. L103
    specialize four_square_conjugate_absolute_coordinates_total j
  9. L104
    specialize four_square_conjugate_absolute_coordinates_total g
  10. L105
    exact four_square_conjugate_absolute_coordinates_total
17Separate the logical casesL106–110

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

  1. L106
    cases hcoordinates
  2. L107
    cases hcoordinates_witness
  3. L108
    cases hcoordinates_witness_witness
  4. L109
    cases hcoordinates_witness_witness_witness
  5. L110
    cases hcoordinates_witness_witness_witness_witness
18Establish habsoluteL111–112

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

  1. L111
    have habsolute : ((((c * f + d * e + a * j + b * g) = (0) + x) \/ ((0) = (c * f + d * e + a * j + b * g) + x)) /\ ((((c * e + a * g) = (d * f + b * j) + x1) \/ ((d * f + b * j) = (c * e + a * g) + x1)) /\ ((((c * j + b * e) = (a * f + d * g) + x2) \/ ((a * f + d * g) = (c * j + b * e) + x2)) /\ (((c * g + d * j) = (b * f + a * e) + x3) \/ ((b * f + a * e) = (c * g + d * j) + x3)))))
  2. L112
    exact hcoordinates_witness_witness_witness_witness_left
19Establish hidentityL113–114

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

  1. L113
    have hidentity : (c * c + d * d + a * a + b * b) * (f * f + e * e + j * j + g * g) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  2. L114
    exact hcoordinates_witness_witness_witness_witness_right
20Establish hcenter_identityL115–124

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

  1. L115
    have hcenter_identity : k * r = f * f + e * e + j * j + g * g
  2. L116
    trans g * g + j * j + e * e + f * f
  3. L117
    exact hcenter_permuted
  4. L118
    trans ((g * g) + ((j * j) + ((e * e) + (f * f))))
  5. L119
    simp [add_assoc]
  6. L120
    trans ((f * f) + ((e * e) + ((j * j) + (g * g))))
  7. L121
    trans ((f * f) + ((g * g) + ((j * j) + (e * e))))
  8. L122
    trans ((g * g) + ((f * f) + ((j * j) + (e * e))))
  9. L123
    congr
  10. L124
    refl
21Calculate and transport equalitiesL125–127

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

  1. L125
    trans ((j * j) + ((f * f) + (e * e)))
  2. L126
    congr
  3. L127
    refl
22Use earlier factsL128–130

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

  1. L128
    apply add_comm
  2. L129
    apply four_square_add_swap_right_tail
  3. L130
    apply four_square_add_swap_right_tail
23Calculate and transport equalitiesL131–136

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 ((e * e) + ((g * g) + (j * j)))
  4. L134
    trans ((g * g) + ((e * e) + (j * j)))
  5. L135
    congr
  6. L136
    refl
24Use earlier factsL137–138

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

  1. L137
    apply add_comm
  2. L138
    apply four_square_add_swap_right_tail
25Calculate and transport equalitiesL139–141

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

  1. L139
    congr
  2. L140
    refl
  3. L141
    trans ((j * j) + (g * g))
26Use earlier factsL142–142

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

  1. L142
    apply add_comm
27Calculate and transport equalitiesL143–147

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

  1. L143
    congr
  2. L144
    refl
  3. L145
    refl
  4. L146
    symm
  5. L147
    simp [add_assoc]
28Establish hproductL148–153

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

  1. L148
    have hproduct : (p * k) * (k * r) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  2. L149
    trans (c * c + d * d + a * a + b * b) * (f * f + e * e + j * j + g * g)
  3. L150
    congr
  4. L151
    exact hfirst_permuted
  5. L152
    exact hcenter_identity
  6. L153
    exact hidentity
29Separate the logical casesL154–159

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

  1. L154
    cases hblocks
  2. L155
    cases hblocks_right
  3. L156
    cases hblocks_right_right
  4. L157
    cases habsolute
  5. L158
    cases habsolute_right
  6. L159
    cases habsolute_right_right
30Use earlier factsL160–169

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

  1. L160
    specialize four_square_signed_absolute_block_representation p
  2. L161
    specialize four_square_signed_absolute_block_representation k
  3. L162
    specialize four_square_signed_absolute_block_representation r
  4. L163
    specialize four_square_signed_absolute_block_representation (c * f + d * e + a * j + b * g)
  5. L164
    specialize four_square_signed_absolute_block_representation (c * e + a * g)
  6. L165
    specialize four_square_signed_absolute_block_representation (c * j + b * e)
  7. L166
    specialize four_square_signed_absolute_block_representation (c * g + d * j)
  8. L167
    specialize four_square_signed_absolute_block_representation (0)
  9. L168
    specialize four_square_signed_absolute_block_representation (d * f + b * j)
  10. L169
    specialize four_square_signed_absolute_block_representation (a * f + d * g)
31Use earlier factsL170–179

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

  1. L170
    specialize four_square_signed_absolute_block_representation (b * f + a * e)
  2. L171
    specialize four_square_signed_absolute_block_representation x
  3. L172
    specialize four_square_signed_absolute_block_representation x1
  4. L173
    specialize four_square_signed_absolute_block_representation x2
  5. L174
    specialize four_square_signed_absolute_block_representation x3
  6. L175
    apply four_square_signed_absolute_block_representation
  7. L176
    exact hnonzero
  8. L177
    exact hproduct
  9. L178
    exact hblocks_left
  10. L179
    exact habsolute_left
32Use earlier factsL180–185

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

  1. L180
    exact hblocks_right_left
  2. L181
    exact habsolute_right_left
  3. L182
    exact hblocks_right_right_left
  4. L183
    exact habsolute_right_right_left
  5. L184
    exact hblocks_right_right_right
  6. L185
    exact habsolute_right_right_right

Library-wide reading audit

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