FS0058

four_square_signed_centered_representation

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

All sixteen actual centered sign patterns construct their signed quaternion quotient, yielding a genuine four-square representation without any orientation premise.

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 fsbr_modulus_orientation fsbr_multiplier_orientation fsbr_half_orientation fsbr_coordinate_orientation_0 fsbr_coordinate_orientation_1 fsbr_coordinate_orientation_2 fsbr_coordinate_orientation_3 fsbr_center_orientation_0 fsbr_center_orientation_1 fsbr_center_orientation_2 fsbr_center_orientation_3 fsbr_quotient_orientation. ~(fsbr_multiplier_orientation = 0) -> fsbr_multiplier_orientation = 2 * fsbr_half_orientation + 1 -> fsbr_modulus_orientation * fsbr_multiplier_orientation = fsbr_coordinate_orientation_0 * fsbr_coordinate_orientation_0 + fsbr_coordinate_orientation_1 * fsbr_coordinate_orientation_1 + fsbr_coordinate_orientation_2 * fsbr_coordinate_orientation_2 + fsbr_coordinate_orientation_3 * fsbr_coordinate_orientation_3 -> (((exists fsd_center_bound_orientation_0. fsd_center_bound_orientation_0 + (fsbr_center_orientation_0 + fsbr_center_orientation_0) = fsbr_multiplier_orientation) /\ ((exists fsd_center_lower_orientation_0. fsbr_coordinate_orientation_0 = fsbr_multiplier_orientation * fsd_center_lower_orientation_0 + fsbr_center_orientation_0) \/ (exists fsd_center_upper_orientation_0. fsbr_coordinate_orientation_0 + fsbr_center_orientation_0 = fsbr_multiplier_orientation * fsd_center_upper_orientation_0)))) -> (((exists fsd_center_bound_orientation_1. fsd_center_bound_orientation_1 + (fsbr_center_orientation_1 + fsbr_center_orientation_1) = fsbr_multiplier_orientation) /\ ((exists fsd_center_lower_orientation_1. fsbr_coordinate_orientation_1 = fsbr_multiplier_orientation * fsd_center_lower_orientation_1 + fsbr_center_orientation_1) \/ (exists fsd_center_upper_orientation_1. fsbr_coordinate_orientation_1 + fsbr_center_orientation_1 = fsbr_multiplier_orientation * fsd_center_upper_orientation_1)))) -> (((exists fsd_center_bound_orientation_2. fsd_center_bound_orientation_2 + (fsbr_center_orientation_2 + fsbr_center_orientation_2) = fsbr_multiplier_orientation) /\ ((exists fsd_center_lower_orientation_2. fsbr_coordinate_orientation_2 = fsbr_multiplier_orientation * fsd_center_lower_orientation_2 + fsbr_center_orientation_2) \/ (exists fsd_center_upper_orientation_2. fsbr_coordinate_orientation_2 + fsbr_center_orientation_2 = fsbr_multiplier_orientation * fsd_center_upper_orientation_2)))) -> (((exists fsd_center_bound_orientation_3. fsd_center_bound_orientation_3 + (fsbr_center_orientation_3 + fsbr_center_orientation_3) = fsbr_multiplier_orientation) /\ ((exists fsd_center_lower_orientation_3. fsbr_coordinate_orientation_3 = fsbr_multiplier_orientation * fsd_center_lower_orientation_3 + fsbr_center_orientation_3) \/ (exists fsd_center_upper_orientation_3. fsbr_coordinate_orientation_3 + fsbr_center_orientation_3 = fsbr_multiplier_orientation * fsd_center_upper_orientation_3)))) -> fsbr_multiplier_orientation * fsbr_quotient_orientation = fsbr_center_orientation_0 * fsbr_center_orientation_0 + fsbr_center_orientation_1 * fsbr_center_orientation_1 + fsbr_center_orientation_2 * fsbr_center_orientation_2 + fsbr_center_orientation_3 * fsbr_center_orientation_3 -> (exists fsl_a_fsbr_signed_orientation fsl_b_fsbr_signed_orientation fsl_c_fsbr_signed_orientation fsl_d_fsbr_signed_orientation. (fsbr_modulus_orientation * fsbr_quotient_orientation) = fsl_a_fsbr_signed_orientation * fsl_a_fsbr_signed_orientation + fsl_b_fsbr_signed_orientation * fsl_b_fsbr_signed_orientation + fsl_c_fsbr_signed_orientation * fsl_c_fsbr_signed_orientation + fsl_d_fsbr_signed_orientation * fsl_d_fsbr_signed_orientation)

Constructive proof overview

Generated structural guide

All sixteen actual centered sign patterns construct their signed quaternion quotient, yielding a genuine four-square representation without any orientation premise.

The unchanged tactic script uses 17 declared prerequisites and contains 395 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

FS005J four_square_signed_centered_orientation FS004Q four_square_signed_orientation_mask_00 FS004R four_square_signed_orientation_mask_01 FS004S four_square_signed_orientation_mask_02 FS004T four_square_signed_orientation_mask_03 FS004U four_square_signed_orientation_mask_04 FS004V four_square_signed_orientation_mask_05 FS004W four_square_signed_orientation_mask_06 FS004X four_square_signed_orientation_mask_07 FS004Y four_square_signed_orientation_mask_08 FS004Z four_square_signed_orientation_mask_09 FS0050 four_square_signed_orientation_mask_10 FS0051 four_square_signed_orientation_mask_11 FS0052 four_square_signed_orientation_mask_12 FS0053 four_square_signed_orientation_mask_13 FS0054 four_square_signed_orientation_mask_14 FS0055 four_square_signed_orientation_mask_15

Direct dependents

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

395 script commands · 54 reading checkpoints · 4 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 (17)
four square signed centered orientationfour square signed orientation mask 00four square signed orientation mask 01four square signed orientation mask 02four square signed orientation mask 03four square signed orientation mask 04four square signed orientation mask 05four square signed orientation mask 06four square signed orientation mask 07four square signed orientation mask 08four square signed orientation mask 09four square signed orientation mask 10four square signed orientation mask 11four square signed orientation mask 12four square signed orientation mask 13four square signed orientation mask 14four square signed orientation mask 15
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 hcenter_a
  7. L17
    intro hcenter_b
  8. L18
    intro hcenter_c
  9. L19
    intro hcenter_d
  10. L20
    intro hsecond
