FS004X

four_square_signed_orientation_mask_07

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

Constructive signed quaternion quotient for centered orientation mask 0111, using the exact four_square_signed_natural_positive_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.

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_7_0 ftcn_right_mask_7_0. (a + e) + (k) * ftcn_left_mask_7_0 = (0) + (k) * ftcn_right_mask_7_0) -> (exists ftcn_left_mask_7_1 ftcn_right_mask_7_1. (b + f) + (k) * ftcn_left_mask_7_1 = (0) + (k) * ftcn_right_mask_7_1) -> (exists ftcn_left_mask_7_2 ftcn_right_mask_7_2. (c + g) + (k) * ftcn_left_mask_7_2 = (0) + (k) * ftcn_right_mask_7_2) -> (exists ftcn_left_mask_7_3 ftcn_right_mask_7_3. (d) + (k) * ftcn_left_mask_7_3 = (j) + (k) * ftcn_right_mask_7_3) -> k * r = e * e + f * f + g * g + j * j -> (exists fsl_a_fssc_mask_7 fsl_b_fssc_mask_7 fsl_c_fssc_mask_7 fsl_d_fssc_mask_7. (p * r) = fsl_a_fssc_mask_7 * fsl_a_fssc_mask_7 + fsl_b_fssc_mask_7 * fsl_b_fssc_mask_7 + fsl_c_fssc_mask_7 * fsl_c_fssc_mask_7 + fsl_d_fssc_mask_7 * fsl_d_fssc_mask_7)

Constructive proof overview

Generated structural guide

Constructive signed quaternion quotient for centered orientation mask 0111, using the exact four_square_signed_natural_positive_first_blocks surface.

The unchanged tactic script uses 8 declared prerequisites and contains 160 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 FS004O four_square_signed_natural_positive_first_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 FS0005 quaternion_coordinate_absolute_total FS002Y four_square_euler_quaternion

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

160 script commands · 24 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 (6)
four square signed cases norm quotient zero congruencefour square signed natural positive first blocksfour square signed absolute block representationfour square add swap right tailquaternion coordinate absolute totalfour square euler quaternion

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 = d * d + a * a + 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 ((d * d) + ((a * a) + ((b * b) + (c * c))))
  7. L27
    trans ((d * d) + ((a * a) + ((b * b) + (c * c))))
  8. L28
    trans ((a * a) + ((d * d) + ((b * b) + (c * c))))
  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
    trans ((b * b) + ((d * d) + (c * c)))
  2. L32
    congr
  3. L33
    refl
05Use earlier factsL34–36

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

  1. L34
    apply add_comm
  2. L35
    apply four_square_add_swap_right_tail
  3. L36
    apply four_square_add_swap_right_tail
06Calculate and transport equalitiesL37–41

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

  1. L37
    congr
  2. L38
    refl
  3. L39
    refl
  4. L40
    symm
  5. L41
    simp [add_assoc]
07Establish hcenter_permutedL42–51

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

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

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

  1. L52
    trans ((f * f) + ((j * j) + (g * g)))
  2. L53
    congr
  3. L54
    refl
09Use earlier factsL55–57

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

  1. L55
    apply add_comm
  2. L56
    apply four_square_add_swap_right_tail
  3. L57
    apply four_square_add_swap_right_tail
10Calculate and transport equalitiesL58–62

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

  1. L58
    congr
  2. L59
    refl
  3. L60
    refl
  4. L61
    symm
  5. L62
    simp [add_assoc]
