FS004R · theorem body

four_square_signed_orientation_mask_01

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

Constructive signed quaternion quotient for centered orientation mask 0001, 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,0) → ModEq(k,b,f) → 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_1_0 ftcn_right_mask_1_0. (a + e) + (k) * ftcn_left_mask_1_0 = (0) + (k) * ftcn_right_mask_1_0) -> (exists ftcn_left_mask_1_1 ftcn_right_mask_1_1. (b) + (k) * ftcn_left_mask_1_1 = (f) + (k) * ftcn_right_mask_1_1) -> (exists ftcn_left_mask_1_2 ftcn_right_mask_1_2. (c) + (k) * ftcn_left_mask_1_2 = (g) + (k) * ftcn_right_mask_1_2) -> (exists ftcn_left_mask_1_3 ftcn_right_mask_1_3. (d) + (k) * ftcn_left_mask_1_3 = (j) + (k) * ftcn_right_mask_1_3) -> k * r = e * e + f * f + g * g + j * j -> (exists fsl_a_fssc_mask_1 fsl_b_fssc_mask_1 fsl_c_fssc_mask_1 fsl_d_fssc_mask_1. (p * r) = fsl_a_fssc_mask_1 * fsl_a_fssc_mask_1 + fsl_b_fssc_mask_1 * fsl_b_fssc_mask_1 + fsl_c_fssc_mask_1 * fsl_c_fssc_mask_1 + fsl_d_fssc_mask_1 * fsl_d_fssc_mask_1)

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

126 script commands · 18 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 natural negative first blocksfour square signed absolute block representationquaternion 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–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 · e,b · f + c · g + d · j) ∧ (ModEq(k,a · f + b · e + c · j,d · g) ∧ (ModEq(k,a · g + c · e + d · f,b · j) ∧ ModEq(k,a · j + b · g + d · e,c · f)))Definitions: ModEq(k,a · e,b · f + c · g + d · j)ModEq(k,a · f + b · e + c · j,d · g)ModEq(k,a · g + c · e + d · f,b · j)ModEq(k,a · j + b · g + d · e,c · f)Original native command in the exact edition
  2. L39
    specialize four_square_signed_natural_negative_first_blocks k
  3. L40
    specialize four_square_signed_natural_negative_first_blocks a
  4. L41
    specialize four_square_signed_natural_negative_first_blocks b
  5. L42
    specialize four_square_signed_natural_negative_first_blocks c
  6. L43
    specialize four_square_signed_natural_negative_first_blocks d
  7. L44
    specialize four_square_signed_natural_negative_first_blocks e
  8. L45
    specialize four_square_signed_natural_negative_first_blocks f
  9. L46
    specialize four_square_signed_natural_negative_first_blocks g
  10. L47
    specialize four_square_signed_natural_negative_first_blocks j
07Use earlier factsL48–53

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

  1. L48
    apply four_square_signed_natural_negative_first_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 * e) = (b * f + c * g + d * j) + m0) \/ ((b * f + c * g + d * j) = (a * e) + m0)) /\ ((((a * f + b * e + c * j) = (d * g) + m1) \/ ((d * g) = (a * f + b * e + c * j) + m1)) /\ ((((a * g + c * e + d * f) = (b * j) + m2) \/ ((b * j) = (a * g + c * e + d * f) + m2)) /\ (((a * j + b * g + d * e) = (c * f) + m3) \/ ((c * f) = (a * j + b * g + d * e) + m3)))))
  2. L55
    specialize quaternion_coordinate_absolute_total a
  3. L56
    specialize quaternion_coordinate_absolute_total b
  4. L57
    specialize quaternion_coordinate_absolute_total c
  5. L58
    specialize quaternion_coordinate_absolute_total d
  6. L59
    specialize quaternion_coordinate_absolute_total e
  7. L60
    specialize quaternion_coordinate_absolute_total f
  8. L61
    specialize quaternion_coordinate_absolute_total g
  9. L62
    specialize quaternion_coordinate_absolute_total j
  10. L63
    exact quaternion_coordinate_absolute_total