03Establish hsign_aL21–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed centered orientation.

  1. L21
    have hsign_a : ((exists ftcn_left_fsso_dispatch_positive_a ftcn_right_fsso_dispatch_positive_a. (a) + (k) * ftcn_left_fsso_dispatch_positive_a = (e) + (k) * ftcn_right_fsso_dispatch_positive_a) \/ (exists ftcn_left_fsso_dispatch_negative_a ftcn_right_fsso_dispatch_negative_a. (a + e) + (k) * ftcn_left_fsso_dispatch_negative_a = (0) + (k) * ftcn_right_fsso_dispatch_negative_a))
  2. L22
    specialize four_square_signed_centered_orientation k
  3. L23
    specialize four_square_signed_centered_orientation a
  4. L24
    specialize four_square_signed_centered_orientation e
  5. L25
    apply four_square_signed_centered_orientation
  6. L26
    exact hcenter_a
04Establish hsign_bL27–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed centered orientation.

  1. L27
    have hsign_b : ((exists ftcn_left_fsso_dispatch_positive_b ftcn_right_fsso_dispatch_positive_b. (b) + (k) * ftcn_left_fsso_dispatch_positive_b = (f) + (k) * ftcn_right_fsso_dispatch_positive_b) \/ (exists ftcn_left_fsso_dispatch_negative_b ftcn_right_fsso_dispatch_negative_b. (b + f) + (k) * ftcn_left_fsso_dispatch_negative_b = (0) + (k) * ftcn_right_fsso_dispatch_negative_b))
  2. L28
    specialize four_square_signed_centered_orientation k
  3. L29
    specialize four_square_signed_centered_orientation b
  4. L30
    specialize four_square_signed_centered_orientation f
  5. L31
    apply four_square_signed_centered_orientation
  6. L32
    exact hcenter_b
05Establish hsign_cL33–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed centered orientation.

  1. L33
    have hsign_c : ((exists ftcn_left_fsso_dispatch_positive_c ftcn_right_fsso_dispatch_positive_c. (c) + (k) * ftcn_left_fsso_dispatch_positive_c = (g) + (k) * ftcn_right_fsso_dispatch_positive_c) \/ (exists ftcn_left_fsso_dispatch_negative_c ftcn_right_fsso_dispatch_negative_c. (c + g) + (k) * ftcn_left_fsso_dispatch_negative_c = (0) + (k) * ftcn_right_fsso_dispatch_negative_c))
  2. L34
    specialize four_square_signed_centered_orientation k
  3. L35
    specialize four_square_signed_centered_orientation c
  4. L36
    specialize four_square_signed_centered_orientation g
  5. L37
    apply four_square_signed_centered_orientation
  6. L38
    exact hcenter_c
06Establish hsign_dL39–44

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed centered orientation.

  1. L39
    have hsign_d : ((exists ftcn_left_fsso_dispatch_positive_d ftcn_right_fsso_dispatch_positive_d. (d) + (k) * ftcn_left_fsso_dispatch_positive_d = (j) + (k) * ftcn_right_fsso_dispatch_positive_d) \/ (exists ftcn_left_fsso_dispatch_negative_d ftcn_right_fsso_dispatch_negative_d. (d + j) + (k) * ftcn_left_fsso_dispatch_negative_d = (0) + (k) * ftcn_right_fsso_dispatch_negative_d))
  2. L40
    specialize four_square_signed_centered_orientation k
  3. L41
    specialize four_square_signed_centered_orientation d
  4. L42
    specialize four_square_signed_centered_orientation j
  5. L43
    apply four_square_signed_centered_orientation
  6. L44
    exact hcenter_d
07Separate the logical casesL45–48

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

  1. L45
    cases hsign_a
  2. L46
    cases hsign_b
  3. L47
    cases hsign_c
  4. L48
    cases hsign_d
08Use earlier factsL49–58

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

  1. L49
    specialize four_square_signed_orientation_mask_00 p
  2. L50
    specialize four_square_signed_orientation_mask_00 k
  3. L51
    specialize four_square_signed_orientation_mask_00 h
  4. L52
    specialize four_square_signed_orientation_mask_00 a
  5. L53
    specialize four_square_signed_orientation_mask_00 b
  6. L54
    specialize four_square_signed_orientation_mask_00 c
  7. L55
    specialize four_square_signed_orientation_mask_00 d
  8. L56
    specialize four_square_signed_orientation_mask_00 e
  9. L57
    specialize four_square_signed_orientation_mask_00 f
  10. L58
    specialize four_square_signed_orientation_mask_00 g
09Use earlier factsL59–68

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

  1. L59
    specialize four_square_signed_orientation_mask_00 j
  2. L60
    specialize four_square_signed_orientation_mask_00 r
  3. L61
    apply four_square_signed_orientation_mask_00
  4. L62
    exact hnonzero
  5. L63
    exact hodd
  6. L64
    exact hfirst
  7. L65
    exact hsign_a_left
  8. L66
    exact hsign_b_left
  9. L67
    exact hsign_c_left
  10. L68
    exact hsign_d_left
10Use earlier factsL69–78

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

  1. L69
    exact hsecond
  2. L70
    specialize four_square_signed_orientation_mask_08 p
  3. L71
    specialize four_square_signed_orientation_mask_08 k
  4. L72
    specialize four_square_signed_orientation_mask_08 h
  5. L73
    specialize four_square_signed_orientation_mask_08 a
  6. L74
    specialize four_square_signed_orientation_mask_08 b
  7. L75
    specialize four_square_signed_orientation_mask_08 c
  8. L76
    specialize four_square_signed_orientation_mask_08 d
  9. L77
    specialize four_square_signed_orientation_mask_08 e
  10. L78
    specialize four_square_signed_orientation_mask_08 f
11Use earlier factsL79–88

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

  1. L79
    specialize four_square_signed_orientation_mask_08 g
  2. L80
    specialize four_square_signed_orientation_mask_08 j
  3. L81
    specialize four_square_signed_orientation_mask_08 r
  4. L82
    apply four_square_signed_orientation_mask_08
  5. L83
    exact hnonzero
  6. L84
    exact hodd
  7. L85
    exact hfirst
  8. L86
    exact hsign_a_left
  9. L87
    exact hsign_b_left
  10. L88
    exact hsign_c_left
12Use earlier factsL89–90

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

  1. L89
    exact hsign_d_right
  2. L90
    exact hsecond
13Separate the logical casesL91–91

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

  1. L91
    cases hsign_d
14Use earlier factsL92–101

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

  1. L92
    specialize four_square_signed_orientation_mask_04 p
  2. L93
    specialize four_square_signed_orientation_mask_04 k
  3. L94
    specialize four_square_signed_orientation_mask_04 h
  4. L95
    specialize four_square_signed_orientation_mask_04 a
  5. L96
    specialize four_square_signed_orientation_mask_04 b
  6. L97
    specialize four_square_signed_orientation_mask_04 c
  7. L98
    specialize four_square_signed_orientation_mask_04 d
  8. L99
    specialize four_square_signed_orientation_mask_04 e
  9. L100
    specialize four_square_signed_orientation_mask_04 f
  10. L101
    specialize four_square_signed_orientation_mask_04 g
