FS004W · theorem body

four_square_signed_orientation_mask_06

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

Constructive signed quaternion quotient for centered orientation mask 0110, 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,0) → ModEq(k,d,j) → 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_6_0 ftcn_right_mask_6_0. (a) + (k) * ftcn_left_mask_6_0 = (e) + (k) * ftcn_right_mask_6_0) -> (exists ftcn_left_mask_6_1 ftcn_right_mask_6_1. (b + f) + (k) * ftcn_left_mask_6_1 = (0) + (k) * ftcn_right_mask_6_1) -> (exists ftcn_left_mask_6_2 ftcn_right_mask_6_2. (c + g) + (k) * ftcn_left_mask_6_2 = (0) + (k) * ftcn_right_mask_6_2) -> (exists ftcn_left_mask_6_3 ftcn_right_mask_6_3. (d) + (k) * ftcn_left_mask_6_3 = (j) + (k) * ftcn_right_mask_6_3) -> k * r = e * e + f * f + g * g + j * j -> (exists fsl_a_fssc_mask_6 fsl_b_fssc_mask_6 fsl_c_fssc_mask_6 fsl_d_fssc_mask_6. (p * r) = fsl_a_fssc_mask_6 * fsl_a_fssc_mask_6 + fsl_b_fssc_mask_6 * fsl_b_fssc_mask_6 + fsl_c_fssc_mask_6 * fsl_c_fssc_mask_6 + fsl_d_fssc_mask_6 * fsl_d_fssc_mask_6)

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

169 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 + c * c + a * a + d * d
  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) + ((c * c) + ((a * a) + (d * d))))
  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–31

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

  1. L31
    trans ((c * c) + ((a * a) + (d * d)))
05Use earlier factsL32–32

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

  1. L32
    apply four_square_add_swap_right_tail
06Calculate and transport equalitiesL33–37

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
    refl
  4. L36
    symm
  5. L37
    simp [add_assoc]
07Establish hcenter_permutedL38–47

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

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

  1. L48
    trans ((g * g) + ((e * e) + (j * j)))
09Use earlier factsL49–49

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

  1. L49
    apply four_square_add_swap_right_tail
10Calculate and transport equalitiesL50–54

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

  1. L50
    congr
  2. L51
    refl
  3. L52
    refl
  4. L53
    symm
  5. L54
    simp [add_assoc]
11Establish hzeroL55–63

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. L55
    have hzero : ModEq(k,f · f + g · g + e · e + j · j,0)Definitions: ModEq(k,f · f + g · g + e · e + j · j,0)Original native command in the exact edition
  2. L56
    specialize four_square_signed_cases_norm_quotient_zero_congruence k
  3. L57
    specialize four_square_signed_cases_norm_quotient_zero_congruence r
  4. L58
    specialize four_square_signed_cases_norm_quotient_zero_congruence f
  5. L59
    specialize four_square_signed_cases_norm_quotient_zero_congruence g
  6. L60
    specialize four_square_signed_cases_norm_quotient_zero_congruence e
  7. L61
    specialize four_square_signed_cases_norm_quotient_zero_congruence j
  8. L62
    apply four_square_signed_cases_norm_quotient_zero_congruence
  9. L63
    exact hcenter_permuted
12Establish hblocksL64–73

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

  1. L64
    have hblocks : ModEq(k,b · j + c · e + a · g + d · f,0) ∧ (ModEq(k,b · e + a · f,c · j + d · g) ∧ (ModEq(k,b · g + d · e,a · j + c · f) ∧ ModEq(k,b · f + c · g,d · j + a · e)))Definitions: ModEq(k,b · j + c · e + a · g + d · f,0)ModEq(k,b · e + a · f,c · j + d · g)ModEq(k,b · g + d · e,a · j + c · f)ModEq(k,b · f + c · g,d · j + a · e)Original native command in the exact edition
  2. L65
    specialize four_square_signed_conjugate_mixed_blocks k
  3. L66
    specialize four_square_signed_conjugate_mixed_blocks b
  4. L67
    specialize four_square_signed_conjugate_mixed_blocks c
  5. L68
    specialize four_square_signed_conjugate_mixed_blocks a
  6. L69
    specialize four_square_signed_conjugate_mixed_blocks d
  7. L70
    specialize four_square_signed_conjugate_mixed_blocks f
  8. L71
    specialize four_square_signed_conjugate_mixed_blocks g
  9. L72
    specialize four_square_signed_conjugate_mixed_blocks e
  10. L73
    specialize four_square_signed_conjugate_mixed_blocks j
