Prime-field arithmetic and finite tables — exact evidence

Current Alpha v34 checked use; first admitted v31; not Stable. Original HA and the independently compiled Lean checker have freshly verified the complete bundle before this page was generated.

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

228 checked bundle nodes · 611 proof edges · 12012 body proof nodes.

Literal self-contained proof bundle · SHA-256 688e7141106c19adec6fa52a0ae77af3d389b77df512622adc93bd3b0c7ba04e

prime_field_arithmetic_candidate.py · prime_field_finiteness_candidate.py · prime_field_tables_candidate.py

Unchanged historical local checkpoint record · Historical snapshot manifest. Those records retain their original non-admitting flags; current authority comes from the separate freshly verified v31 release.

Exact theorem nodes and inherited prerequisites

FP0001 prime_field_mod_of_equal · actual bundle node 140
FP0002 prime_field_zero_below_prime · actual bundle node 141
FP0003 prime_field_residue_reflexive · actual bundle node 142
FP0004 prime_field_residue_input_equal · actual bundle node 143
FP0005 prime_field_residue_congruence_transport · actual bundle node 144
FP0006 prime_field_residue_bounded_value · actual bundle node 145
FP0007 prime_field_residue_modulus_zero · actual bundle node 146
FP0008 prime_field_add_exists · actual bundle node 147
FP0009 prime_field_add_functional · actual bundle node 148
FP000A prime_field_add_exists_unique · actual bundle node 149
FP000B prime_field_add_commutative · actual bundle node 150
FP000C prime_field_multiply_exists · actual bundle node 151
FP000D prime_field_multiply_functional · actual bundle node 152
FP000E prime_field_multiply_exists_unique · actual bundle node 153
FP000F prime_field_multiply_commutative · actual bundle node 154
FP0010 prime_field_add_associative · actual bundle node 155
FP0011 prime_field_multiply_associative · actual bundle node 156
FP0012 prime_field_left_distributive · actual bundle node 157
FP0013 prime_field_right_distributive · actual bundle node 158
FP0014 prime_field_add_zero_right · actual bundle node 159
FP0015 prime_field_add_zero_left · actual bundle node 160
FP0016 prime_field_multiply_one_right · actual bundle node 161
FP0017 prime_field_multiply_one_left · actual bundle node 162
FP0018 prime_field_multiply_zero_right · actual bundle node 163
FP0019 prime_field_multiply_zero_left · actual bundle node 164
FP001A prime_field_add_cancel_left · actual bundle node 165
FP001B prime_field_negate_exists · actual bundle node 166
FP001C prime_field_negate_functional · actual bundle node 167
FP001D prime_field_negate_exists_unique · actual bundle node 168
FP001E prime_field_inverse_exists · actual bundle node 169
FP001F prime_field_inverse_functional · actual bundle node 170
FP0020 prime_field_inverse_exists_unique · actual bundle node 171
FP0021 prime_field_zero_has_no_multiplicative_inverse · actual bundle node 172
FP0022 prime_field_inverse_output_nonzero · actual bundle node 173
FP0023 prime_field_inverse_symmetric · actual bundle node 174
FP0024 prime_field_nonzero_coprime · actual bundle node 175
FP0025 prime_field_multiply_cancel_nonzero_left · actual bundle node 176
FP0026 prime_field_no_zero_divisors · actual bundle node 177
FP0027 prime_field_residue_add · actual bundle node 178
FP0028 prime_field_residue_multiply · actual bundle node 179
FP0029 prime_field_positive_below_modulus_not_zero · actual bundle node 180
FP002A prime_field_arithmetic_laws · actual bundle node 181
FP002B prime_field_add_grid_value_exists · actual bundle node 182
FP002C prime_field_multiply_grid_value_exists · actual bundle node 183
FP002D prime_field_zero_extended_inverse_exists · actual bundle node 184
FP002E prime_field_zero_extended_inverse_functional · actual bundle node 185
FP002F prime_field_add_prefix_choice · actual bundle node 186
FP0030 prime_field_multiply_prefix_choice · actual bundle node 187
FP0031 prime_field_negate_prefix_choice · actual bundle node 188
FP0032 prime_field_inverse_prefix_choice · actual bundle node 189
FP0033 prime_field_add_table_exists · actual bundle node 190
FP0034 prime_field_multiply_table_exists · actual bundle node 191
FP0035 prime_field_negate_table_exists · actual bundle node 192
FP0036 prime_field_inverse_table_exists · actual bundle node 193
FP0037 prime_field_operation_tables_exists · actual bundle node 194
FP0038 prime_field_add_grid_value_lookup · actual bundle node 195
FP0039 prime_field_add_table_lookup · actual bundle node 196
FP003A prime_field_add_table_reflect · actual bundle node 197
FP003B prime_field_multiply_grid_value_lookup · actual bundle node 198
FP003C prime_field_multiply_table_lookup · actual bundle node 199
FP003D prime_field_multiply_table_reflect · actual bundle node 200
FP003E prime_field_negate_table_lookup · actual bundle node 201
FP003F prime_field_negate_table_reflect · actual bundle node 202
FP0040 prime_field_inverse_table_lookup · actual bundle node 203
FP0041 prime_field_inverse_table_reflect · actual bundle node 204
FP0042 prime_field_add_table_commutative · actual bundle node 205
FP0043 prime_field_add_table_associative · actual bundle node 206
FP0044 prime_field_multiply_table_commutative · actual bundle node 207
FP0045 prime_field_multiply_table_associative · actual bundle node 208
FP0046 prime_field_inverse_table_zero · actual bundle node 209
FP0047 prime_field_inverse_table_nonzero · actual bundle node 210
FP0048 prime_field_left_table_distributive · actual bundle node 211
FP0049 prime_field_right_table_distributive · actual bundle node 212
FP004A prime_field_enumeration_value · actual bundle node 213
FP004B prime_field_enumeration_is_bijection · actual bundle node 214
FP004C prime_field_cardinality_exists · actual bundle node 215
FP004D prime_field_unit_trace_recode · actual bundle node 216
FP004E prime_field_unit_trace_successor · actual bundle node 217
FP004F prime_field_unit_trace_residue · actual bundle node 218
FP0050 prime_field_unit_trace_result_bounded · actual bundle node 219
FP0051 prime_field_unit_trace_exists · actual bundle node 220
FP0052 prime_field_unit_multiple_residue · actual bundle node 221
FP0053 prime_field_unit_multiple_from_residue · actual bundle node 222
FP0054 prime_field_unit_multiple_functional · actual bundle node 223
FP0055 prime_field_unit_multiple_exists_unique · actual bundle node 224
FP0056 prime_field_characteristic_exact · actual bundle node 225
FP0057 prime_field_of_prime_order_exists · actual bundle node 226
add_assoc · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n m k. (n + m) + k = n + (m + k)
```
add_comm · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n m. n + m = m + n
```
add_mul · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n m k. (n + m) * k = n * k + m * k
```

beta_at_exists · checked inherited prerequisite

Exact statement in the checked dependency cone

forall b c i. exists x. ((exists h. h + S x = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + x)

beta_at_unique · checked inherited prerequisite

Exact statement in the checked dependency cone

forall b c i x y. ((exists h. h + S x = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + x) -> ((exists h. h + S y = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + y) -> x = y

beta_prefix_extend · checked inherited prerequisite

Exact statement in the checked dependency cone

forall k b e s. exists z c. (((exists h. h + S s = S ((S k) * c)) /\ exists q. z = q * S ((S k) * c) + s) /\ forall i a. (exists h. h + S i = k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> ((exists h. h + S a = S ((S i) * c)) /\ exists q. z = q * S ((S i) * c) + a))

binary_canonical_residue_functional · checked inherited prerequisite

Exact statement in the checked dependency cone

forall m n r s. (((exists ff_gap_binary_value. ff_gap_binary_value + S (r) = m) /\ (exists ff_left_binary_value_congruence ff_right_binary_value_congruence. (n) + m * ff_left_binary_value_congruence = (r) + m * ff_right_binary_value_congruence))) -> (((exists ff_gap_binary_other. ff_gap_binary_other + S (s) = m) /\ (exists ff_left_binary_other_congruence ff_right_binary_other_congruence. (n) + m * ff_left_binary_other_congruence = (s) + m * ff_right_binary_other_congruence))) -> r = s

bounded_mod_inverse_unique · checked inherited prerequisite

Exact statement in the checked dependency cone

forall p x y z. (exists wip_strict_gap_unique_y_bound. wip_strict_gap_unique_y_bound + S y = p) -> (exists wip_strict_gap_unique_z_bound. wip_strict_gap_unique_z_bound + S z = p) -> (exists wip_mod_left_unique_xy wip_mod_right_unique_xy. x * y + p * wip_mod_left_unique_xy = 1 + p * wip_mod_right_unique_xy) -> (exists wip_mod_left_unique_xz wip_mod_right_unique_xz. x * z + p * wip_mod_left_unique_xz = 1 + p * wip_mod_right_unique_xz) -> y = z

division_remainder_exists · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall m n. ~(m = 0) -> exists q r. n = m * q + r /\ S r <= m
```

