FS004V · theorem body

four_square_signed_orientation_mask_05

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

Constructive signed quaternion quotient for centered orientation mask 0101, 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,0) → ModEq(k,b,f) → 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_5_0 ftcn_right_mask_5_0. (a + e) + (k) * ftcn_left_mask_5_0 = (0) + (k) * ftcn_right_mask_5_0) -> (exists ftcn_left_mask_5_1 ftcn_right_mask_5_1. (b) + (k) * ftcn_left_mask_5_1 = (f) + (k) * ftcn_right_mask_5_1) -> (exists ftcn_left_mask_5_2 ftcn_right_mask_5_2. (c + g) + (k) * ftcn_left_mask_5_2 = (0) + (k) * ftcn_right_mask_5_2) -> (exists ftcn_left_mask_5_3 ftcn_right_mask_5_3. (d) + (k) * ftcn_left_mask_5_3 = (j) + (k) * ftcn_right_mask_5_3) -> k * r = e * e + f * f + g * g + j * j -> (exists fsl_a_fssc_mask_5 fsl_b_fssc_mask_5 fsl_c_fssc_mask_5 fsl_d_fssc_mask_5. (p * r) = fsl_a_fssc_mask_5 * fsl_a_fssc_mask_5 + fsl_b_fssc_mask_5 * fsl_b_fssc_mask_5 + fsl_c_fssc_mask_5 * fsl_c_fssc_mask_5 + fsl_d_fssc_mask_5 * fsl_d_fssc_mask_5)

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

165 script commands · 26 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 = a * a + c * c + b * b + 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 ((a * a) + ((c * c) + ((b * b) + (d * d))))
  7. L27
    congr
  8. L28
    refl
  9. L29
    trans ((c * c) + ((b * b) + (d * d)))
  10. L30
    apply four_square_add_swap_right_tail
04Calculate and transport equalitiesL31–35

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

  1. L31
    congr
  2. L32
    refl
  3. L33
    refl
  4. L34
    symm
  5. L35
    simp [add_assoc]
05Establish hcenter_permutedL36–45

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

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

  1. L46
    congr
  2. L47
    refl
  3. L48
    refl
  4. L49
    symm
  5. L50
    simp [add_assoc]
07Establish hzeroL51–59

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. L51
    have hzero : ModEq(k,e · e + g · g + f · f + j · j,0)Definitions: ModEq(k,e · e + g · g + f · f + j · j,0)Original native command in the exact edition
  2. L52
    specialize four_square_signed_cases_norm_quotient_zero_congruence k
  3. L53
    specialize four_square_signed_cases_norm_quotient_zero_congruence r
  4. L54
    specialize four_square_signed_cases_norm_quotient_zero_congruence e
  5. L55
    specialize four_square_signed_cases_norm_quotient_zero_congruence g
  6. L56
    specialize four_square_signed_cases_norm_quotient_zero_congruence f
  7. L57
    specialize four_square_signed_cases_norm_quotient_zero_congruence j
  8. L58
    apply four_square_signed_cases_norm_quotient_zero_congruence
  9. L59
    exact hcenter_permuted
08Establish hblocksL60–69

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

  1. L60
    have hblocks : ModEq(k,a · j + c · f + b · g + d · e,0) ∧ (ModEq(k,a · f + b · e,c · j + d · g) ∧ (ModEq(k,a · g + d · f,b · j + c · e) ∧ ModEq(k,a · e + c · g,d · j + b · f)))Definitions: ModEq(k,a · j + c · f + b · g + d · e,0)ModEq(k,a · f + b · e,c · j + d · g)ModEq(k,a · g + d · f,b · j + c · e)ModEq(k,a · e + c · g,d · j + b · f)Original native command in the exact edition
  2. L61
    specialize four_square_signed_conjugate_mixed_blocks k
  3. L62
    specialize four_square_signed_conjugate_mixed_blocks a
  4. L63
    specialize four_square_signed_conjugate_mixed_blocks c
  5. L64
    specialize four_square_signed_conjugate_mixed_blocks b
  6. L65
    specialize four_square_signed_conjugate_mixed_blocks d
  7. L66
    specialize four_square_signed_conjugate_mixed_blocks e
  8. L67
    specialize four_square_signed_conjugate_mixed_blocks g
  9. L68
    specialize four_square_signed_conjugate_mixed_blocks f
  10. L69
    specialize four_square_signed_conjugate_mixed_blocks j