13Use earlier factsL74–79

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

  1. L74
    apply four_square_signed_conjugate_mixed_blocks
  2. L75
    exact hzero
  3. L76
    exact horientation1
  4. L77
    exact horientation2
  5. L78
    exact horientation0
  6. L79
    exact horientation3
14Establish hcoordinatesL80–89

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

  1. L80
    have hcoordinates : exists m0 m1 m2 m3. (((((b * j + c * e + a * g + d * f) = (0) + m0) \/ ((0) = (b * j + c * e + a * g + d * f) + m0)) /\ ((((b * e + a * f) = (c * j + d * g) + m1) \/ ((c * j + d * g) = (b * e + a * f) + m1)) /\ ((((b * g + d * e) = (a * j + c * f) + m2) \/ ((a * j + c * f) = (b * g + d * e) + m2)) /\ (((b * f + c * g) = (d * j + a * e) + m3) \/ ((d * j + a * e) = (b * f + c * g) + m3))))) /\ ((b * b + c * c + a * a + d * d) * (j * j + e * e + g * g + f * f) = m0 * m0 + m1 * m1 + m2 * m2 + m3 * m3))
  2. L81
    specialize four_square_conjugate_absolute_coordinates_total b
  3. L82
    specialize four_square_conjugate_absolute_coordinates_total c
  4. L83
    specialize four_square_conjugate_absolute_coordinates_total a
  5. L84
    specialize four_square_conjugate_absolute_coordinates_total d
  6. L85
    specialize four_square_conjugate_absolute_coordinates_total j
  7. L86
    specialize four_square_conjugate_absolute_coordinates_total e
  8. L87
    specialize four_square_conjugate_absolute_coordinates_total g
  9. L88
    specialize four_square_conjugate_absolute_coordinates_total f
  10. L89
    exact four_square_conjugate_absolute_coordinates_total
15Separate the logical casesL90–94

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

  1. L90
    cases hcoordinates
  2. L91
    cases hcoordinates_witness
  3. L92
    cases hcoordinates_witness_witness
  4. L93
    cases hcoordinates_witness_witness_witness
  5. L94
    cases hcoordinates_witness_witness_witness_witness
16Establish habsoluteL95–96

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

  1. L95
    have habsolute : ((((b * j + c * e + a * g + d * f) = (0) + x) \/ ((0) = (b * j + c * e + a * g + d * f) + x)) /\ ((((b * e + a * f) = (c * j + d * g) + x1) \/ ((c * j + d * g) = (b * e + a * f) + x1)) /\ ((((b * g + d * e) = (a * j + c * f) + x2) \/ ((a * j + c * f) = (b * g + d * e) + x2)) /\ (((b * f + c * g) = (d * j + a * e) + x3) \/ ((d * j + a * e) = (b * f + c * g) + x3)))))
  2. L96
    exact hcoordinates_witness_witness_witness_witness_left
17Establish hidentityL97–98

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

  1. L97
    have hidentity : (b * b + c * c + a * a + d * d) * (j * j + e * e + g * g + f * f) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  2. L98
    exact hcoordinates_witness_witness_witness_witness_right
