FS004Z

four_square_signed_orientation_mask_09

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Constructive signed quaternion quotient for centered orientation mask 1001, 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.

Exact expanded first-order arithmetic 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_9_0 ftcn_right_mask_9_0. (a + e) + (k) * ftcn_left_mask_9_0 = (0) + (k) * ftcn_right_mask_9_0) -> (exists ftcn_left_mask_9_1 ftcn_right_mask_9_1. (b) + (k) * ftcn_left_mask_9_1 = (f) + (k) * ftcn_right_mask_9_1) -> (exists ftcn_left_mask_9_2 ftcn_right_mask_9_2. (c) + (k) * ftcn_left_mask_9_2 = (g) + (k) * ftcn_right_mask_9_2) -> (exists ftcn_left_mask_9_3 ftcn_right_mask_9_3. (d + j) + (k) * ftcn_left_mask_9_3 = (0) + (k) * ftcn_right_mask_9_3) -> k * r = e * e + f * f + g * g + j * j -> (exists fsl_a_fssc_mask_9 fsl_b_fssc_mask_9 fsl_c_fssc_mask_9 fsl_d_fssc_mask_9. (p * r) = fsl_a_fssc_mask_9 * fsl_a_fssc_mask_9 + fsl_b_fssc_mask_9 * fsl_b_fssc_mask_9 + fsl_c_fssc_mask_9 * fsl_c_fssc_mask_9 + fsl_d_fssc_mask_9 * fsl_d_fssc_mask_9)

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 7 declared prerequisites and contains 173 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

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 theorem; checked-use authorized add_comm Stable theorem; checked-use authorized FS0006 four_square_add_swap_right_tail FS0013 four_square_conjugate_absolute_coordinates_total

Direct dependents

FS0058 four_square_signed_centered_representation

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

173 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.

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

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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 = a * a + d * d + b * b + 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 ((a * a) + ((d * d) + ((b * b) + (c * c))))
  7. L27
    congr
  8. L28
    refl
  9. L29
    trans ((d * d) + ((b * b) + (c * c)))
  10. L30
    trans ((b * b) + ((d * d) + (c * c)))
04Calculate and transport equalitiesL31–32

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

  1. L31
    congr
  2. L32
    refl
05Use earlier factsL33–34

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

  1. L33
    apply add_comm
  2. L34
    apply four_square_add_swap_right_tail
06Calculate and transport equalitiesL35–39

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

  1. L35
    congr
  2. L36
    refl
  3. L37
    refl
  4. L38
    symm
  5. L39
    simp [add_assoc]
07Establish hcenter_permutedL40–49

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

  1. L40
    have hcenter_permuted : k * r = e * e + j * j + f * f + g * g
  2. L41
    trans e * e + f * f + g * g + j * j
  3. L42
    exact hcenter
  4. L43
    trans ((e * e) + ((f * f) + ((g * g) + (j * j))))
  5. L44
    simp [add_assoc]
  6. L45
    trans ((e * e) + ((j * j) + ((f * f) + (g * g))))
  7. L46
    congr
  8. L47
    refl
  9. L48
    trans ((j * j) + ((f * f) + (g * g)))
  10. L49
    trans ((f * f) + ((j * j) + (g * g)))
08Calculate and transport equalitiesL50–51

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

  1. L50
    congr
  2. L51
    refl
09Use earlier factsL52–53

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

  1. L52
    apply add_comm
  2. L53
    apply four_square_add_swap_right_tail
10Calculate and transport equalitiesL54–58

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

  1. L54
    congr
  2. L55
    refl
  3. L56
    refl
  4. L57
    symm
  5. L58
    simp [add_assoc]
11Establish hzeroL59–67

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. L59
    have hzero : (exists ftcn_left_case_9_zero ftcn_right_case_9_zero. (e * e + j * j + f * f + g * g) + (k) * ftcn_left_case_9_zero = (0) + (k) * ftcn_right_case_9_zero)
  2. L60
    specialize four_square_signed_cases_norm_quotient_zero_congruence k
  3. L61
    specialize four_square_signed_cases_norm_quotient_zero_congruence r
  4. L62
    specialize four_square_signed_cases_norm_quotient_zero_congruence e
  5. L63
    specialize four_square_signed_cases_norm_quotient_zero_congruence j
  6. L64
    specialize four_square_signed_cases_norm_quotient_zero_congruence f
  7. L65
    specialize four_square_signed_cases_norm_quotient_zero_congruence g
  8. L66
    apply four_square_signed_cases_norm_quotient_zero_congruence
  9. L67
    exact hcenter_permuted
12Establish hblocksL68–77

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

  1. L68
    have hblocks : ModEq(k,a · g + d · f + b · j + c · e,0) ∧ (ModEq(k,a · f + b · e,d · g + c · j) ∧ (ModEq(k,a · j + c · f,b · g + d · e) ∧ ModEq(k,a · e + d · j,c · g + b · f)))Definitions: ModEq
  2. L69
    specialize four_square_signed_conjugate_mixed_blocks k
  3. L70
    specialize four_square_signed_conjugate_mixed_blocks a
  4. L71
    specialize four_square_signed_conjugate_mixed_blocks d
  5. L72
    specialize four_square_signed_conjugate_mixed_blocks b
  6. L73
    specialize four_square_signed_conjugate_mixed_blocks c
  7. L74
    specialize four_square_signed_conjugate_mixed_blocks e
  8. L75
    specialize four_square_signed_conjugate_mixed_blocks j
  9. L76
    specialize four_square_signed_conjugate_mixed_blocks f
  10. L77
    specialize four_square_signed_conjugate_mixed_blocks g