division_remainder_unique · checked inherited prerequisite

Exact statement in the checked dependency cone

forall m n q r q2 r2. n = m * q + r -> (exists k. k + S r = m) -> n = m * q2 + r2 -> (exists k. k + S r2 = m) -> q = q2 /\ r = r2

eq_decidable · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b. a = b \/ ~(a = b)
```
finite_lt_succ_eq_or_lt · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n x. (exists h. h + S x = S n) -> x = n \/ exists h. h + S x = n
```

hensel_canonical_residue_exists · checked inherited prerequisite

Exact statement in the checked dependency cone

forall m a. ~(m = 0) -> exists r. ((exists hpl_gap_bound. hpl_gap_bound + S (r) = (m)) /\ (exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. a + m * hgcrt_mod_left_hpl_mod = r + m * hgcrt_mod_right_hpl_mod))

le_succ · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b. (exists k. k + a = b) -> exists r. r + a = S b
```
lt_not_le · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b. (exists k. k + S a = b) -> ~ (exists k. k + b = a)
```

matrix_lattice_identity_selector_exists · checked inherited prerequisite

Exact statement in the checked dependency cone

forall d. exists b c. (forall mdr_i_identity_exists. (exists mdr_gap_identity_existsbound. mdr_gap_identity_existsbound + S (mdr_i_identity_exists) = (d)) -> (((exists ff_h_mdr_identity_existsentry. ff_h_mdr_identity_existsentry + S (mdr_i_identity_exists) = S ((S (mdr_i_identity_exists)) * c)) /\ exists ff_q_mdr_identity_existsentry. b = ff_q_mdr_identity_existsentry * S ((S (mdr_i_identity_exists)) * c) + (mdr_i_identity_exists))))

