FS004S · theorem body

four_square_signed_orientation_mask_02

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

Constructive signed quaternion quotient for centered orientation mask 0010, using the exact four_square_signed_natural_negative_first_blocks surface.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ p. ∀ k. ∀ h. ∀ a. ∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ j. ∀ r. ¬k = 0 → k = 2 · h + 1 → p · k = a · a + b · b + c · c + d · d → ModEq(k,a,e) → ModEq(k,b + f,0) → ModEq(k,c,g) → ModEq(k,d,j) → 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_2_0 ftcn_right_mask_2_0. (a) + (k) * ftcn_left_mask_2_0 = (e) + (k) * ftcn_right_mask_2_0) -> (exists ftcn_left_mask_2_1 ftcn_right_mask_2_1. (b + f) + (k) * ftcn_left_mask_2_1 = (0) + (k) * ftcn_right_mask_2_1) -> (exists ftcn_left_mask_2_2 ftcn_right_mask_2_2. (c) + (k) * ftcn_left_mask_2_2 = (g) + (k) * ftcn_right_mask_2_2) -> (exists ftcn_left_mask_2_3 ftcn_right_mask_2_3. (d) + (k) * ftcn_left_mask_2_3 = (j) + (k) * ftcn_right_mask_2_3) -> k * r = e * e + f * f + g * g + j * j -> (exists fsl_a_fssc_mask_2 fsl_b_fssc_mask_2 fsl_c_fssc_mask_2 fsl_d_fssc_mask_2. (p * r) = fsl_a_fssc_mask_2 * fsl_a_fssc_mask_2 + fsl_b_fssc_mask_2 * fsl_b_fssc_mask_2 + fsl_c_fssc_mask_2 * fsl_c_fssc_mask_2 + fsl_d_fssc_mask_2 * fsl_d_fssc_mask_2)

Proof neighborhood

Direct theorem prerequisites

FS004P four_square_signed_cases_norm_quotient_zero_congruence FS0060 four_square_signed_natural_negative_first_blocks FS0057 four_square_signed_absolute_block_representation add_assoc · Stable closed add_comm · Stable closed FS0006 four_square_add_swap_right_tail FS0005 quaternion_coordinate_absolute_total FS002Y four_square_euler_quaternion

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