09Separate the logical casesL64–67

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
10Establish habsoluteL68–69

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

  1. L68
    have habsolute : ((((a * e) = (b * f + c * g + d * j) + x) \/ ((b * f + c * g + d * j) = (a * e) + x)) /\ ((((a * f + b * e + c * j) = (d * g) + x1) \/ ((d * g) = (a * f + b * e + c * j) + x1)) /\ ((((a * g + c * e + d * f) = (b * j) + x2) \/ ((b * j) = (a * g + c * e + d * f) + x2)) /\ (((a * j + b * g + d * e) = (c * f) + x3) \/ ((c * f) = (a * j + b * g + d * e) + x3)))))
  2. L69
    exact hcoordinates_witness_witness_witness_witness
11Establish hidentityL70–79

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

  1. L70
    have hidentity : (a * a + b * b + c * c + d * d) * (e * e + f * f + g * g + j * j) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  2. L71
    specialize four_square_euler_quaternion a
  3. L72
    specialize four_square_euler_quaternion b
  4. L73
    specialize four_square_euler_quaternion c
  5. L74
    specialize four_square_euler_quaternion d
  6. L75
    specialize four_square_euler_quaternion e
  7. L76
    specialize four_square_euler_quaternion f
  8. L77
    specialize four_square_euler_quaternion g
  9. L78
    specialize four_square_euler_quaternion j
  10. L79
    specialize four_square_euler_quaternion x
12Use earlier factsL80–84

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

  1. L80
    specialize four_square_euler_quaternion x1
  2. L81
    specialize four_square_euler_quaternion x2
  3. L82
    specialize four_square_euler_quaternion x3
  4. L83
    apply four_square_euler_quaternion
  5. L84
    exact habsolute
13Establish hcenter_identityL85–88

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

  1. L85
    have hcenter_identity : k * r = e * e + f * f + g * g + j * j
  2. L86
    trans e * e + f * f + g * g + j * j
  3. L87
    exact hcenter_permuted
  4. L88
    refl
14Establish hproductL89–94

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

  1. L89
    have hproduct : (p * k) * (k * r) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  2. L90
    trans (a * a + b * b + c * c + d * d) * (e * e + f * f + g * g + j * j)
  3. L91
    congr
  4. L92
    exact hfirst_permuted
  5. L93
    exact hcenter_identity
  6. L94
    exact hidentity
15Separate the logical casesL95–100

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

  1. L95
    cases hblocks
  2. L96
    cases hblocks_right
  3. L97
    cases hblocks_right_right
  4. L98
    cases habsolute
  5. L99
    cases habsolute_right
  6. L100
    cases habsolute_right_right
16Use earlier factsL101–110

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

  1. L101
    specialize four_square_signed_absolute_block_representation p
  2. L102
    specialize four_square_signed_absolute_block_representation k
  3. L103
    specialize four_square_signed_absolute_block_representation r
  4. L104
    specialize four_square_signed_absolute_block_representation (a * e)
  5. L105
    specialize four_square_signed_absolute_block_representation (a * f + b * e + c * j)
  6. L106
    specialize four_square_signed_absolute_block_representation (a * g + c * e + d * f)
  7. L107
    specialize four_square_signed_absolute_block_representation (a * j + b * g + d * e)
  8. L108
    specialize four_square_signed_absolute_block_representation (b * f + c * g + d * j)
  9. L109
    specialize four_square_signed_absolute_block_representation (d * g)
  10. L110
    specialize four_square_signed_absolute_block_representation (b * j)
17Use earlier factsL111–120

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

  1. L111
    specialize four_square_signed_absolute_block_representation (c * f)
  2. L112
    specialize four_square_signed_absolute_block_representation x
  3. L113
    specialize four_square_signed_absolute_block_representation x1
  4. L114
    specialize four_square_signed_absolute_block_representation x2
  5. L115
    specialize four_square_signed_absolute_block_representation x3
  6. L116
    apply four_square_signed_absolute_block_representation
  7. L117
    exact hnonzero
  8. L118
    exact hproduct
  9. L119
    exact hblocks_left
  10. L120
    exact habsolute_left
