FS004T · theorem body

four_square_signed_orientation_mask_03

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

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

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

Statement with defined notation

∀ p. ∀ k. ∀ h. ∀ a. ∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ j. ∀ r. ¬k = 0 → k = 2 · h + 1 → p · k = a · a + b · b + c · c + d · d → ModEq(k,a + e,0) → ModEq(k,b + f,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_3_0 ftcn_right_mask_3_0. (a + e) + (k) * ftcn_left_mask_3_0 = (0) + (k) * ftcn_right_mask_3_0) -> (exists ftcn_left_mask_3_1 ftcn_right_mask_3_1. (b + f) + (k) * ftcn_left_mask_3_1 = (0) + (k) * ftcn_right_mask_3_1) -> (exists ftcn_left_mask_3_2 ftcn_right_mask_3_2. (c) + (k) * ftcn_left_mask_3_2 = (g) + (k) * ftcn_right_mask_3_2) -> (exists ftcn_left_mask_3_3 ftcn_right_mask_3_3. (d) + (k) * ftcn_left_mask_3_3 = (j) + (k) * ftcn_right_mask_3_3) -> k * r = e * e + f * f + g * g + j * j -> (exists fsl_a_fssc_mask_3 fsl_b_fssc_mask_3 fsl_c_fssc_mask_3 fsl_d_fssc_mask_3. (p * r) = fsl_a_fssc_mask_3 * fsl_a_fssc_mask_3 + fsl_b_fssc_mask_3 * fsl_b_fssc_mask_3 + fsl_c_fssc_mask_3 * fsl_c_fssc_mask_3 + fsl_d_fssc_mask_3 * fsl_d_fssc_mask_3)

Proof neighborhood

Direct theorem prerequisites

FS004P four_square_signed_cases_norm_quotient_zero_congruence FS005Z four_square_signed_conjugate_mixed_blocks FS0057 four_square_signed_absolute_block_representation add_assoc · Stable closed add_comm · Stable closed FS0006 four_square_add_swap_right_tail FS0013 four_square_conjugate_absolute_coordinates_total

Direct theorem dependents

FS0058 four_square_signed_centered_representation

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

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

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (5)
four square signed cases norm quotient zero congruencefour square signed conjugate mixed blocksfour square signed absolute block representationfour square add swap right tailfour square conjugate absolute coordinates total
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro k
  3. L3
    intro h
  4. L4
    intro a
  5. L5
    intro b
  6. L6
    intro c
  7. L7
    intro d
  8. L8
    intro e
  9. L9
    intro f
  10. L10
    intro g
02Fix variables and assumptionsL11–20

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro j
  2. L12
    intro r
  3. L13
    intro hnonzero
  4. L14
    intro hodd
  5. L15
    intro hfirst
  6. L16
    intro horientation0
  7. L17
    intro horientation1
  8. L18
    intro horientation2
  9. L19
    intro horientation3
  10. L20
    intro hcenter
03Establish hfirst_permutedL21–24

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

  1. L21
    have hfirst_permuted : p * k = a * a + b * b + c * c + d * d
  2. L22
    trans a * a + b * b + c * c + d * d
  3. L23
    exact hfirst
  4. L24
    refl
04Establish hcenter_permutedL25–28

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

  1. L25
    have hcenter_permuted : k * r = e * e + f * f + g * g + j * j
  2. L26
    trans e * e + f * f + g * g + j * j
  3. L27
    exact hcenter
  4. L28
    refl
05Establish hzeroL29–37

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. L29
    have hzero : ModEq(k,e · e + f · f + g · g + j · j,0)Definitions: ModEq(k,e · e + f · f + g · g + j · j,0)Original native command in the exact edition
  2. L30
    specialize four_square_signed_cases_norm_quotient_zero_congruence k
  3. L31
    specialize four_square_signed_cases_norm_quotient_zero_congruence r
  4. L32
    specialize four_square_signed_cases_norm_quotient_zero_congruence e
  5. L33
    specialize four_square_signed_cases_norm_quotient_zero_congruence f
  6. L34
    specialize four_square_signed_cases_norm_quotient_zero_congruence g
  7. L35
    specialize four_square_signed_cases_norm_quotient_zero_congruence j
  8. L36
    apply four_square_signed_cases_norm_quotient_zero_congruence
  9. L37
    exact hcenter_permuted