09Use earlier factsL70–75

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

  1. L70
    apply four_square_signed_conjugate_mixed_blocks
  2. L71
    exact hzero
  3. L72
    exact horientation0
  4. L73
    exact horientation2
  5. L74
    exact horientation1
  6. L75
    exact horientation3
10Establish hcoordinatesL76–85

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

  1. L76
    have hcoordinates : exists m0 m1 m2 m3. (((((a * j + c * f + b * g + d * e) = (0) + m0) \/ ((0) = (a * j + c * f + b * g + d * e) + m0)) /\ ((((a * f + b * e) = (c * j + d * g) + m1) \/ ((c * j + d * g) = (a * f + b * e) + m1)) /\ ((((a * g + d * f) = (b * j + c * e) + m2) \/ ((b * j + c * e) = (a * g + d * f) + m2)) /\ (((a * e + c * g) = (d * j + b * f) + m3) \/ ((d * j + b * f) = (a * e + c * g) + m3))))) /\ ((a * a + c * c + b * b + d * d) * (j * j + f * f + g * g + e * e) = m0 * m0 + m1 * m1 + m2 * m2 + m3 * m3))
  2. L77
    specialize four_square_conjugate_absolute_coordinates_total a
  3. L78
    specialize four_square_conjugate_absolute_coordinates_total c
  4. L79
    specialize four_square_conjugate_absolute_coordinates_total b
  5. L80
    specialize four_square_conjugate_absolute_coordinates_total d
  6. L81
    specialize four_square_conjugate_absolute_coordinates_total j
  7. L82
    specialize four_square_conjugate_absolute_coordinates_total f
  8. L83
    specialize four_square_conjugate_absolute_coordinates_total g
  9. L84
    specialize four_square_conjugate_absolute_coordinates_total e
  10. L85
    exact four_square_conjugate_absolute_coordinates_total
11Separate the logical casesL86–90

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

  1. L86
    cases hcoordinates
  2. L87
    cases hcoordinates_witness
  3. L88
    cases hcoordinates_witness_witness
  4. L89
    cases hcoordinates_witness_witness_witness
  5. L90
    cases hcoordinates_witness_witness_witness_witness
12Establish habsoluteL91–92

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

  1. L91
    have habsolute : ((((a * j + c * f + b * g + d * e) = (0) + x) \/ ((0) = (a * j + c * f + b * g + d * e) + x)) /\ ((((a * f + b * e) = (c * j + d * g) + x1) \/ ((c * j + d * g) = (a * f + b * e) + x1)) /\ ((((a * g + d * f) = (b * j + c * e) + x2) \/ ((b * j + c * e) = (a * g + d * f) + x2)) /\ (((a * e + c * g) = (d * j + b * f) + x3) \/ ((d * j + b * f) = (a * e + c * g) + x3)))))
  2. L92
    exact hcoordinates_witness_witness_witness_witness_left
13Establish hidentityL93–94

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

  1. L93
    have hidentity : (a * a + c * c + b * b + d * d) * (j * j + f * f + g * g + e * e) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  2. L94
    exact hcoordinates_witness_witness_witness_witness_right
14Establish hcenter_identityL95–104

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

  1. L95
    have hcenter_identity : k * r = j * j + f * f + g * g + e * e
  2. L96
    trans e * e + g * g + f * f + j * j
  3. L97
    exact hcenter_permuted
  4. L98
    trans ((e * e) + ((g * g) + ((f * f) + (j * j))))
  5. L99
    simp [add_assoc]
  6. L100
    trans ((j * j) + ((f * f) + ((g * g) + (e * e))))
  7. L101
    trans ((j * j) + ((e * e) + ((g * g) + (f * f))))
  8. L102
    trans ((e * e) + ((j * j) + ((g * g) + (f * f))))
  9. L103
    congr
  10. L104
    refl