18Use earlier factsL121–126

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

  1. L121
    exact hblocks_right_left
  2. L122
    exact habsolute_right_left
  3. L123
    exact hblocks_right_right_left
  4. L124
    exact habsolute_right_right_left
  5. L125
    exact hblocks_right_right_right
  6. L126
    exact habsolute_right_right_right

Library-wide reading audit

Original defined command ledger · 126 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_1_zero ftcn_right_case_1_zero. (e * e + f * f + g * g + j * j) + (k) * ftcn_left_case_1_zero = (0) + (k) * ftcn_right_case_1_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 · e,b · f + c · g + d · j) ∧ (ModEq(k,a · f + b · e + c · j,d · g) ∧ (ModEq(k,a · g + c · e + d · f,b · j) ∧ ModEq(k,a · j + b · g + d · e,c · f)))
    Exact native replay linehave hblocks : ((exists ftcn_left_case_1_block_0 ftcn_right_case_1_block_0. (a * e) + (k) * ftcn_left_case_1_block_0 = (b * f + c * g + d * j) + (k) * ftcn_right_case_1_block_0) /\ ((exists ftcn_left_case_1_block_1 ftcn_right_case_1_block_1. (a * f + b * e + c * j) + (k) * ftcn_left_case_1_block_1 = (d * g) + (k) * ftcn_right_case_1_block_1) /\ ((exists ftcn_left_case_1_block_2 ftcn_right_case_1_block_2. (a * g + c * e + d * f) + (k) * ftcn_left_case_1_block_2 = (b * j) + (k) * ftcn_right_case_1_block_2) /\ (exists ftcn_left_case_1_block_3 ftcn_right_case_1_block_3. (a * j + b * g + d * e) + (k) * ftcn_left_case_1_block_3 = (c * f) + (k) * ftcn_right_case_1_block_3))))
  39. 0039specialize four_square_signed_natural_negative_first_blocks k
  40. 0040specialize four_square_signed_natural_negative_first_blocks a
  41. 0041specialize four_square_signed_natural_negative_first_blocks b
  42. 0042specialize four_square_signed_natural_negative_first_blocks c
  43. 0043specialize four_square_signed_natural_negative_first_blocks d
  44. 0044specialize four_square_signed_natural_negative_first_blocks e
  45. 0045specialize four_square_signed_natural_negative_first_blocks f
  46. 0046specialize four_square_signed_natural_negative_first_blocks g
  47. 0047specialize four_square_signed_natural_negative_first_blocks j
  48. 0048apply four_square_signed_natural_negative_first_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 * e) = (b * f + c * g + d * j) + m0) \/ ((b * f + c * g + d * j) = (a * e) + m0)) /\ ((((a * f + b * e + c * j) = (d * g) + m1) \/ ((d * g) = (a * f + b * e + c * j) + m1)) /\ ((((a * g + c * e + d * f) = (b * j) + m2) \/ ((b * j) = (a * g + c * e + d * f) + m2)) /\ (((a * j + b * g + d * e) = (c * f) + m3) \/ ((c * f) = (a * j + b * g + d * e) + m3)))))
  55. 0055specialize quaternion_coordinate_absolute_total a
  56. 0056specialize quaternion_coordinate_absolute_total b
  57. 0057specialize quaternion_coordinate_absolute_total c
  58. 0058specialize quaternion_coordinate_absolute_total d
  59. 0059specialize quaternion_coordinate_absolute_total e
  60. 0060specialize quaternion_coordinate_absolute_total f
  61. 0061specialize quaternion_coordinate_absolute_total g
  62. 0062specialize quaternion_coordinate_absolute_total j
  63. 0063exact quaternion_coordinate_absolute_total
  64. 0064cases hcoordinates
  65. 0065cases hcoordinates_witness
  66. 0066cases hcoordinates_witness_witness
  67. 0067cases hcoordinates_witness_witness_witness
  68. 0068have habsolute : ((((a * e) = (b * f + c * g + d * j) + x) \/ ((b * f + c * g + d * j) = (a * e) + x)) /\ ((((a * f + b * e + c * j) = (d * g) + x1) \/ ((d * g) = (a * f + b * e + c * j) + x1)) /\ ((((a * g + c * e + d * f) = (b * j) + x2) \/ ((b * j) = (a * g + c * e + d * f) + x2)) /\ (((a * j + b * g + d * e) = (c * f) + x3) \/ ((c * f) = (a * j + b * g + d * e) + x3)))))
  69. 0069exact hcoordinates_witness_witness_witness_witness
  70. 0070have hidentity : (a * a + b * b + c * c + d * d) * (e * e + f * f + g * g + j * j) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  71. 0071specialize four_square_euler_quaternion a
  72. 0072specialize four_square_euler_quaternion b
  73. 0073specialize four_square_euler_quaternion c
  74. 0074specialize four_square_euler_quaternion d
  75. 0075specialize four_square_euler_quaternion e
  76. 0076specialize four_square_euler_quaternion f
  77. 0077specialize four_square_euler_quaternion g
  78. 0078specialize four_square_euler_quaternion j
  79. 0079specialize four_square_euler_quaternion x
  80. 0080specialize four_square_euler_quaternion x1
  81. 0081specialize four_square_euler_quaternion x2
  82. 0082specialize four_square_euler_quaternion x3
  83. 0083apply four_square_euler_quaternion
  84. 0084exact habsolute
  85. 0085have hcenter_identity : k * r = e * e + f * f + g * g + j * j
  86. 0086trans e * e + f * f + g * g + j * j
  87. 0087exact hcenter_permuted
  88. 0088refl
  89. 0089have hproduct : (p * k) * (k * r) = x * x + x1 * x1 + x2 * x2 + x3 * x3
  90. 0090trans (a * a + b * b + c * c + d * d) * (e * e + f * f + g * g + j * j)
  91. 0091congr
  92. 0092exact hfirst_permuted
  93. 0093exact hcenter_identity
  94. 0094exact hidentity
  95. 0095cases hblocks
  96. 0096cases hblocks_right
  97. 0097cases hblocks_right_right
  98. 0098cases habsolute
  99. 0099cases habsolute_right
  100. 0100cases habsolute_right_right
  101. 0101specialize four_square_signed_absolute_block_representation p
  102. 0102specialize four_square_signed_absolute_block_representation k
  103. 0103specialize four_square_signed_absolute_block_representation r
  104. 0104specialize four_square_signed_absolute_block_representation (a * e)
  105. 0105specialize four_square_signed_absolute_block_representation (a * f + b * e + c * j)
  106. 0106specialize four_square_signed_absolute_block_representation (a * g + c * e + d * f)
  107. 0107specialize four_square_signed_absolute_block_representation (a * j + b * g + d * e)
  108. 0108specialize four_square_signed_absolute_block_representation (b * f + c * g + d * j)
  109. 0109specialize four_square_signed_absolute_block_representation (d * g)
  110. 0110specialize four_square_signed_absolute_block_representation (b * j)
  111. 0111specialize four_square_signed_absolute_block_representation (c * f)
  112. 0112specialize four_square_signed_absolute_block_representation x
  113. 0113specialize four_square_signed_absolute_block_representation x1
  114. 0114specialize four_square_signed_absolute_block_representation x2
  115. 0115specialize four_square_signed_absolute_block_representation x3
  116. 0116apply four_square_signed_absolute_block_representation
  117. 0117exact hnonzero
  118. 0118exact hproduct
  119. 0119exact hblocks_left
  120. 0120exact habsolute_left
  121. 0121exact hblocks_right_left
  122. 0122exact habsolute_right_left
  123. 0123exact hblocks_right_right_left
  124. 0124exact habsolute_right_right_left
  125. 0125exact hblocks_right_right_right
  126. 0126exact habsolute_right_right_right