matrix_recursive_flattened_index_bound · checked inherited prerequisite

Exact statement in the checked dependency cone

forall w r s. (exists mdr_gap_flat_row. mdr_gap_flat_row + S (r) = (w)) -> (exists mdr_gap_flat_column. mdr_gap_flat_column + S (s) = (w)) -> (exists mdr_gap_flat_result. mdr_gap_flat_result + S (r * w + s) = (w * w))

matrix_recursive_quotient_row_bound · checked inherited prerequisite

Exact statement in the checked dependency cone

forall q k r s. k = q * r + s -> (exists mdr_gap_quotient_source. mdr_gap_quotient_source + S (k) = (q * q)) -> (exists mdr_gap_quotient_row. mdr_gap_quotient_row + S (r) = (q))

mod_eq_add · checked inherited prerequisite

Exact statement in the checked dependency cone

forall m a b c d. (exists u v. a + m * u = b + m * v) -> (exists r s. c + m * r = d + m * s) -> exists x y. (a + c) + m * x = (b + d) + m * y

mod_eq_add_cancel_left · checked inherited prerequisite

Exact statement in the checked dependency cone

forall d a b c. (exists fspm_u_cancel_input fspm_v_cancel_input. (a + b) + d * fspm_u_cancel_input = (a + c) + d * fspm_v_cancel_input) -> (exists fspm_u_cancel_result fspm_v_cancel_result. (b) + d * fspm_u_cancel_result = (c) + d * fspm_v_cancel_result)

mod_eq_bounded_unique · checked inherited prerequisite

Exact statement in the checked dependency cone

forall m a b. (exists ha. ha + S a = m) -> (exists hb. hb + S b = m) -> (exists u v. a + m * u = b + m * v) -> a = b

mod_eq_cancel_coprime · checked inherited prerequisite

Exact statement in the checked dependency cone

forall m a x y. ~(m = 0) -> (forall d. (exists x. a = d * x) -> (exists y. m = d * y) -> d = 1) -> (exists u v. (a * x) + m * u = (a * y) + m * v) -> exists r s. x + m * r = y + m * s

mod_eq_mul · checked inherited prerequisite