11Establish hzeroL63–71

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. L63
    have hzero : (exists ftcn_left_case_7_zero ftcn_right_case_7_zero. (j * j + e * e + f * f + g * g) + (k) * ftcn_left_case_7_zero = (0) + (k) * ftcn_right_case_7_zero)
  2. L64
    specialize four_square_signed_cases_norm_quotient_zero_congruence k
  3. L65
    specialize four_square_signed_cases_norm_quotient_zero_congruence r
  4. L66
    specialize four_square_signed_cases_norm_quotient_zero_congruence j
  5. L67
    specialize four_square_signed_cases_norm_quotient_zero_congruence e
  6. L68
    specialize four_square_signed_cases_norm_quotient_zero_congruence f
  7. L69
    specialize four_square_signed_cases_norm_quotient_zero_congruence g
  8. L70
    apply four_square_signed_cases_norm_quotient_zero_congruence
  9. L71
    exact hcenter_permuted
12Establish hblocksL72–81

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

  1. L72
    have hblocks : ModEq(k,d · j,a · e + b · f + c · g) ∧ (ModEq(k,d · e + a · j + b · g,c · f) ∧ (ModEq(k,d · f + b · j + c · e,a · g) ∧ ModEq(k,d · g + a · f + c · j,b · e)))Definitions: ModEq
  2. L73
    specialize four_square_signed_natural_positive_first_blocks k
  3. L74
    specialize four_square_signed_natural_positive_first_blocks d
  4. L75
    specialize four_square_signed_natural_positive_first_blocks a
  5. L76
    specialize four_square_signed_natural_positive_first_blocks b
  6. L77
    specialize four_square_signed_natural_positive_first_blocks c
  7. L78
    specialize four_square_signed_natural_positive_first_blocks j
  8. L79
    specialize four_square_signed_natural_positive_first_blocks e
  9. L80
    specialize four_square_signed_natural_positive_first_blocks f
  10. L81
    specialize four_square_signed_natural_positive_first_blocks g
13Use earlier factsL82–87

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

  1. L82
    apply four_square_signed_natural_positive_first_blocks
  2. L83
    exact hzero
  3. L84
    exact horientation3
  4. L85
    exact horientation0
  5. L86
    exact horientation1
  6. L87
    exact horientation2
14Establish hcoordinatesL88–97

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

  1. L88
    have hcoordinates : exists m0 m1 m2 m3. ((((d * j) = (a * e + b * f + c * g) + m0) \/ ((a * e + b * f + c * g) = (d * j) + m0)) /\ ((((d * e + a * j + b * g) = (c * f) + m1) \/ ((c * f) = (d * e + a * j + b * g) + m1)) /\ ((((d * f + b * j + c * e) = (a * g) + m2) \/ ((a * g) = (d * f + b * j + c * e) + m2)) /\ (((d * g + a * f + c * j) = (b * e) + m3) \/ ((b * e) = (d * g + a * f + c * j) + m3)))))
  2. L89
    specialize quaternion_coordinate_absolute_total d
  3. L90
    specialize quaternion_coordinate_absolute_total a
  4. L91
    specialize quaternion_coordinate_absolute_total b
  5. L92
    specialize quaternion_coordinate_absolute_total c
  6. L93
    specialize quaternion_coordinate_absolute_total j
  7. L94
    specialize quaternion_coordinate_absolute_total e
  8. L95
    specialize quaternion_coordinate_absolute_total f
  9. L96
    specialize quaternion_coordinate_absolute_total g
  10. L97
    exact quaternion_coordinate_absolute_total
15Separate the logical casesL98–101

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

  1. L98
    cases hcoordinates
  2. L99
    cases hcoordinates_witness
  3. L100
    cases hcoordinates_witness_witness
  4. L101
    cases hcoordinates_witness_witness_witness
16Establish habsoluteL102–103

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

  1. L102
    have habsolute : ((((d * j) = (a * e + b * f + c * g) + x) \/ ((a * e + b * f + c * g) = (d * j) + x)) /\ ((((d * e + a * j + b * g) = (c * f) + x1) \/ ((c * f) = (d * e + a * j + b * g) + x1)) /\ ((((d * f + b * j + c * e) = (a * g) + x2) \/ ((a * g) = (d * f + b * j + c * e) + x2)) /\ (((d * g + a * f + c * j) = (b * e) + x3) \/ ((b * e) = (d * g + a * f + c * j) + x3)))))
  2. L103
    exact hcoordinates_witness_witness_witness_witness