15Use earlier factsL102–111

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

  1. L102
    specialize four_square_signed_orientation_mask_04 j
  2. L103
    specialize four_square_signed_orientation_mask_04 r
  3. L104
    apply four_square_signed_orientation_mask_04
  4. L105
    exact hnonzero
  5. L106
    exact hodd
  6. L107
    exact hfirst
  7. L108
    exact hsign_a_left
  8. L109
    exact hsign_b_left
  9. L110
    exact hsign_c_right
  10. L111
    exact hsign_d_left
16Use earlier factsL112–121

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

  1. L112
    exact hsecond
  2. L113
    specialize four_square_signed_orientation_mask_12 p
  3. L114
    specialize four_square_signed_orientation_mask_12 k
  4. L115
    specialize four_square_signed_orientation_mask_12 h
  5. L116
    specialize four_square_signed_orientation_mask_12 a
  6. L117
    specialize four_square_signed_orientation_mask_12 b
  7. L118
    specialize four_square_signed_orientation_mask_12 c
  8. L119
    specialize four_square_signed_orientation_mask_12 d
  9. L120
    specialize four_square_signed_orientation_mask_12 e
  10. L121
    specialize four_square_signed_orientation_mask_12 f
17Use earlier factsL122–131

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

  1. L122
    specialize four_square_signed_orientation_mask_12 g
  2. L123
    specialize four_square_signed_orientation_mask_12 j
  3. L124
    specialize four_square_signed_orientation_mask_12 r
  4. L125
    apply four_square_signed_orientation_mask_12
  5. L126
    exact hnonzero
  6. L127
    exact hodd
  7. L128
    exact hfirst
  8. L129
    exact hsign_a_left
  9. L130
    exact hsign_b_left
  10. L131
    exact hsign_c_right
18Use earlier factsL132–133

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

  1. L132
    exact hsign_d_right
  2. L133
    exact hsecond
19Separate the logical casesL134–135

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

  1. L134
    cases hsign_c
  2. L135
    cases hsign_d
20Use earlier factsL136–145

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

  1. L136
    specialize four_square_signed_orientation_mask_02 p
  2. L137
    specialize four_square_signed_orientation_mask_02 k
  3. L138
    specialize four_square_signed_orientation_mask_02 h
  4. L139
    specialize four_square_signed_orientation_mask_02 a
  5. L140
    specialize four_square_signed_orientation_mask_02 b
  6. L141
    specialize four_square_signed_orientation_mask_02 c
  7. L142
    specialize four_square_signed_orientation_mask_02 d
  8. L143
    specialize four_square_signed_orientation_mask_02 e
  9. L144
    specialize four_square_signed_orientation_mask_02 f
  10. L145
    specialize four_square_signed_orientation_mask_02 g
21Use earlier factsL146–155

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

  1. L146
    specialize four_square_signed_orientation_mask_02 j
  2. L147
    specialize four_square_signed_orientation_mask_02 r
  3. L148
    apply four_square_signed_orientation_mask_02
  4. L149
    exact hnonzero
  5. L150
    exact hodd
  6. L151
    exact hfirst
  7. L152
    exact hsign_a_left
  8. L153
    exact hsign_b_right
  9. L154
    exact hsign_c_left
  10. L155
    exact hsign_d_left
22Use earlier factsL156–165

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

  1. L156
    exact hsecond
  2. L157
    specialize four_square_signed_orientation_mask_10 p
  3. L158
    specialize four_square_signed_orientation_mask_10 k
  4. L159
    specialize four_square_signed_orientation_mask_10 h
  5. L160
    specialize four_square_signed_orientation_mask_10 a
  6. L161
    specialize four_square_signed_orientation_mask_10 b
  7. L162
    specialize four_square_signed_orientation_mask_10 c
  8. L163
    specialize four_square_signed_orientation_mask_10 d
  9. L164
    specialize four_square_signed_orientation_mask_10 e
  10. L165
    specialize four_square_signed_orientation_mask_10 f
23Use earlier factsL166–175

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

  1. L166
    specialize four_square_signed_orientation_mask_10 g
  2. L167
    specialize four_square_signed_orientation_mask_10 j
  3. L168
    specialize four_square_signed_orientation_mask_10 r
  4. L169
    apply four_square_signed_orientation_mask_10
  5. L170
    exact hnonzero
  6. L171
    exact hodd
  7. L172
    exact hfirst
  8. L173
    exact hsign_a_left
  9. L174
    exact hsign_b_right
  10. L175
    exact hsign_c_left
24Use earlier factsL176–177

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

  1. L176
    exact hsign_d_right
  2. L177
    exact hsecond
25Separate the logical casesL178–178

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

  1. L178
    cases hsign_d
26Use earlier factsL179–188

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

  1. L179
    specialize four_square_signed_orientation_mask_06 p
  2. L180
    specialize four_square_signed_orientation_mask_06 k
  3. L181
    specialize four_square_signed_orientation_mask_06 h
  4. L182
    specialize four_square_signed_orientation_mask_06 a
  5. L183
    specialize four_square_signed_orientation_mask_06 b
  6. L184
    specialize four_square_signed_orientation_mask_06 c
  7. L185
    specialize four_square_signed_orientation_mask_06 d
  8. L186
    specialize four_square_signed_orientation_mask_06 e
  9. L187
    specialize four_square_signed_orientation_mask_06 f
  10. L188
    specialize four_square_signed_orientation_mask_06 g
27Use earlier factsL189–198

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

  1. L189
    specialize four_square_signed_orientation_mask_06 j
  2. L190
    specialize four_square_signed_orientation_mask_06 r
  3. L191
    apply four_square_signed_orientation_mask_06
  4. L192
    exact hnonzero
  5. L193
    exact hodd
  6. L194
    exact hfirst
  7. L195
    exact hsign_a_left
  8. L196
    exact hsign_b_right
  9. L197
    exact hsign_c_right
  10. L198
    exact hsign_d_left
28Use earlier factsL199–208

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

  1. L199
    exact hsecond
  2. L200
    specialize four_square_signed_orientation_mask_14 p
  3. L201
    specialize four_square_signed_orientation_mask_14 k
  4. L202
    specialize four_square_signed_orientation_mask_14 h
  5. L203
    specialize four_square_signed_orientation_mask_14 a
  6. L204
    specialize four_square_signed_orientation_mask_14 b
  7. L205
    specialize four_square_signed_orientation_mask_14 c
  8. L206
    specialize four_square_signed_orientation_mask_14 d
  9. L207
    specialize four_square_signed_orientation_mask_14 e
  10. L208
    specialize four_square_signed_orientation_mask_14 f