06Establish hblocksL38–47

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

  1. L38
    have hblocks : ModEq(k,a · j + b · g + c · f + d · e,0) ∧ (ModEq(k,a · g + c · e,b · j + d · f) ∧ (ModEq(k,a · f + d · g,c · j + b · e) ∧ ModEq(k,a · e + b · f,d · j + c · g)))Definitions: ModEq(k,a · j + b · g + c · f + d · e,0)ModEq(k,a · g + c · e,b · j + d · f)ModEq(k,a · f + d · g,c · j + b · e)ModEq(k,a · e + b · f,d · j + c · g)Original native command in the exact edition
  2. L39
    specialize four_square_signed_conjugate_mixed_blocks k
  3. L40
    specialize four_square_signed_conjugate_mixed_blocks a
  4. L41
    specialize four_square_signed_conjugate_mixed_blocks b
  5. L42
    specialize four_square_signed_conjugate_mixed_blocks c
  6. L43
    specialize four_square_signed_conjugate_mixed_blocks d
  7. L44
    specialize four_square_signed_conjugate_mixed_blocks e
  8. L45
    specialize four_square_signed_conjugate_mixed_blocks f
  9. L46
    specialize four_square_signed_conjugate_mixed_blocks g
  10. L47
    specialize four_square_signed_conjugate_mixed_blocks j
07Use earlier factsL48–53

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

  1. L48
    apply four_square_signed_conjugate_mixed_blocks
  2. L49
    exact hzero
  3. L50
    exact horientation0
  4. L51
    exact horientation1
  5. L52
    exact horientation2
  6. L53
    exact horientation3
08Establish hcoordinatesL54–63

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

  1. L54
    have hcoordinates : exists m0 m1 m2 m3. (((((a * j + b * g + c * f + d * e) = (0) + m0) \/ ((0) = (a * j + b * g + c * f + d * e) + m0)) /\ ((((a * g + c * e) = (b * j + d * f) + m1) \/ ((b * j + d * f) = (a * g + c * e) + m1)) /\ ((((a * f + d * g) = (c * j + b * e) + m2) \/ ((c * j + b * e) = (a * f + d * g) + m2)) /\ (((a * e + b * f) = (d * j + c * g) + m3) \/ ((d * j + c * g) = (a * e + b * f) + m3))))) /\ ((a * a + b * b + c * c + d * d) * (j * j + g * g + f * f + e * e) = m0 * m0 + m1 * m1 + m2 * m2 + m3 * m3))
  2. L55
    specialize four_square_conjugate_absolute_coordinates_total a
  3. L56
    specialize four_square_conjugate_absolute_coordinates_total b
  4. L57
    specialize four_square_conjugate_absolute_coordinates_total c
  5. L58
    specialize four_square_conjugate_absolute_coordinates_total d
  6. L59
    specialize four_square_conjugate_absolute_coordinates_total j
  7. L60
    specialize four_square_conjugate_absolute_coordinates_total g
  8. L61
    specialize four_square_conjugate_absolute_coordinates_total f
  9. L62
    specialize four_square_conjugate_absolute_coordinates_total e
  10. L63
    exact four_square_conjugate_absolute_coordinates_total
09Separate the logical casesL64–68

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

  1. L64
    cases hcoordinates
  2. L65
    cases hcoordinates_witness
  3. L66
    cases hcoordinates_witness_witness
  4. L67
    cases hcoordinates_witness_witness_witness
  5. L68
    cases hcoordinates_witness_witness_witness_witness