17Establish hidentityL104–113

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

  1. L104
    have hidentity : (d * d + a * a + b * b + c * c) * (j * j + e * e + f * f + g * g) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  2. L105
    specialize four_square_euler_quaternion d
  3. L106
    specialize four_square_euler_quaternion a
  4. L107
    specialize four_square_euler_quaternion b
  5. L108
    specialize four_square_euler_quaternion c
  6. L109
    specialize four_square_euler_quaternion j
  7. L110
    specialize four_square_euler_quaternion e
  8. L111
    specialize four_square_euler_quaternion f
  9. L112
    specialize four_square_euler_quaternion g
  10. L113
    specialize four_square_euler_quaternion x
18Use earlier factsL114–118

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

  1. L114
    specialize four_square_euler_quaternion x1
  2. L115
    specialize four_square_euler_quaternion x2
  3. L116
    specialize four_square_euler_quaternion x3
  4. L117
    apply four_square_euler_quaternion
  5. L118
    exact habsolute
19Establish hcenter_identityL119–122

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

  1. L119
    have hcenter_identity : k * r = j * j + e * e + f * f + g * g
  2. L120
    trans j * j + e * e + f * f + g * g
  3. L121
    exact hcenter_permuted
  4. L122
    refl
20Establish hproductL123–128

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

  1. L123
    have hproduct : (p * k) * (k * r) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  2. L124
    trans (d * d + a * a + b * b + c * c) * (j * j + e * e + f * f + g * g)
  3. L125
    congr
  4. L126
    exact hfirst_permuted
  5. L127
    exact hcenter_identity
  6. L128
    exact hidentity
21Separate the logical casesL129–134

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

  1. L129
    cases hblocks
  2. L130
    cases hblocks_right
  3. L131
    cases hblocks_right_right
  4. L132
    cases habsolute
  5. L133
    cases habsolute_right
  6. L134
    cases habsolute_right_right
22Use earlier factsL135–144

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

  1. L135
    specialize four_square_signed_absolute_block_representation p
  2. L136
    specialize four_square_signed_absolute_block_representation k
  3. L137
    specialize four_square_signed_absolute_block_representation r
  4. L138
    specialize four_square_signed_absolute_block_representation (d * j)
  5. L139
    specialize four_square_signed_absolute_block_representation (d * e + a * j + b * g)
  6. L140
    specialize four_square_signed_absolute_block_representation (d * f + b * j + c * e)
  7. L141
    specialize four_square_signed_absolute_block_representation (d * g + a * f + c * j)
  8. L142
    specialize four_square_signed_absolute_block_representation (a * e + b * f + c * g)
  9. L143
    specialize four_square_signed_absolute_block_representation (c * f)
  10. L144
    specialize four_square_signed_absolute_block_representation (a * g)
23Use earlier factsL145–154

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

  1. L145
    specialize four_square_signed_absolute_block_representation (b * e)
  2. L146
    specialize four_square_signed_absolute_block_representation x
  3. L147
    specialize four_square_signed_absolute_block_representation x1
  4. L148
    specialize four_square_signed_absolute_block_representation x2
  5. L149
    specialize four_square_signed_absolute_block_representation x3
  6. L150
    apply four_square_signed_absolute_block_representation
  7. L151
    exact hnonzero
  8. L152
    exact hproduct
  9. L153
    exact hblocks_left
  10. L154
    exact habsolute_left
24Use earlier factsL155–160

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

  1. L155
    exact hblocks_right_left
  2. L156
    exact habsolute_right_left
  3. L157
    exact hblocks_right_right_left
  4. L158
    exact habsolute_right_right_left
  5. L159
    exact hblocks_right_right_right
  6. L160
    exact habsolute_right_right_right

Library-wide reading audit

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