29Use earlier factsL209–218

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

  1. L209
    specialize four_square_signed_orientation_mask_14 g
  2. L210
    specialize four_square_signed_orientation_mask_14 j
  3. L211
    specialize four_square_signed_orientation_mask_14 r
  4. L212
    apply four_square_signed_orientation_mask_14
  5. L213
    exact hnonzero
  6. L214
    exact hodd
  7. L215
    exact hfirst
  8. L216
    exact hsign_a_left
  9. L217
    exact hsign_b_right
  10. L218
    exact hsign_c_right
30Use earlier factsL219–220

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

  1. L219
    exact hsign_d_right
  2. L220
    exact hsecond
31Separate the logical casesL221–223

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

  1. L221
    cases hsign_b
  2. L222
    cases hsign_c
  3. L223
    cases hsign_d
32Use earlier factsL224–233

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

  1. L224
    specialize four_square_signed_orientation_mask_01 p
  2. L225
    specialize four_square_signed_orientation_mask_01 k
  3. L226
    specialize four_square_signed_orientation_mask_01 h
  4. L227
    specialize four_square_signed_orientation_mask_01 a
  5. L228
    specialize four_square_signed_orientation_mask_01 b
  6. L229
    specialize four_square_signed_orientation_mask_01 c
  7. L230
    specialize four_square_signed_orientation_mask_01 d
  8. L231
    specialize four_square_signed_orientation_mask_01 e
  9. L232
    specialize four_square_signed_orientation_mask_01 f
  10. L233
    specialize four_square_signed_orientation_mask_01 g
33Use earlier factsL234–243

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

  1. L234
    specialize four_square_signed_orientation_mask_01 j
  2. L235
    specialize four_square_signed_orientation_mask_01 r
  3. L236
    apply four_square_signed_orientation_mask_01
  4. L237
    exact hnonzero
  5. L238
    exact hodd
  6. L239
    exact hfirst
  7. L240
    exact hsign_a_right
  8. L241
    exact hsign_b_left
  9. L242
    exact hsign_c_left
  10. L243
    exact hsign_d_left
34Use earlier factsL244–253

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

  1. L244
    exact hsecond
  2. L245
    specialize four_square_signed_orientation_mask_09 p
  3. L246
    specialize four_square_signed_orientation_mask_09 k
  4. L247
    specialize four_square_signed_orientation_mask_09 h
  5. L248
    specialize four_square_signed_orientation_mask_09 a
  6. L249
    specialize four_square_signed_orientation_mask_09 b
  7. L250
    specialize four_square_signed_orientation_mask_09 c
  8. L251
    specialize four_square_signed_orientation_mask_09 d
  9. L252
    specialize four_square_signed_orientation_mask_09 e
  10. L253
    specialize four_square_signed_orientation_mask_09 f
35Use earlier factsL254–263

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

  1. L254
    specialize four_square_signed_orientation_mask_09 g
  2. L255
    specialize four_square_signed_orientation_mask_09 j
  3. L256
    specialize four_square_signed_orientation_mask_09 r
  4. L257
    apply four_square_signed_orientation_mask_09
  5. L258
    exact hnonzero
  6. L259
    exact hodd
  7. L260
    exact hfirst
  8. L261
    exact hsign_a_right
  9. L262
    exact hsign_b_left
  10. L263
    exact hsign_c_left
36Use earlier factsL264–265

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

  1. L264
    exact hsign_d_right
  2. L265
    exact hsecond
37Separate the logical casesL266–266

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

  1. L266
    cases hsign_d
38Use earlier factsL267–276

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

  1. L267
    specialize four_square_signed_orientation_mask_05 p
  2. L268
    specialize four_square_signed_orientation_mask_05 k
  3. L269
    specialize four_square_signed_orientation_mask_05 h
  4. L270
    specialize four_square_signed_orientation_mask_05 a
  5. L271
    specialize four_square_signed_orientation_mask_05 b
  6. L272
    specialize four_square_signed_orientation_mask_05 c
  7. L273
    specialize four_square_signed_orientation_mask_05 d
  8. L274
    specialize four_square_signed_orientation_mask_05 e
  9. L275
    specialize four_square_signed_orientation_mask_05 f
  10. L276
    specialize four_square_signed_orientation_mask_05 g
39Use earlier factsL277–286

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

  1. L277
    specialize four_square_signed_orientation_mask_05 j
  2. L278
    specialize four_square_signed_orientation_mask_05 r
  3. L279
    apply four_square_signed_orientation_mask_05
  4. L280
    exact hnonzero
  5. L281
    exact hodd
  6. L282
    exact hfirst
  7. L283
    exact hsign_a_right
  8. L284
    exact hsign_b_left
  9. L285
    exact hsign_c_right
  10. L286
    exact hsign_d_left
40Use earlier factsL287–296

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

  1. L287
    exact hsecond
  2. L288
    specialize four_square_signed_orientation_mask_13 p
  3. L289
    specialize four_square_signed_orientation_mask_13 k
  4. L290
    specialize four_square_signed_orientation_mask_13 h
  5. L291
    specialize four_square_signed_orientation_mask_13 a
  6. L292
    specialize four_square_signed_orientation_mask_13 b
  7. L293
    specialize four_square_signed_orientation_mask_13 c
  8. L294
    specialize four_square_signed_orientation_mask_13 d
  9. L295
    specialize four_square_signed_orientation_mask_13 e
  10. L296
    specialize four_square_signed_orientation_mask_13 f
41Use earlier factsL297–306

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

  1. L297
    specialize four_square_signed_orientation_mask_13 g
  2. L298
    specialize four_square_signed_orientation_mask_13 j
  3. L299
    specialize four_square_signed_orientation_mask_13 r
  4. L300
    apply four_square_signed_orientation_mask_13
  5. L301
    exact hnonzero
  6. L302
    exact hodd
  7. L303
    exact hfirst
  8. L304
    exact hsign_a_right
  9. L305
    exact hsign_b_left
  10. L306
    exact hsign_c_right
42Use earlier factsL307–308

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

  1. L307
    exact hsign_d_right
  2. L308
    exact hsecond
43Separate the logical casesL309–310

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

  1. L309
    cases hsign_c
  2. L310
    cases hsign_d
44Use earlier factsL311–320

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

  1. L311
    specialize four_square_signed_orientation_mask_03 p
  2. L312
    specialize four_square_signed_orientation_mask_03 k
  3. L313
    specialize four_square_signed_orientation_mask_03 h
  4. L314
    specialize four_square_signed_orientation_mask_03 a
  5. L315
    specialize four_square_signed_orientation_mask_03 b
  6. L316
    specialize four_square_signed_orientation_mask_03 c
  7. L317
    specialize four_square_signed_orientation_mask_03 d
  8. L318
    specialize four_square_signed_orientation_mask_03 e
  9. L319
    specialize four_square_signed_orientation_mask_03 f
  10. L320
    specialize four_square_signed_orientation_mask_03 g
