FS0051 · theorem body

four_square_signed_orientation_mask_11

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

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

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,0) → ModEq(k,c,g) → ModEq(k,d + j,0) → 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_11_0 ftcn_right_mask_11_0. (a + e) + (k) * ftcn_left_mask_11_0 = (0) + (k) * ftcn_right_mask_11_0) -> (exists ftcn_left_mask_11_1 ftcn_right_mask_11_1. (b + f) + (k) * ftcn_left_mask_11_1 = (0) + (k) * ftcn_right_mask_11_1) -> (exists ftcn_left_mask_11_2 ftcn_right_mask_11_2. (c) + (k) * ftcn_left_mask_11_2 = (g) + (k) * ftcn_right_mask_11_2) -> (exists ftcn_left_mask_11_3 ftcn_right_mask_11_3. (d + j) + (k) * ftcn_left_mask_11_3 = (0) + (k) * ftcn_right_mask_11_3) -> k * r = e * e + f * f + g * g + j * j -> (exists fsl_a_fssc_mask_11 fsl_b_fssc_mask_11 fsl_c_fssc_mask_11 fsl_d_fssc_mask_11. (p * r) = fsl_a_fssc_mask_11 * fsl_a_fssc_mask_11 + fsl_b_fssc_mask_11 * fsl_b_fssc_mask_11 + fsl_c_fssc_mask_11 * fsl_c_fssc_mask_11 + fsl_d_fssc_mask_11 * fsl_d_fssc_mask_11)

Proof neighborhood

Direct theorem prerequisites

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

152 script commands · 22 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 positive 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.

  1. L21
    have hfirst_permuted : p * k = c * c + a * a + 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 ((c * c) + ((a * a) + ((b * b) + (d * d))))
  7. L27
    trans ((c * c) + ((a * a) + ((b * b) + (d * d))))
  8. L28
    trans ((a * a) + ((c * c) + ((b * b) + (d * d))))
  9. L29
    congr
  10. L30
    refl
04Use earlier factsL31–32

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

  1. L31
    apply four_square_add_swap_right_tail
  2. L32
    apply four_square_add_swap_right_tail
05Calculate and transport equalitiesL33–37

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

  1. L33
    congr
  2. L34
    refl
  3. L35
    refl
  4. L36
    symm
  5. L37
    simp [add_assoc]
06Establish hcenter_permutedL38–47

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

  1. L38
    have hcenter_permuted : k * r = g * g + e * e + f * f + j * j
  2. L39
    trans e * e + f * f + g * g + j * j
  3. L40
    exact hcenter
  4. L41
    trans ((e * e) + ((f * f) + ((g * g) + (j * j))))
  5. L42
    simp [add_assoc]
  6. L43
    trans ((g * g) + ((e * e) + ((f * f) + (j * j))))
  7. L44
    trans ((g * g) + ((e * e) + ((f * f) + (j * j))))
  8. L45
    trans ((e * e) + ((g * g) + ((f * f) + (j * j))))
  9. L46
    congr
  10. L47
    refl
07Use earlier factsL48–49

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

  1. L48
    apply four_square_add_swap_right_tail
  2. L49
    apply four_square_add_swap_right_tail
08Calculate and transport equalitiesL50–54

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

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

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed cases norm quotient zero congruence.

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

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

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

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

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

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

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

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

  1. L90
    cases hcoordinates
  2. L91
    cases hcoordinates_witness
  3. L92
    cases hcoordinates_witness_witness
  4. L93
    cases hcoordinates_witness_witness_witness
14Establish habsoluteL94–95

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

  1. L94
    have habsolute : ((((c * g) = (a * e + b * f + d * j) + x) \/ ((a * e + b * f + d * j) = (c * g) + x)) /\ ((((c * e + a * g + b * j) = (d * f) + x1) \/ ((d * f) = (c * e + a * g + b * j) + x1)) /\ ((((c * f + b * g + d * e) = (a * j) + x2) \/ ((a * j) = (c * f + b * g + d * e) + x2)) /\ (((c * j + a * f + d * g) = (b * e) + x3) \/ ((b * e) = (c * j + a * f + d * g) + x3)))))
  2. L95
    exact hcoordinates_witness_witness_witness_witness