15Calculate and transport equalitiesL105–107

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

  1. L105
    trans ((g * g) + ((j * j) + (f * f)))
  2. L106
    congr
  3. L107
    refl
16Use earlier factsL108–110

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

  1. L108
    apply add_comm
  2. L109
    apply four_square_add_swap_right_tail
  3. L110
    apply four_square_add_swap_right_tail
17Calculate and transport equalitiesL111–116

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

  1. L111
    congr
  2. L112
    refl
  3. L113
    trans ((f * f) + ((e * e) + (g * g)))
  4. L114
    trans ((e * e) + ((f * f) + (g * g)))
  5. L115
    congr
  6. L116
    refl
18Use earlier factsL117–118

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

  1. L117
    apply add_comm
  2. L118
    apply four_square_add_swap_right_tail
19Calculate and transport equalitiesL119–121

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

  1. L119
    congr
  2. L120
    refl
  3. L121
    trans ((g * g) + (e * e))
20Use earlier factsL122–122

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

  1. L122
    apply add_comm
21Calculate and transport equalitiesL123–127

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
    refl
  4. L126
    symm
  5. L127
    simp [add_assoc]
22Establish hproductL128–133

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

  1. L128
    have hproduct : (p * k) * (k * r) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  2. L129
    trans (a * a + c * c + b * b + d * d) * (j * j + f * f + g * g + e * e)
  3. L130
    congr
  4. L131
    exact hfirst_permuted
  5. L132
    exact hcenter_identity
  6. L133
    exact hidentity
23Separate the logical casesL134–139

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

  1. L134
    cases hblocks
  2. L135
    cases hblocks_right
  3. L136
    cases hblocks_right_right
  4. L137
    cases habsolute
  5. L138
    cases habsolute_right
  6. L139
    cases habsolute_right_right
24Use earlier factsL140–149

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

  1. L140
    specialize four_square_signed_absolute_block_representation p
  2. L141
    specialize four_square_signed_absolute_block_representation k
  3. L142
    specialize four_square_signed_absolute_block_representation r
  4. L143
    specialize four_square_signed_absolute_block_representation (a * j + c * f + b * g + d * e)
  5. L144
    specialize four_square_signed_absolute_block_representation (a * f + b * e)
  6. L145
    specialize four_square_signed_absolute_block_representation (a * g + d * f)
  7. L146
    specialize four_square_signed_absolute_block_representation (a * e + c * g)
  8. L147
    specialize four_square_signed_absolute_block_representation (0)
  9. L148
    specialize four_square_signed_absolute_block_representation (c * j + d * g)
  10. L149
    specialize four_square_signed_absolute_block_representation (b * j + c * e)
25Use earlier factsL150–159

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

  1. L150
    specialize four_square_signed_absolute_block_representation (d * j + b * f)
  2. L151
    specialize four_square_signed_absolute_block_representation x
  3. L152
    specialize four_square_signed_absolute_block_representation x1
  4. L153
    specialize four_square_signed_absolute_block_representation x2
  5. L154
    specialize four_square_signed_absolute_block_representation x3
  6. L155
    apply four_square_signed_absolute_block_representation
  7. L156
    exact hnonzero
  8. L157
    exact hproduct
  9. L158
    exact hblocks_left
  10. L159
    exact habsolute_left
26Use earlier factsL160–165

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

  1. L160
    exact hblocks_right_left
  2. L161
    exact habsolute_right_left
  3. L162
    exact hblocks_right_right_left
  4. L163
    exact habsolute_right_right_left
  5. L164
    exact hblocks_right_right_right
  6. L165
    exact habsolute_right_right_right

Library-wide reading audit

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