45Use earlier factsL321–330

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

  1. L321
    specialize four_square_signed_orientation_mask_03 j
  2. L322
    specialize four_square_signed_orientation_mask_03 r
  3. L323
    apply four_square_signed_orientation_mask_03
  4. L324
    exact hnonzero
  5. L325
    exact hodd
  6. L326
    exact hfirst
  7. L327
    exact hsign_a_right
  8. L328
    exact hsign_b_right
  9. L329
    exact hsign_c_left
  10. L330
    exact hsign_d_left
46Use earlier factsL331–340

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

  1. L331
    exact hsecond
  2. L332
    specialize four_square_signed_orientation_mask_11 p
  3. L333
    specialize four_square_signed_orientation_mask_11 k
  4. L334
    specialize four_square_signed_orientation_mask_11 h
  5. L335
    specialize four_square_signed_orientation_mask_11 a
  6. L336
    specialize four_square_signed_orientation_mask_11 b
  7. L337
    specialize four_square_signed_orientation_mask_11 c
  8. L338
    specialize four_square_signed_orientation_mask_11 d
  9. L339
    specialize four_square_signed_orientation_mask_11 e
  10. L340
    specialize four_square_signed_orientation_mask_11 f
47Use earlier factsL341–350

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

  1. L341
    specialize four_square_signed_orientation_mask_11 g
  2. L342
    specialize four_square_signed_orientation_mask_11 j
  3. L343
    specialize four_square_signed_orientation_mask_11 r
  4. L344
    apply four_square_signed_orientation_mask_11
  5. L345
    exact hnonzero
  6. L346
    exact hodd
  7. L347
    exact hfirst
  8. L348
    exact hsign_a_right
  9. L349
    exact hsign_b_right
  10. L350
    exact hsign_c_left
48Use earlier factsL351–352

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

  1. L351
    exact hsign_d_right
  2. L352
    exact hsecond
49Separate the logical casesL353–353

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

  1. L353
    cases hsign_d
50Use earlier factsL354–363

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

  1. L354
    specialize four_square_signed_orientation_mask_07 p
  2. L355
    specialize four_square_signed_orientation_mask_07 k
  3. L356
    specialize four_square_signed_orientation_mask_07 h
  4. L357
    specialize four_square_signed_orientation_mask_07 a
  5. L358
    specialize four_square_signed_orientation_mask_07 b
  6. L359
    specialize four_square_signed_orientation_mask_07 c
  7. L360
    specialize four_square_signed_orientation_mask_07 d
  8. L361
    specialize four_square_signed_orientation_mask_07 e
  9. L362
    specialize four_square_signed_orientation_mask_07 f
  10. L363
    specialize four_square_signed_orientation_mask_07 g
51Use earlier factsL364–373

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

  1. L364
    specialize four_square_signed_orientation_mask_07 j
  2. L365
    specialize four_square_signed_orientation_mask_07 r
  3. L366
    apply four_square_signed_orientation_mask_07
  4. L367
    exact hnonzero
  5. L368
    exact hodd
  6. L369
    exact hfirst
  7. L370
    exact hsign_a_right
  8. L371
    exact hsign_b_right
  9. L372
    exact hsign_c_right
  10. L373
    exact hsign_d_left
52Use earlier factsL374–383

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

  1. L374
    exact hsecond
  2. L375
    specialize four_square_signed_orientation_mask_15 p
  3. L376
    specialize four_square_signed_orientation_mask_15 k
  4. L377
    specialize four_square_signed_orientation_mask_15 h
  5. L378
    specialize four_square_signed_orientation_mask_15 a
  6. L379
    specialize four_square_signed_orientation_mask_15 b
  7. L380
    specialize four_square_signed_orientation_mask_15 c
  8. L381
    specialize four_square_signed_orientation_mask_15 d
  9. L382
    specialize four_square_signed_orientation_mask_15 e
  10. L383
    specialize four_square_signed_orientation_mask_15 f
53Use earlier factsL384–393

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

  1. L384
    specialize four_square_signed_orientation_mask_15 g
  2. L385
    specialize four_square_signed_orientation_mask_15 j
  3. L386
    specialize four_square_signed_orientation_mask_15 r
  4. L387
    apply four_square_signed_orientation_mask_15
  5. L388
    exact hnonzero
  6. L389
    exact hodd
  7. L390
    exact hfirst
  8. L391
    exact hsign_a_right
  9. L392
    exact hsign_b_right
  10. L393
    exact hsign_c_right
54Use earlier factsL394–395

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

  1. L394
    exact hsign_d_right
  2. L395
    exact hsecond

Library-wide reading audit