10Establish habsoluteL69–70

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

  1. L69
    have habsolute : ((((a * j + b * g + c * f + d * e) = (0) + x) \/ ((0) = (a * j + b * g + c * f + d * e) + x)) /\ ((((a * g + c * e) = (b * j + d * f) + x1) \/ ((b * j + d * f) = (a * g + c * e) + x1)) /\ ((((a * f + d * g) = (c * j + b * e) + x2) \/ ((c * j + b * e) = (a * f + d * g) + x2)) /\ (((a * e + b * f) = (d * j + c * g) + x3) \/ ((d * j + c * g) = (a * e + b * f) + x3)))))
  2. L70
    exact hcoordinates_witness_witness_witness_witness_left
11Establish hidentityL71–72

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

  1. L71
    have hidentity : (a * a + b * b + c * c + d * d) * (j * j + g * g + f * f + e * e) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  2. L72
    exact hcoordinates_witness_witness_witness_witness_right
12Establish hcenter_identityL73–82

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

  1. L73
    have hcenter_identity : k * r = j * j + g * g + f * f + e * e
  2. L74
    trans e * e + f * f + g * g + j * j
  3. L75
    exact hcenter_permuted
  4. L76
    trans ((e * e) + ((f * f) + ((g * g) + (j * j))))
  5. L77
    simp [add_assoc]
  6. L78
    trans ((j * j) + ((g * g) + ((f * f) + (e * e))))
  7. L79
    trans ((j * j) + ((e * e) + ((f * f) + (g * g))))
  8. L80
    trans ((e * e) + ((j * j) + ((f * f) + (g * g))))
  9. L81
    congr
  10. L82
    refl
13Calculate and transport equalitiesL83–85

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

  1. L83
    trans ((f * f) + ((j * j) + (g * g)))
  2. L84
    congr
  3. L85
    refl
14Use earlier factsL86–88

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

  1. L86
    apply add_comm
  2. L87
    apply four_square_add_swap_right_tail
  3. L88
    apply four_square_add_swap_right_tail
15Calculate and transport equalitiesL89–94

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

  1. L89
    congr
  2. L90
    refl
  3. L91
    trans ((g * g) + ((e * e) + (f * f)))
  4. L92
    trans ((e * e) + ((g * g) + (f * f)))
  5. L93
    congr
  6. L94
    refl
16Use earlier factsL95–96

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

  1. L95
    apply add_comm
  2. L96
    apply four_square_add_swap_right_tail
17Calculate and transport equalitiesL97–99

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

  1. L97
    congr
  2. L98
    refl
  3. L99
    trans ((f * f) + (e * e))
18Use earlier factsL100–100

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

  1. L100
    apply add_comm
19Calculate and transport equalitiesL101–105

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

  1. L101
    congr
  2. L102
    refl
  3. L103
    refl
  4. L104
    symm
  5. L105
    simp [add_assoc]
20Establish hproductL106–111

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

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

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

  1. L112
    cases hblocks
  2. L113
    cases hblocks_right
  3. L114
    cases hblocks_right_right
  4. L115
    cases habsolute
  5. L116
    cases habsolute_right
  6. L117
    cases habsolute_right_right
22Use earlier factsL118–127

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

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

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

  1. L128
    specialize four_square_signed_absolute_block_representation (d * j + c * g)
  2. L129
    specialize four_square_signed_absolute_block_representation x
  3. L130
    specialize four_square_signed_absolute_block_representation x1
  4. L131
    specialize four_square_signed_absolute_block_representation x2
  5. L132
    specialize four_square_signed_absolute_block_representation x3
  6. L133
    apply four_square_signed_absolute_block_representation
  7. L134
    exact hnonzero
  8. L135
    exact hproduct
  9. L136
    exact hblocks_left
  10. L137
    exact habsolute_left
24Use earlier factsL138–143

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

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

Library-wide reading audit

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