15Establish hidentityL96–105

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

  1. L96
    have hidentity : (c * c + a * a + b * b + d * d) * (g * g + e * e + f * f + j * j) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  2. L97
    specialize four_square_euler_quaternion c
  3. L98
    specialize four_square_euler_quaternion a
  4. L99
    specialize four_square_euler_quaternion b
  5. L100
    specialize four_square_euler_quaternion d
  6. L101
    specialize four_square_euler_quaternion g
  7. L102
    specialize four_square_euler_quaternion e
  8. L103
    specialize four_square_euler_quaternion f
  9. L104
    specialize four_square_euler_quaternion j
  10. L105
    specialize four_square_euler_quaternion x
16Use earlier factsL106–110

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

  1. L106
    specialize four_square_euler_quaternion x1
  2. L107
    specialize four_square_euler_quaternion x2
  3. L108
    specialize four_square_euler_quaternion x3
  4. L109
    apply four_square_euler_quaternion
  5. L110
    exact habsolute
17Establish hcenter_identityL111–114

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

  1. L111
    have hcenter_identity : k * r = g * g + e * e + f * f + j * j
  2. L112
    trans g * g + e * e + f * f + j * j
  3. L113
    exact hcenter_permuted
  4. L114
    refl
18Establish hproductL115–120

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

  1. L115
    have hproduct : (p * k) * (k * r) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  2. L116
    trans (c * c + a * a + b * b + d * d) * (g * g + e * e + f * f + j * j)
  3. L117
    congr
  4. L118
    exact hfirst_permuted
  5. L119
    exact hcenter_identity
  6. L120
    exact hidentity
19Separate the logical casesL121–126

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

  1. L121
    cases hblocks
  2. L122
    cases hblocks_right
  3. L123
    cases hblocks_right_right
  4. L124
    cases habsolute
  5. L125
    cases habsolute_right
  6. L126
    cases habsolute_right_right
20Use earlier factsL127–136

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

  1. L127
    specialize four_square_signed_absolute_block_representation p
  2. L128
    specialize four_square_signed_absolute_block_representation k
  3. L129
    specialize four_square_signed_absolute_block_representation r
  4. L130
    specialize four_square_signed_absolute_block_representation (c * g)
  5. L131
    specialize four_square_signed_absolute_block_representation (c * e + a * g + b * j)
  6. L132
    specialize four_square_signed_absolute_block_representation (c * f + b * g + d * e)
  7. L133
    specialize four_square_signed_absolute_block_representation (c * j + a * f + d * g)
  8. L134
    specialize four_square_signed_absolute_block_representation (a * e + b * f + d * j)
  9. L135
    specialize four_square_signed_absolute_block_representation (d * f)
  10. L136
    specialize four_square_signed_absolute_block_representation (a * j)
21Use earlier factsL137–146

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

  1. L137
    specialize four_square_signed_absolute_block_representation (b * e)
  2. L138
    specialize four_square_signed_absolute_block_representation x
  3. L139
    specialize four_square_signed_absolute_block_representation x1
  4. L140
    specialize four_square_signed_absolute_block_representation x2
  5. L141
    specialize four_square_signed_absolute_block_representation x3
  6. L142
    apply four_square_signed_absolute_block_representation
  7. L143
    exact hnonzero
  8. L144
    exact hproduct
  9. L145
    exact hblocks_left
  10. L146
    exact habsolute_left
22Use earlier factsL147–152

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

  1. L147
    exact hblocks_right_left
  2. L148
    exact habsolute_right_left
  3. L149
    exact hblocks_right_right_left
  4. L150
    exact habsolute_right_right_left
  5. L151
    exact hblocks_right_right_right
  6. L152
    exact habsolute_right_right_right

Library-wide reading audit

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