Original exact command ledger · 395 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 hcenter_a
  17. 0017intro hcenter_b
  18. 0018intro hcenter_c
  19. 0019intro hcenter_d
  20. 0020intro hsecond
  21. 0021have hsign_a : ((exists ftcn_left_fsso_dispatch_positive_a ftcn_right_fsso_dispatch_positive_a. (a) + (k) * ftcn_left_fsso_dispatch_positive_a = (e) + (k) * ftcn_right_fsso_dispatch_positive_a) \/ (exists ftcn_left_fsso_dispatch_negative_a ftcn_right_fsso_dispatch_negative_a. (a + e) + (k) * ftcn_left_fsso_dispatch_negative_a = (0) + (k) * ftcn_right_fsso_dispatch_negative_a))
  22. 0022specialize four_square_signed_centered_orientation k
  23. 0023specialize four_square_signed_centered_orientation a
  24. 0024specialize four_square_signed_centered_orientation e
  25. 0025apply four_square_signed_centered_orientation
  26. 0026exact hcenter_a
  27. 0027have hsign_b : ((exists ftcn_left_fsso_dispatch_positive_b ftcn_right_fsso_dispatch_positive_b. (b) + (k) * ftcn_left_fsso_dispatch_positive_b = (f) + (k) * ftcn_right_fsso_dispatch_positive_b) \/ (exists ftcn_left_fsso_dispatch_negative_b ftcn_right_fsso_dispatch_negative_b. (b + f) + (k) * ftcn_left_fsso_dispatch_negative_b = (0) + (k) * ftcn_right_fsso_dispatch_negative_b))
  28. 0028specialize four_square_signed_centered_orientation k
  29. 0029specialize four_square_signed_centered_orientation b
  30. 0030specialize four_square_signed_centered_orientation f
  31. 0031apply four_square_signed_centered_orientation
  32. 0032exact hcenter_b
  33. 0033have hsign_c : ((exists ftcn_left_fsso_dispatch_positive_c ftcn_right_fsso_dispatch_positive_c. (c) + (k) * ftcn_left_fsso_dispatch_positive_c = (g) + (k) * ftcn_right_fsso_dispatch_positive_c) \/ (exists ftcn_left_fsso_dispatch_negative_c ftcn_right_fsso_dispatch_negative_c. (c + g) + (k) * ftcn_left_fsso_dispatch_negative_c = (0) + (k) * ftcn_right_fsso_dispatch_negative_c))
  34. 0034specialize four_square_signed_centered_orientation k
  35. 0035specialize four_square_signed_centered_orientation c
  36. 0036specialize four_square_signed_centered_orientation g
  37. 0037apply four_square_signed_centered_orientation
  38. 0038exact hcenter_c
  39. 0039have hsign_d : ((exists ftcn_left_fsso_dispatch_positive_d ftcn_right_fsso_dispatch_positive_d. (d) + (k) * ftcn_left_fsso_dispatch_positive_d = (j) + (k) * ftcn_right_fsso_dispatch_positive_d) \/ (exists ftcn_left_fsso_dispatch_negative_d ftcn_right_fsso_dispatch_negative_d. (d + j) + (k) * ftcn_left_fsso_dispatch_negative_d = (0) + (k) * ftcn_right_fsso_dispatch_negative_d))
  40. 0040specialize four_square_signed_centered_orientation k
  41. 0041specialize four_square_signed_centered_orientation d
  42. 0042specialize four_square_signed_centered_orientation j
  43. 0043apply four_square_signed_centered_orientation
  44. 0044exact hcenter_d
  45. 0045cases hsign_a
  46. 0046cases hsign_b
  47. 0047cases hsign_c
  48. 0048cases hsign_d
  49. 0049specialize four_square_signed_orientation_mask_00 p
  50. 0050specialize four_square_signed_orientation_mask_00 k
  51. 0051specialize four_square_signed_orientation_mask_00 h
  52. 0052specialize four_square_signed_orientation_mask_00 a
  53. 0053specialize four_square_signed_orientation_mask_00 b
  54. 0054specialize four_square_signed_orientation_mask_00 c
  55. 0055specialize four_square_signed_orientation_mask_00 d
  56. 0056specialize four_square_signed_orientation_mask_00 e
  57. 0057specialize four_square_signed_orientation_mask_00 f
  58. 0058specialize four_square_signed_orientation_mask_00 g
  59. 0059specialize four_square_signed_orientation_mask_00 j
  60. 0060specialize four_square_signed_orientation_mask_00 r
  61. 0061apply four_square_signed_orientation_mask_00
  62. 0062exact hnonzero
  63. 0063exact hodd
  64. 0064exact hfirst
  65. 0065exact hsign_a_left
  66. 0066exact hsign_b_left
  67. 0067exact hsign_c_left
  68. 0068exact hsign_d_left
  69. 0069exact hsecond
  70. 0070specialize four_square_signed_orientation_mask_08 p
  71. 0071specialize four_square_signed_orientation_mask_08 k
  72. 0072specialize four_square_signed_orientation_mask_08 h
  73. 0073specialize four_square_signed_orientation_mask_08 a
  74. 0074specialize four_square_signed_orientation_mask_08 b
  75. 0075specialize four_square_signed_orientation_mask_08 c
  76. 0076specialize four_square_signed_orientation_mask_08 d
  77. 0077specialize four_square_signed_orientation_mask_08 e
  78. 0078specialize four_square_signed_orientation_mask_08 f
  79. 0079specialize four_square_signed_orientation_mask_08 g
  80. 0080specialize four_square_signed_orientation_mask_08 j
  81. 0081specialize four_square_signed_orientation_mask_08 r
  82. 0082apply four_square_signed_orientation_mask_08
  83. 0083exact hnonzero
  84. 0084exact hodd
  85. 0085exact hfirst
  86. 0086exact hsign_a_left
  87. 0087exact hsign_b_left
  88. 0088exact hsign_c_left
  89. 0089exact hsign_d_right
  90. 0090exact hsecond
  91. 0091cases hsign_d
  92. 0092specialize four_square_signed_orientation_mask_04 p
  93. 0093specialize four_square_signed_orientation_mask_04 k
  94. 0094specialize four_square_signed_orientation_mask_04 h
  95. 0095specialize four_square_signed_orientation_mask_04 a
  96. 0096specialize four_square_signed_orientation_mask_04 b
  97. 0097specialize four_square_signed_orientation_mask_04 c
  98. 0098specialize four_square_signed_orientation_mask_04 d
  99. 0099specialize four_square_signed_orientation_mask_04 e
  100. 0100specialize four_square_signed_orientation_mask_04 f
  101. 0101specialize four_square_signed_orientation_mask_04 g
  102. 0102specialize four_square_signed_orientation_mask_04 j
  103. 0103specialize four_square_signed_orientation_mask_04 r
  104. 0104apply four_square_signed_orientation_mask_04
  105. 0105exact hnonzero
  106. 0106exact hodd
  107. 0107exact hfirst
  108. 0108exact hsign_a_left
  109. 0109exact hsign_b_left
  110. 0110exact hsign_c_right
  111. 0111exact hsign_d_left
  112. 0112exact hsecond
  113. 0113specialize four_square_signed_orientation_mask_12 p
  114. 0114specialize four_square_signed_orientation_mask_12 k
  115. 0115specialize four_square_signed_orientation_mask_12 h
  116. 0116specialize four_square_signed_orientation_mask_12 a
  117. 0117specialize four_square_signed_orientation_mask_12 b
  118. 0118specialize four_square_signed_orientation_mask_12 c
  119. 0119specialize four_square_signed_orientation_mask_12 d
  120. 0120specialize four_square_signed_orientation_mask_12 e
  121. 0121specialize four_square_signed_orientation_mask_12 f
  122. 0122specialize four_square_signed_orientation_mask_12 g
  123. 0123specialize four_square_signed_orientation_mask_12 j
  124. 0124specialize four_square_signed_orientation_mask_12 r
  125. 0125apply four_square_signed_orientation_mask_12
  126. 0126exact hnonzero
  127. 0127exact hodd
  128. 0128exact hfirst
  129. 0129exact hsign_a_left
  130. 0130exact hsign_b_left
  131. 0131exact hsign_c_right
  132. 0132exact hsign_d_right
  133. 0133exact hsecond
  134. 0134cases hsign_c
  135. 0135cases hsign_d
  136. 0136specialize four_square_signed_orientation_mask_02 p
  137. 0137specialize four_square_signed_orientation_mask_02 k
  138. 0138specialize four_square_signed_orientation_mask_02 h
  139. 0139specialize four_square_signed_orientation_mask_02 a
  140. 0140specialize four_square_signed_orientation_mask_02 b
  141. 0141specialize four_square_signed_orientation_mask_02 c
  142. 0142specialize four_square_signed_orientation_mask_02 d
  143. 0143specialize four_square_signed_orientation_mask_02 e
  144. 0144specialize four_square_signed_orientation_mask_02 f
  145. 0145specialize four_square_signed_orientation_mask_02 g
  146. 0146specialize four_square_signed_orientation_mask_02 j
  147. 0147specialize four_square_signed_orientation_mask_02 r
  148. 0148apply four_square_signed_orientation_mask_02
  149. 0149exact hnonzero
  150. 0150exact hodd
  151. 0151exact hfirst
  152. 0152exact hsign_a_left
  153. 0153exact hsign_b_right
  154. 0154exact hsign_c_left
  155. 0155exact hsign_d_left
  156. 0156exact hsecond
  157. 0157specialize four_square_signed_orientation_mask_10 p
  158. 0158specialize four_square_signed_orientation_mask_10 k
  159. 0159specialize four_square_signed_orientation_mask_10 h
  160. 0160specialize four_square_signed_orientation_mask_10 a
  161. 0161specialize four_square_signed_orientation_mask_10 b
  162. 0162specialize four_square_signed_orientation_mask_10 c
  163. 0163specialize four_square_signed_orientation_mask_10 d
  164. 0164specialize four_square_signed_orientation_mask_10 e
  165. 0165specialize four_square_signed_orientation_mask_10 f
  166. 0166specialize four_square_signed_orientation_mask_10 g
  167. 0167specialize four_square_signed_orientation_mask_10 j
  168. 0168specialize four_square_signed_orientation_mask_10 r
  169. 0169apply four_square_signed_orientation_mask_10
  170. 0170exact hnonzero
  171. 0171exact hodd
  172. 0172exact hfirst
  173. 0173exact hsign_a_left
  174. 0174exact hsign_b_right
  175. 0175exact hsign_c_left
  176. 0176exact hsign_d_right
  177. 0177exact hsecond
  178. 0178cases hsign_d
  179. 0179specialize four_square_signed_orientation_mask_06 p
  180. 0180specialize four_square_signed_orientation_mask_06 k
  181. 0181specialize four_square_signed_orientation_mask_06 h
  182. 0182specialize four_square_signed_orientation_mask_06 a
  183. 0183specialize four_square_signed_orientation_mask_06 b
  184. 0184specialize four_square_signed_orientation_mask_06 c
  185. 0185specialize four_square_signed_orientation_mask_06 d
  186. 0186specialize four_square_signed_orientation_mask_06 e
  187. 0187specialize four_square_signed_orientation_mask_06 f
  188. 0188specialize four_square_signed_orientation_mask_06 g
  189. 0189specialize four_square_signed_orientation_mask_06 j
  190. 0190specialize four_square_signed_orientation_mask_06 r
  191. 0191apply four_square_signed_orientation_mask_06
  192. 0192exact hnonzero
  193. 0193exact hodd
  194. 0194exact hfirst
  195. 0195exact hsign_a_left
  196. 0196exact hsign_b_right
  197. 0197exact hsign_c_right
  198. 0198exact hsign_d_left
  199. 0199exact hsecond
  200. 0200specialize four_square_signed_orientation_mask_14 p
  201. 0201specialize four_square_signed_orientation_mask_14 k
  202. 0202specialize four_square_signed_orientation_mask_14 h
  203. 0203specialize four_square_signed_orientation_mask_14 a
  204. 0204specialize four_square_signed_orientation_mask_14 b
  205. 0205specialize four_square_signed_orientation_mask_14 c
  206. 0206specialize four_square_signed_orientation_mask_14 d
  207. 0207specialize four_square_signed_orientation_mask_14 e
  208. 0208specialize four_square_signed_orientation_mask_14 f
  209. 0209specialize four_square_signed_orientation_mask_14 g
  210. 0210specialize four_square_signed_orientation_mask_14 j
  211. 0211specialize four_square_signed_orientation_mask_14 r
  212. 0212apply four_square_signed_orientation_mask_14
  213. 0213exact hnonzero
  214. 0214exact hodd
  215. 0215exact hfirst
  216. 0216exact hsign_a_left
  217. 0217exact hsign_b_right
  218. 0218exact hsign_c_right
  219. 0219exact hsign_d_right
  220. 0220exact hsecond
  221. 0221cases hsign_b
  222. 0222cases hsign_c
  223. 0223cases hsign_d
  224. 0224specialize four_square_signed_orientation_mask_01 p
  225. 0225specialize four_square_signed_orientation_mask_01 k
  226. 0226specialize four_square_signed_orientation_mask_01 h
  227. 0227specialize four_square_signed_orientation_mask_01 a
  228. 0228specialize four_square_signed_orientation_mask_01 b
  229. 0229specialize four_square_signed_orientation_mask_01 c
  230. 0230specialize four_square_signed_orientation_mask_01 d
  231. 0231specialize four_square_signed_orientation_mask_01 e
  232. 0232specialize four_square_signed_orientation_mask_01 f
  233. 0233specialize four_square_signed_orientation_mask_01 g
  234. 0234specialize four_square_signed_orientation_mask_01 j
  235. 0235specialize four_square_signed_orientation_mask_01 r
  236. 0236apply four_square_signed_orientation_mask_01
  237. 0237exact hnonzero
  238. 0238exact hodd
  239. 0239exact hfirst
  240. 0240exact hsign_a_right
  241. 0241exact hsign_b_left
  242. 0242exact hsign_c_left
  243. 0243exact hsign_d_left
  244. 0244exact hsecond
  245. 0245specialize four_square_signed_orientation_mask_09 p
  246. 0246specialize four_square_signed_orientation_mask_09 k
  247. 0247specialize four_square_signed_orientation_mask_09 h
  248. 0248specialize four_square_signed_orientation_mask_09 a
  249. 0249specialize four_square_signed_orientation_mask_09 b
  250. 0250specialize four_square_signed_orientation_mask_09 c
  251. 0251specialize four_square_signed_orientation_mask_09 d
  252. 0252specialize four_square_signed_orientation_mask_09 e
  253. 0253specialize four_square_signed_orientation_mask_09 f
  254. 0254specialize four_square_signed_orientation_mask_09 g
  255. 0255specialize four_square_signed_orientation_mask_09 j
  256. 0256specialize four_square_signed_orientation_mask_09 r
  257. 0257apply four_square_signed_orientation_mask_09
  258. 0258exact hnonzero
  259. 0259exact hodd
  260. 0260exact hfirst
  261. 0261exact hsign_a_right
  262. 0262exact hsign_b_left
  263. 0263exact hsign_c_left
  264. 0264exact hsign_d_right
  265. 0265exact hsecond
  266. 0266cases hsign_d
  267. 0267specialize four_square_signed_orientation_mask_05 p
  268. 0268specialize four_square_signed_orientation_mask_05 k
  269. 0269specialize four_square_signed_orientation_mask_05 h
  270. 0270specialize four_square_signed_orientation_mask_05 a
  271. 0271specialize four_square_signed_orientation_mask_05 b
  272. 0272specialize four_square_signed_orientation_mask_05 c
  273. 0273specialize four_square_signed_orientation_mask_05 d
  274. 0274specialize four_square_signed_orientation_mask_05 e
  275. 0275specialize four_square_signed_orientation_mask_05 f
  276. 0276specialize four_square_signed_orientation_mask_05 g
  277. 0277specialize four_square_signed_orientation_mask_05 j
  278. 0278specialize four_square_signed_orientation_mask_05 r
  279. 0279apply four_square_signed_orientation_mask_05
  280. 0280exact hnonzero
  281. 0281exact hodd
  282. 0282exact hfirst
  283. 0283exact hsign_a_right
  284. 0284exact hsign_b_left
  285. 0285exact hsign_c_right
  286. 0286exact hsign_d_left
  287. 0287exact hsecond
  288. 0288specialize four_square_signed_orientation_mask_13 p
  289. 0289specialize four_square_signed_orientation_mask_13 k
  290. 0290specialize four_square_signed_orientation_mask_13 h
  291. 0291specialize four_square_signed_orientation_mask_13 a
  292. 0292specialize four_square_signed_orientation_mask_13 b
  293. 0293specialize four_square_signed_orientation_mask_13 c
  294. 0294specialize four_square_signed_orientation_mask_13 d
  295. 0295specialize four_square_signed_orientation_mask_13 e
  296. 0296specialize four_square_signed_orientation_mask_13 f
  297. 0297specialize four_square_signed_orientation_mask_13 g
  298. 0298specialize four_square_signed_orientation_mask_13 j
  299. 0299specialize four_square_signed_orientation_mask_13 r
  300. 0300apply four_square_signed_orientation_mask_13
  301. 0301exact hnonzero
  302. 0302exact hodd
  303. 0303exact hfirst
  304. 0304exact hsign_a_right
  305. 0305exact hsign_b_left
  306. 0306exact hsign_c_right
  307. 0307exact hsign_d_right
  308. 0308exact hsecond
  309. 0309cases hsign_c
  310. 0310cases hsign_d
  311. 0311specialize four_square_signed_orientation_mask_03 p
  312. 0312specialize four_square_signed_orientation_mask_03 k
  313. 0313specialize four_square_signed_orientation_mask_03 h
  314. 0314specialize four_square_signed_orientation_mask_03 a
  315. 0315specialize four_square_signed_orientation_mask_03 b
  316. 0316specialize four_square_signed_orientation_mask_03 c
  317. 0317specialize four_square_signed_orientation_mask_03 d
  318. 0318specialize four_square_signed_orientation_mask_03 e
  319. 0319specialize four_square_signed_orientation_mask_03 f
  320. 0320specialize four_square_signed_orientation_mask_03 g
  321. 0321specialize four_square_signed_orientation_mask_03 j
  322. 0322specialize four_square_signed_orientation_mask_03 r
  323. 0323apply four_square_signed_orientation_mask_03
  324. 0324exact hnonzero
  325. 0325exact hodd
  326. 0326exact hfirst
  327. 0327exact hsign_a_right
  328. 0328exact hsign_b_right
  329. 0329exact hsign_c_left
  330. 0330exact hsign_d_left
  331. 0331exact hsecond
  332. 0332specialize four_square_signed_orientation_mask_11 p
  333. 0333specialize four_square_signed_orientation_mask_11 k
  334. 0334specialize four_square_signed_orientation_mask_11 h
  335. 0335specialize four_square_signed_orientation_mask_11 a
  336. 0336specialize four_square_signed_orientation_mask_11 b
  337. 0337specialize four_square_signed_orientation_mask_11 c
  338. 0338specialize four_square_signed_orientation_mask_11 d
  339. 0339specialize four_square_signed_orientation_mask_11 e
  340. 0340specialize four_square_signed_orientation_mask_11 f
  341. 0341specialize four_square_signed_orientation_mask_11 g
  342. 0342specialize four_square_signed_orientation_mask_11 j
  343. 0343specialize four_square_signed_orientation_mask_11 r
  344. 0344apply four_square_signed_orientation_mask_11
  345. 0345exact hnonzero
  346. 0346exact hodd
  347. 0347exact hfirst
  348. 0348exact hsign_a_right
  349. 0349exact hsign_b_right
  350. 0350exact hsign_c_left
  351. 0351exact hsign_d_right
  352. 0352exact hsecond
  353. 0353cases hsign_d
  354. 0354specialize four_square_signed_orientation_mask_07 p
  355. 0355specialize four_square_signed_orientation_mask_07 k
  356. 0356specialize four_square_signed_orientation_mask_07 h
  357. 0357specialize four_square_signed_orientation_mask_07 a
  358. 0358specialize four_square_signed_orientation_mask_07 b
  359. 0359specialize four_square_signed_orientation_mask_07 c
  360. 0360specialize four_square_signed_orientation_mask_07 d
  361. 0361specialize four_square_signed_orientation_mask_07 e
  362. 0362specialize four_square_signed_orientation_mask_07 f
  363. 0363specialize four_square_signed_orientation_mask_07 g
  364. 0364specialize four_square_signed_orientation_mask_07 j
  365. 0365specialize four_square_signed_orientation_mask_07 r
  366. 0366apply four_square_signed_orientation_mask_07
  367. 0367exact hnonzero
  368. 0368exact hodd
  369. 0369exact hfirst
  370. 0370exact hsign_a_right
  371. 0371exact hsign_b_right
  372. 0372exact hsign_c_right
  373. 0373exact hsign_d_left
  374. 0374exact hsecond
  375. 0375specialize four_square_signed_orientation_mask_15 p
  376. 0376specialize four_square_signed_orientation_mask_15 k
  377. 0377specialize four_square_signed_orientation_mask_15 h
  378. 0378specialize four_square_signed_orientation_mask_15 a
  379. 0379specialize four_square_signed_orientation_mask_15 b
  380. 0380specialize four_square_signed_orientation_mask_15 c
  381. 0381specialize four_square_signed_orientation_mask_15 d
  382. 0382specialize four_square_signed_orientation_mask_15 e
  383. 0383specialize four_square_signed_orientation_mask_15 f
  384. 0384specialize four_square_signed_orientation_mask_15 g
  385. 0385specialize four_square_signed_orientation_mask_15 j
  386. 0386specialize four_square_signed_orientation_mask_15 r
  387. 0387apply four_square_signed_orientation_mask_15
  388. 0388exact hnonzero
  389. 0389exact hodd
  390. 0390exact hfirst
  391. 0391exact hsign_a_right
  392. 0392exact hsign_b_right
  393. 0393exact hsign_c_right
  394. 0394exact hsign_d_right
  395. 0395exact hsecond