18Establish hcenter_identityL99–108

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

  1. L99
    have hcenter_identity : k * r = j * j + e * e + g * g + f * f
  2. L100
    trans f * f + g * g + e * e + j * j
  3. L101
    exact hcenter_permuted
  4. L102
    trans ((f * f) + ((g * g) + ((e * e) + (j * j))))
  5. L103
    simp [add_assoc]
  6. L104
    trans ((j * j) + ((e * e) + ((g * g) + (f * f))))
  7. L105
    trans ((j * j) + ((f * f) + ((g * g) + (e * e))))
  8. L106
    trans ((f * f) + ((j * j) + ((g * g) + (e * e))))
  9. L107
    congr
  10. L108
    refl
19Calculate and transport equalitiesL109–111

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

  1. L109
    trans ((g * g) + ((j * j) + (e * e)))
  2. L110
    congr
  3. L111
    refl
20Use earlier factsL112–114

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

  1. L112
    apply add_comm
  2. L113
    apply four_square_add_swap_right_tail
  3. L114
    apply four_square_add_swap_right_tail
21Calculate and transport equalitiesL115–120

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

  1. L115
    congr
  2. L116
    refl
  3. L117
    trans ((e * e) + ((f * f) + (g * g)))
  4. L118
    trans ((f * f) + ((e * e) + (g * g)))
  5. L119
    congr
  6. L120
    refl
22Use earlier factsL121–122

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

  1. L121
    apply add_comm
  2. L122
    apply four_square_add_swap_right_tail
23Calculate and transport equalitiesL123–125

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 ((g * g) + (f * f))
24Use earlier factsL126–126

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

  1. L126
    apply add_comm
25Calculate and transport equalitiesL127–131

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

  1. L127
    congr
  2. L128
    refl
  3. L129
    refl
  4. L130
    symm
  5. L131
    simp [add_assoc]
26Establish hproductL132–137

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

  1. L132
    have hproduct : (p * k) * (k * r) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  2. L133
    trans (b * b + c * c + a * a + d * d) * (j * j + e * e + g * g + f * f)
  3. L134
    congr
  4. L135
    exact hfirst_permuted
  5. L136
    exact hcenter_identity
  6. L137
    exact hidentity
27Separate the logical casesL138–143

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

  1. L138
    cases hblocks
  2. L139
    cases hblocks_right
  3. L140
    cases hblocks_right_right
  4. L141
    cases habsolute
  5. L142
    cases habsolute_right
  6. L143
    cases habsolute_right_right
28Use earlier factsL144–153

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

  1. L144
    specialize four_square_signed_absolute_block_representation p
  2. L145
    specialize four_square_signed_absolute_block_representation k
  3. L146
    specialize four_square_signed_absolute_block_representation r
  4. L147
    specialize four_square_signed_absolute_block_representation (b * j + c * e + a * g + d * f)
  5. L148
    specialize four_square_signed_absolute_block_representation (b * e + a * f)
  6. L149
    specialize four_square_signed_absolute_block_representation (b * g + d * e)
  7. L150
    specialize four_square_signed_absolute_block_representation (b * f + c * g)
  8. L151
    specialize four_square_signed_absolute_block_representation (0)
  9. L152
    specialize four_square_signed_absolute_block_representation (c * j + d * g)
  10. L153
    specialize four_square_signed_absolute_block_representation (a * j + c * f)
29Use earlier factsL154–163

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

  1. L154
    specialize four_square_signed_absolute_block_representation (d * j + a * e)
  2. L155
    specialize four_square_signed_absolute_block_representation x
  3. L156
    specialize four_square_signed_absolute_block_representation x1
  4. L157
    specialize four_square_signed_absolute_block_representation x2
  5. L158
    specialize four_square_signed_absolute_block_representation x3
  6. L159
    apply four_square_signed_absolute_block_representation
  7. L160
    exact hnonzero
  8. L161
    exact hproduct
  9. L162
    exact hblocks_left
  10. L163
    exact habsolute_left
30Use earlier factsL164–169

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

  1. L164
    exact hblocks_right_left
  2. L165
    exact habsolute_right_left
  3. L166
    exact hblocks_right_right_left
  4. L167
    exact habsolute_right_right_left
  5. L168
    exact hblocks_right_right_right
  6. L169
    exact habsolute_right_right_right

Library-wide reading audit

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