144 script commands · 20 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 (6)
four square signed cases norm quotient zero congruencefour square signed natural negative first blocksfour square signed absolute block representationfour square add swap right tailquaternion coordinate absolute totalfour square euler quaternion
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 + a * a + c * c + 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) + ((a * a) + ((c * c) + (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–33

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

  1. L31
    refl
  2. L32
    symm
  3. L33
    simp [add_assoc]
05Establish hcenter_permutedL34–43

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

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

  1. L44
    refl
  2. L45
    symm
  3. L46
    simp [add_assoc]
07Establish hzeroL47–55

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

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

  1. L56
    have hblocks : ModEq(k,b · f,a · e + c · g + d · j) ∧ (ModEq(k,b · e + a · f + c · j,d · g) ∧ (ModEq(k,b · g + c · f + d · e,a · j) ∧ ModEq(k,b · j + a · g + d · f,c · e)))Definitions: ModEq(k,b · f,a · e + c · g + d · j)ModEq(k,b · e + a · f + c · j,d · g)ModEq(k,b · g + c · f + d · e,a · j)ModEq(k,b · j + a · g + d · f,c · e)Original native command in the exact edition
  2. L57
    specialize four_square_signed_natural_negative_first_blocks k
  3. L58
    specialize four_square_signed_natural_negative_first_blocks b
  4. L59
    specialize four_square_signed_natural_negative_first_blocks a
  5. L60
    specialize four_square_signed_natural_negative_first_blocks c
  6. L61
    specialize four_square_signed_natural_negative_first_blocks d
  7. L62
    specialize four_square_signed_natural_negative_first_blocks f
  8. L63
    specialize four_square_signed_natural_negative_first_blocks e
  9. L64
    specialize four_square_signed_natural_negative_first_blocks g
  10. L65
    specialize four_square_signed_natural_negative_first_blocks j
09Use earlier factsL66–71

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

  1. L66
    apply four_square_signed_natural_negative_first_blocks
  2. L67
    exact hzero
  3. L68
    exact horientation1
  4. L69
    exact horientation0
  5. L70
    exact horientation2
  6. L71
    exact horientation3
10Establish hcoordinatesL72–81

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

  1. L72
    have hcoordinates : exists m0 m1 m2 m3. ((((b * f) = (a * e + c * g + d * j) + m0) \/ ((a * e + c * g + d * j) = (b * f) + m0)) /\ ((((b * e + a * f + c * j) = (d * g) + m1) \/ ((d * g) = (b * e + a * f + c * j) + m1)) /\ ((((b * g + c * f + d * e) = (a * j) + m2) \/ ((a * j) = (b * g + c * f + d * e) + m2)) /\ (((b * j + a * g + d * f) = (c * e) + m3) \/ ((c * e) = (b * j + a * g + d * f) + m3)))))
  2. L73
    specialize quaternion_coordinate_absolute_total b
  3. L74
    specialize quaternion_coordinate_absolute_total a
  4. L75
    specialize quaternion_coordinate_absolute_total c
  5. L76
    specialize quaternion_coordinate_absolute_total d
  6. L77
    specialize quaternion_coordinate_absolute_total f
  7. L78
    specialize quaternion_coordinate_absolute_total e
  8. L79
    specialize quaternion_coordinate_absolute_total g
  9. L80
    specialize quaternion_coordinate_absolute_total j
  10. L81
    exact quaternion_coordinate_absolute_total
11Separate the logical casesL82–85

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

  1. L82
    cases hcoordinates
  2. L83
    cases hcoordinates_witness
  3. L84
    cases hcoordinates_witness_witness
  4. L85
    cases hcoordinates_witness_witness_witness
12Establish habsoluteL86–87

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

  1. L86
    have habsolute : ((((b * f) = (a * e + c * g + d * j) + x) \/ ((a * e + c * g + d * j) = (b * f) + x)) /\ ((((b * e + a * f + c * j) = (d * g) + x1) \/ ((d * g) = (b * e + a * f + c * j) + x1)) /\ ((((b * g + c * f + d * e) = (a * j) + x2) \/ ((a * j) = (b * g + c * f + d * e) + x2)) /\ (((b * j + a * g + d * f) = (c * e) + x3) \/ ((c * e) = (b * j + a * g + d * f) + x3)))))
  2. L87
    exact hcoordinates_witness_witness_witness_witness
13Establish hidentityL88–97

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

  1. L88
    have hidentity : (b * b + a * a + c * c + d * d) * (f * f + e * e + g * g + j * j) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  2. L89
    specialize four_square_euler_quaternion b
  3. L90
    specialize four_square_euler_quaternion a
  4. L91
    specialize four_square_euler_quaternion c
  5. L92
    specialize four_square_euler_quaternion d
  6. L93
    specialize four_square_euler_quaternion f
  7. L94
    specialize four_square_euler_quaternion e
  8. L95
    specialize four_square_euler_quaternion g
  9. L96
    specialize four_square_euler_quaternion j
  10. L97
    specialize four_square_euler_quaternion x
14Use earlier factsL98–102

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

  1. L98
    specialize four_square_euler_quaternion x1
  2. L99
    specialize four_square_euler_quaternion x2
  3. L100
    specialize four_square_euler_quaternion x3
  4. L101
    apply four_square_euler_quaternion
  5. L102
    exact habsolute
15Establish hcenter_identityL103–106

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

  1. L103
    have hcenter_identity : k * r = f * f + e * e + g * g + j * j
  2. L104
    trans f * f + e * e + g * g + j * j
  3. L105
    exact hcenter_permuted
  4. L106
    refl
16Establish hproductL107–112

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

  1. L107
    have hproduct : (p * k) * (k * r) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  2. L108
    trans (b * b + a * a + c * c + d * d) * (f * f + e * e + g * g + j * j)
  3. L109
    congr
  4. L110
    exact hfirst_permuted
  5. L111
    exact hcenter_identity
  6. L112
    exact hidentity
17Separate the logical casesL113–118

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

  1. L113
    cases hblocks
  2. L114
    cases hblocks_right
  3. L115
    cases hblocks_right_right
  4. L116
    cases habsolute
  5. L117
    cases habsolute_right
  6. L118
    cases habsolute_right_right
18Use earlier factsL119–128

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

  1. L119
    specialize four_square_signed_absolute_block_representation p
  2. L120
    specialize four_square_signed_absolute_block_representation k
  3. L121
    specialize four_square_signed_absolute_block_representation r
  4. L122
    specialize four_square_signed_absolute_block_representation (b * f)
  5. L123
    specialize four_square_signed_absolute_block_representation (b * e + a * f + c * j)
  6. L124
    specialize four_square_signed_absolute_block_representation (b * g + c * f + d * e)
  7. L125
    specialize four_square_signed_absolute_block_representation (b * j + a * g + d * f)
  8. L126
    specialize four_square_signed_absolute_block_representation (a * e + c * g + d * j)
  9. L127
    specialize four_square_signed_absolute_block_representation (d * g)
  10. L128
    specialize four_square_signed_absolute_block_representation (a * j)
19Use earlier factsL129–138

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

  1. L129
    specialize four_square_signed_absolute_block_representation (c * e)
  2. L130
    specialize four_square_signed_absolute_block_representation x
  3. L131
    specialize four_square_signed_absolute_block_representation x1
  4. L132
    specialize four_square_signed_absolute_block_representation x2
  5. L133
    specialize four_square_signed_absolute_block_representation x3
  6. L134
    apply four_square_signed_absolute_block_representation
  7. L135
    exact hnonzero
  8. L136
    exact hproduct
  9. L137
    exact hblocks_left
  10. L138
    exact habsolute_left
20Use earlier factsL139–144

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

  1. L139
    exact hblocks_right_left
  2. L140
    exact habsolute_right_left
  3. L141
    exact hblocks_right_right_left
  4. L142
    exact habsolute_right_right_left
  5. L143
    exact hblocks_right_right_right
  6. L144
    exact habsolute_right_right_right

Library-wide reading audit

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