Exact statement in the checked dependency cone

forall m a b c d. (exists u v. a + m * u = b + m * v) -> (exists r s. c + m * r = d + m * s) -> exists x y. (a * c) + m * x = (b * d) + m * y

mod_eq_mul_left · checked inherited prerequisite

Exact statement in the checked dependency cone

forall m a b c. (exists u v. a + m * u = b + m * v) -> exists r s. (c * a) + m * r = (c * b) + m * s

mod_eq_mul_right · checked inherited prerequisite

Exact statement in the checked dependency cone

forall m a b c. (exists u v. a + m * u = b + m * v) -> exists r s. (a * c) + m * r = (b * c) + m * s

mod_eq_refl · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall m a. exists u v. a + m * u = a + m * v
```
mod_eq_symm · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall m a b. (exists u v. a + m * u = b + m * v) -> exists r s. b + m * r = a + m * s
```

mod_eq_trans · checked inherited prerequisite

Exact statement in the checked dependency cone

forall m a b c. (exists u v. a + m * u = b + m * v) -> (exists r s. b + m * r = c + m * s) -> exists x y. a + m * x = c + m * y

mod_inverse_implies_coprime · checked inherited prerequisite

Exact statement in the checked dependency cone

forall a m z. (exists hmi_left_offset_converse_assumption hmi_right_offset_converse_assumption. a * z + m * hmi_left_offset_converse_assumption = 1 + m * hmi_right_offset_converse_assumption) -> (forall hmi_divisor_converse_result. (exists hmi_left_factor_converse_result. a = hmi_divisor_converse_result * hmi_left_factor_converse_result) -> (exists hmi_right_factor_converse_result. m = hmi_divisor_converse_result * hmi_right_factor_converse_result) -> hmi_divisor_converse_result = 1)

mul_add · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n m k. n * (m + k) = n * m + n * k
```
mul_assoc · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n m k. (n * m) * k = n * (m * k)
```
mul_comm · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n m. n * m = m * n
```
mul_one · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. n * 1 = n
```
one_le_of_ne_zero · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. ~(n = 0) -> 1 <= n
```

prime_bounded_nonzero_mod_inverse · checked inherited prerequisite

Exact statement in the checked dependency cone

forall p a. ((~(p = 1) /\ forall qrbu_factor_left_prime_p qrbu_factor_right_prime_p. p = qrbu_factor_left_prime_p * qrbu_factor_right_prime_p -> qrbu_factor_left_prime_p = 1 \/ qrbu_factor_right_prime_p = 1)) -> ~(a = 0) -> (exists qrbu_gap_a_lt_p. qrbu_gap_a_lt_p + S a = p) -> (exists qrbu_inverse_bounded_inverse. (~(qrbu_inverse_bounded_inverse = 0) /\ ((exists qrbu_gap_bounded_inverse_bound. qrbu_gap_bounded_inverse_bound + S qrbu_inverse_bounded_inverse = p) /\ (exists qrbu_mod_left_bounded_inverse_mod qrbu_mod_right_bounded_inverse_mod. a * qrbu_inverse_bounded_inverse + p * qrbu_mod_left_bounded_inverse_mod = 1 + p * qrbu_mod_right_bounded_inverse_mod))))

prime_nonzero · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall p. (~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1) -> ~(p = 0)
```

prime_two_le · checked inherited prerequisite

Exact statement in the checked dependency cone

forall p. ((~(p = 1) /\ forall frm_prime_left_bpvl_prime frm_prime_right_bpvl_prime. p = frm_prime_left_bpvl_prime * frm_prime_right_bpvl_prime -> frm_prime_left_bpvl_prime = 1 \/ frm_prime_right_bpvl_prime = 1)) -> (exists bpvl_gap_prime_two. bpvl_gap_prime_two + (2) = (p))

signed_integer_floor_exists · checked inherited prerequisite

Exact statement in the checked dependency cone

forall xp xn m. ~(m = 0) -> exists qp qn r. (((xp) + (m) * (qn) = ((xn) + (m) * (qp)) + (r) /\ exists sif_gap_pair_total. sif_gap_pair_total + S (r) = (m)))

succ_le_succ · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b. (exists k. k + a = b) -> exists r. r + S a = S b
```
succ_ne_zero · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. ~(S n = 0)
```
zero_add · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. 0 + n = n
```
zero_le · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. 0 <= n
```