13Use earlier factsL78–83

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

  1. L78
    apply four_square_signed_conjugate_mixed_blocks
  2. L79
    exact hzero
  3. L80
    exact horientation0
  4. L81
    exact horientation3
  5. L82
    exact horientation1
  6. L83
    exact horientation2
14Establish hcoordinatesL84–93

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

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

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

  1. L94
    cases hcoordinates
  2. L95
    cases hcoordinates_witness
  3. L96
    cases hcoordinates_witness_witness
  4. L97
    cases hcoordinates_witness_witness_witness
  5. L98
    cases hcoordinates_witness_witness_witness_witness
16Establish habsoluteL99–100

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

  1. L99
    have habsolute : ((((a * g + d * f + b * j + c * e) = (0) + x) \/ ((0) = (a * g + d * f + b * j + c * e) + x)) /\ ((((a * f + b * e) = (d * g + c * j) + x1) \/ ((d * g + c * j) = (a * f + b * e) + x1)) /\ ((((a * j + c * f) = (b * g + d * e) + x2) \/ ((b * g + d * e) = (a * j + c * f) + x2)) /\ (((a * e + d * j) = (c * g + b * f) + x3) \/ ((c * g + b * f) = (a * e + d * j) + x3)))))
  2. L100
    exact hcoordinates_witness_witness_witness_witness_left
17Establish hidentityL101–102

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

  1. L101
    have hidentity : (a * a + d * d + b * b + c * c) * (g * g + f * f + j * j + e * e) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  2. L102
    exact hcoordinates_witness_witness_witness_witness_right
18Establish hcenter_identityL103–112

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

  1. L103
    have hcenter_identity : k * r = g * g + f * f + j * j + e * e
  2. L104
    trans e * e + j * j + f * f + g * g
  3. L105
    exact hcenter_permuted
  4. L106
    trans ((e * e) + ((j * j) + ((f * f) + (g * g))))
  5. L107
    simp [add_assoc]
  6. L108
    trans ((g * g) + ((f * f) + ((j * j) + (e * e))))
  7. L109
    trans ((g * g) + ((e * e) + ((j * j) + (f * f))))
  8. L110
    trans ((e * e) + ((g * g) + ((j * j) + (f * f))))
  9. L111
    congr
  10. L112
    refl
19Calculate and transport equalitiesL113–115

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

  1. L113
    trans ((j * j) + ((g * g) + (f * f)))
  2. L114
    congr
  3. L115
    refl
20Use earlier factsL116–118

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

  1. L116
    apply add_comm
  2. L117
    apply four_square_add_swap_right_tail
  3. L118
    apply four_square_add_swap_right_tail
21Calculate and transport equalitiesL119–124

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 ((f * f) + ((e * e) + (j * j)))
  4. L122
    trans ((e * e) + ((f * f) + (j * j)))
  5. L123
    congr
  6. L124
    refl
22Use earlier factsL125–126

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

  1. L125
    apply add_comm
  2. L126
    apply four_square_add_swap_right_tail
23Calculate and transport equalitiesL127–129

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
    trans ((j * j) + (e * e))
24Use earlier factsL130–130

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

  1. L130
    apply add_comm
25Calculate and transport equalitiesL131–135

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
    refl
  4. L134
    symm
  5. L135
    simp [add_assoc]
26Establish hproductL136–141

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

  1. L136
    have hproduct : (p * k) * (k * r) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  2. L137
    trans (a * a + d * d + b * b + c * c) * (g * g + f * f + j * j + e * e)
  3. L138
    congr
  4. L139
    exact hfirst_permuted
  5. L140
    exact hcenter_identity
  6. L141
    exact hidentity
27Separate the logical casesL142–147

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

  1. L142
    cases hblocks
  2. L143
    cases hblocks_right
  3. L144
    cases hblocks_right_right
  4. L145
    cases habsolute
  5. L146
    cases habsolute_right
  6. L147
    cases habsolute_right_right
28Use earlier factsL148–157

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

  1. L148
    specialize four_square_signed_absolute_block_representation p
  2. L149
    specialize four_square_signed_absolute_block_representation k
  3. L150
    specialize four_square_signed_absolute_block_representation r
  4. L151
    specialize four_square_signed_absolute_block_representation (a * g + d * f + b * j + c * e)
  5. L152
    specialize four_square_signed_absolute_block_representation (a * f + b * e)
  6. L153
    specialize four_square_signed_absolute_block_representation (a * j + c * f)
  7. L154
    specialize four_square_signed_absolute_block_representation (a * e + d * j)
  8. L155
    specialize four_square_signed_absolute_block_representation (0)
  9. L156
    specialize four_square_signed_absolute_block_representation (d * g + c * j)
  10. L157
    specialize four_square_signed_absolute_block_representation (b * g + d * e)
29Use earlier factsL158–167

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

  1. L158
    specialize four_square_signed_absolute_block_representation (c * g + b * f)
  2. L159
    specialize four_square_signed_absolute_block_representation x
  3. L160
    specialize four_square_signed_absolute_block_representation x1
  4. L161
    specialize four_square_signed_absolute_block_representation x2
  5. L162
    specialize four_square_signed_absolute_block_representation x3
  6. L163
    apply four_square_signed_absolute_block_representation
  7. L164
    exact hnonzero
  8. L165
    exact hproduct
  9. L166
    exact hblocks_left
  10. L167
    exact habsolute_left
30Use earlier factsL168–173

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

  1. L168
    exact hblocks_right_left
  2. L169
    exact habsolute_right_left
  3. L170
    exact hblocks_right_right_left
  4. L171
    exact habsolute_right_right_left
  5. L172
    exact hblocks_right_right_right
  6. L173
    exact habsolute_right_right_right

Library-wide reading audit

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