Möbius values and prime adjunction — 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.

237 checked bundle nodes · 675 proof edges · 15134 body proof nodes.

Literal self-contained proof bundle · SHA-256 041f1a3471002ff3cd5fc3da2a6cc751ad2f4a4458a497b3de2a26276fd314b8

mobius_prime_step_candidate.py · mobius_value_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

MV0001 alternating_signed_unit_exists · actual bundle node 215
MV0002 alternating_signed_unit_functional · actual bundle node 216
MV0003 alternating_signed_unit_zero · actual bundle node 217
MV0004 mobius_prime_factor_count_unique · actual bundle node 218
MV0005 mobius_input_positive · actual bundle node 219
MV0006 mobius_zero_has_no_value · actual bundle node 220
MV0007 mobius_from_prime_square · actual bundle node 221
MV0008 mobius_from_squarefree_factor_count · actual bundle node 222
MV0009 mobius_value_exists · actual bundle node 223
MV000A mobius_squarefree_evaluation · actual bundle node 224
MV000B mobius_value_functional · actual bundle node 225
MV000C mobius_value_exists_unique · actual bundle node 226
MV000D mobius_one · actual bundle node 227
MV000E mobius_squarefree_divisor · actual bundle node 228
MV000F mobius_prime_squarefree · actual bundle node 229
MV0010 mobius_squarefree_fresh_prime_product · actual bundle node 230
MV0011 mobius_prime_factor_list_append · actual bundle node 231
MV0012 mobius_positive_unit_negates_to_negative_unit · actual bundle node 232
MV0013 alternating_signed_unit_successor_negates · actual bundle node 233
MV0014 mobius_prime_square_value_zero · actual bundle node 234
MV0015 mobius_fresh_prime_negates · actual bundle node 235

all_prime_succ_intro · checked inherited prerequisite

Exact statement in the checked dependency cone

forall b c l p. (forall i. (exists h. h + S i = l) -> exists p. (((exists h. h + S p = S ((S i) * c)) /\ exists w. b = w * S ((S i) * c) + p) /\ (~(p = 1) /\ forall a d. p = a * d -> a = 1 \/ d = 1))) -> (((exists h. h + S p = S ((S l) * c)) /\ exists w. b = w * S ((S l) * c) + p) /\ (~(p = 1) /\ forall a d. p = a * d -> a = 1 \/ d = 1)) -> (forall i. (exists h. h + S i = S l) -> exists p. (((exists h. h + S p = S ((S i) * c)) /\ exists w. b = w * S ((S i) * c) + p) /\ (~(p = 1) /\ forall a d. p = a * d -> a = 1 \/ d = 1)))

all_prime_transport · checked inherited prerequisite

Exact statement in the checked dependency cone

forall b c z d l. (forall i. (exists h. h + S i = l) -> exists p. (((exists h. h + S p = S ((S i) * c)) /\ exists w. b = w * S ((S i) * c) + p) /\ (~(p = 1) /\ forall a d. p = a * d -> a = 1 \/ d = 1))) -> (forall i p. (exists h. h + S i = l) -> ((exists h. h + S p = S ((S i) * c)) /\ exists w. b = w * S ((S i) * c) + p) -> ((exists h. h + S p = S ((S i) * d)) /\ exists w. z = w * S ((S i) * d) + p)) -> (forall i. (exists h. h + S i = l) -> exists p. (((exists h. h + S p = S ((S i) * d)) /\ exists w. z = w * S ((S i) * d) + p) /\ (~(p = 1) /\ forall a d. p = a * d -> a = 1 \/ d = 1)))

beta_factor_prefix_product_append · checked inherited prerequisite

Exact statement in the checked dependency cone

forall b c l r p. (exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S r = S ((S l) * v)) /\ exists q. u = q * S ((S l) * v) + r) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p)))))) -> exists z e. (((exists h. h + S p = S ((S l) * e)) /\ exists q. z = q * S ((S l) * e) + p) /\ ((forall i a. (exists h. h + S i = l) -> ((exists h. h + S a = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + a) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. z = q * S ((S i) * e) + a)) /\ (exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S (r * p) = S ((S S l) * v)) /\ exists q. u = q * S ((S S l) * v) + (r * p)) /\ forall i. (exists h. h + S i = S l) -> exists p r s. (((exists h. h + S p = S ((S i) * e)) /\ exists q. z = q * S ((S i) * e) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p))))))))

coprime_mul_left · checked inherited prerequisite

Exact statement in the checked dependency cone

forall a b n. (forall d. (exists x. a = d * x) -> (exists y. n = d * y) -> d = 1) -> (forall d. (exists x. b = d * x) -> (exists y. n = d * y) -> d = 1) -> forall d. (exists x. a * b = d * x) -> (exists y. n = d * y) -> d = 1

distinct_primes_coprime · checked inherited prerequisite

Exact statement in the checked dependency cone

forall p q. (~(p = 1) /\ forall c e. p = c * e -> c = 1 \/ e = 1) -> (~(q = 1) /\ forall c e. q = c * e -> c = 1 \/ e = 1) -> ~(p = q) -> forall d. (exists x. p = d * x) -> (exists y. q = d * y) -> d = 1

divisor_one · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall d. (exists y. 1 = d * y) -> d = 1
```
eq_decidable · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b. a = b \/ ~(a = b)
```
even_not_odd · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. (exists a. n = 2 * a) -> ~(exists b. n = 2 * b + 1)
```
factor_nonzero_left · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n c d. ~(n = 0) -> n = c * d -> ~(c = 0)
```

factor_permutation_unit_length_zero · checked inherited prerequisite

Exact statement in the checked dependency cone

forall n b c l. ((~(n = 0) /\ ((exists ff_u_fsat_unit_product ff_v_fsat_unit_product. ((((exists ff_h_fsat_unit_product_start. ff_h_fsat_unit_product_start + S (1) = S ((S (0)) * ff_v_fsat_unit_product)) /\ exists ff_q_fsat_unit_product_start. ff_u_fsat_unit_product = ff_q_fsat_unit_product_start * S ((S (0)) * ff_v_fsat_unit_product) + (1))) /\ ((((exists ff_h_fsat_unit_product_terminal. ff_h_fsat_unit_product_terminal + S (n) = S ((S (l)) * ff_v_fsat_unit_product)) /\ exists ff_q_fsat_unit_product_terminal. ff_u_fsat_unit_product = ff_q_fsat_unit_product_terminal * S ((S (l)) * ff_v_fsat_unit_product) + (n))) /\ forall ff_i_fsat_unit_product. (exists ff_lt_fsat_unit_product_bound. ff_lt_fsat_unit_product_bound + S ff_i_fsat_unit_product = l) -> exists ff_p_fsat_unit_product ff_r_fsat_unit_product ff_s_fsat_unit_product. ((((exists ff_h_fsat_unit_product_factor. ff_h_fsat_unit_product_factor + S (ff_p_fsat_unit_product) = S ((S (ff_i_fsat_unit_product)) * c)) /\ exists ff_q_fsat_unit_product_factor. b = ff_q_fsat_unit_product_factor * S ((S (ff_i_fsat_unit_product)) * c) + (ff_p_fsat_unit_product))) /\ ((((exists ff_h_fsat_unit_product_partial. ff_h_fsat_unit_product_partial + S (ff_r_fsat_unit_product) = S ((S (ff_i_fsat_unit_product)) * ff_v_fsat_unit_product)) /\ exists ff_q_fsat_unit_product_partial. ff_u_fsat_unit_product = ff_q_fsat_unit_product_partial * S ((S (ff_i_fsat_unit_product)) * ff_v_fsat_unit_product) + (ff_r_fsat_unit_product))) /\ ((((exists ff_h_fsat_unit_product_successor. ff_h_fsat_unit_product_successor + S (ff_s_fsat_unit_product) = S ((S (S ff_i_fsat_unit_product)) * ff_v_fsat_unit_product)) /\ exists ff_q_fsat_unit_product_successor. ff_u_fsat_unit_product = ff_q_fsat_unit_product_successor * S ((S (S ff_i_fsat_unit_product)) * ff_v_fsat_unit_product) + (ff_s_fsat_unit_product))) /\ ff_s_fsat_unit_product = ff_r_fsat_unit_product * ff_p_fsat_unit_product)))))) /\ (forall ftsf_index_fsat_unit_primes. (exists ftsf_gap_fsat_unit_primes_bound. ftsf_gap_fsat_unit_primes_bound + S ftsf_index_fsat_unit_primes = (l)) -> exists ftsf_factor_fsat_unit_primes. ((((exists ff_h_ftsf_fsat_unit_primes_entry. ff_h_ftsf_fsat_unit_primes_entry + S (ftsf_factor_fsat_unit_primes) = S ((S (ftsf_index_fsat_unit_primes)) * c)) /\ exists ff_q_ftsf_fsat_unit_primes_entry. b = ff_q_ftsf_fsat_unit_primes_entry * S ((S (ftsf_index_fsat_unit_primes)) * c) + (ftsf_factor_fsat_unit_primes))) /\ ((~(ftsf_factor_fsat_unit_primes = 1) /\ forall frm_prime_left_ftsf_fsat_unit_primes_prime frm_prime_right_ftsf_fsat_unit_primes_prime. ftsf_factor_fsat_unit_primes = frm_prime_left_ftsf_fsat_unit_primes_prime * frm_prime_right_ftsf_fsat_unit_primes_prime -> frm_prime_left_ftsf_fsat_unit_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_unit_primes_prime = 1))))))) -> n = 1 -> l = 0

foundation_prime_factor_list_exists · checked inherited prerequisite

Exact statement in the checked dependency cone

forall n. ~(n = 0) -> exists l b c. ((~(n = 0) /\ ((exists ff_u_fsat_exists_product ff_v_fsat_exists_product. ((((exists ff_h_fsat_exists_product_start. ff_h_fsat_exists_product_start + S (1) = S ((S (0)) * ff_v_fsat_exists_product)) /\ exists ff_q_fsat_exists_product_start. ff_u_fsat_exists_product = ff_q_fsat_exists_product_start * S ((S (0)) * ff_v_fsat_exists_product) + (1))) /\ ((((exists ff_h_fsat_exists_product_terminal. ff_h_fsat_exists_product_terminal + S (n) = S ((S (l)) * ff_v_fsat_exists_product)) /\ exists ff_q_fsat_exists_product_terminal. ff_u_fsat_exists_product = ff_q_fsat_exists_product_terminal * S ((S (l)) * ff_v_fsat_exists_product) + (n))) /\ forall ff_i_fsat_exists_product. (exists ff_lt_fsat_exists_product_bound. ff_lt_fsat_exists_product_bound + S ff_i_fsat_exists_product = l) -> exists ff_p_fsat_exists_product ff_r_fsat_exists_product ff_s_fsat_exists_product. ((((exists ff_h_fsat_exists_product_factor. ff_h_fsat_exists_product_factor + S (ff_p_fsat_exists_product) = S ((S (ff_i_fsat_exists_product)) * c)) /\ exists ff_q_fsat_exists_product_factor. b = ff_q_fsat_exists_product_factor * S ((S (ff_i_fsat_exists_product)) * c) + (ff_p_fsat_exists_product))) /\ ((((exists ff_h_fsat_exists_product_partial. ff_h_fsat_exists_product_partial + S (ff_r_fsat_exists_product) = S ((S (ff_i_fsat_exists_product)) * ff_v_fsat_exists_product)) /\ exists ff_q_fsat_exists_product_partial. ff_u_fsat_exists_product = ff_q_fsat_exists_product_partial * S ((S (ff_i_fsat_exists_product)) * ff_v_fsat_exists_product) + (ff_r_fsat_exists_product))) /\ ((((exists ff_h_fsat_exists_product_successor. ff_h_fsat_exists_product_successor + S (ff_s_fsat_exists_product) = S ((S (S ff_i_fsat_exists_product)) * ff_v_fsat_exists_product)) /\ exists ff_q_fsat_exists_product_successor. ff_u_fsat_exists_product = ff_q_fsat_exists_product_successor * S ((S (S ff_i_fsat_exists_product)) * ff_v_fsat_exists_product) + (ff_s_fsat_exists_product))) /\ ff_s_fsat_exists_product = ff_r_fsat_exists_product * ff_p_fsat_exists_product)))))) /\ (forall ftsf_index_fsat_exists_primes. (exists ftsf_gap_fsat_exists_primes_bound. ftsf_gap_fsat_exists_primes_bound + S ftsf_index_fsat_exists_primes = (l)) -> exists ftsf_factor_fsat_exists_primes. ((((exists ff_h_ftsf_fsat_exists_primes_entry. ff_h_ftsf_fsat_exists_primes_entry + S (ftsf_factor_fsat_exists_primes) = S ((S (ftsf_index_fsat_exists_primes)) * c)) /\ exists ff_q_ftsf_fsat_exists_primes_entry. b = ff_q_ftsf_fsat_exists_primes_entry * S ((S (ftsf_index_fsat_exists_primes)) * c) + (ftsf_factor_fsat_exists_primes))) /\ ((~(ftsf_factor_fsat_exists_primes = 1) /\ forall frm_prime_left_ftsf_fsat_exists_primes_prime frm_prime_right_ftsf_fsat_exists_primes_prime. ftsf_factor_fsat_exists_primes = frm_prime_left_ftsf_fsat_exists_primes_prime * frm_prime_right_ftsf_fsat_exists_primes_prime -> frm_prime_left_ftsf_fsat_exists_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_exists_primes_prime = 1)))))))

gauss_coprime_cancel · checked inherited prerequisite

Exact statement in the checked dependency cone

forall a b z. (forall d. (exists x. a = d * x) -> (exists y. b = d * y) -> d = 1) -> (exists q. b * z = a * q) -> exists w. z = a * w

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_left_cancel_nonzero · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b c. ~(a = 0) -> a * b = a * c -> b = c
```
mul_ne_zero · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b. ~(a = 0) -> ~(b = 0) -> ~(a * b = 0)
```
mul_one · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. n * 1 = n
```
multiple_mul_left · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a n m. (exists q. n = a * q) -> exists s. m * n = a * s
```
multiple_trans · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b n. (exists q. n = a * q) -> (exists r. a = b * r) -> exists s. n = b * s
```
odd_not_even · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. (exists b. n = 2 * b + 1) -> ~(exists a. n = 2 * a)
```
parity_cases · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. exists k. n = 2 * k \/ n = 2 * k + 1
```

prime_divisor_of_prime_forces_equality · checked inherited prerequisite

Exact statement in the checked dependency cone

forall p q. ((~(p = 1) /\ forall frm_prime_left_ftsp_p frm_prime_right_ftsp_p. p = frm_prime_left_ftsp_p * frm_prime_right_ftsp_p -> frm_prime_left_ftsp_p = 1 \/ frm_prime_right_ftsp_p = 1)) -> ((~(q = 1) /\ forall frm_prime_left_ftsp_q frm_prime_right_ftsp_q. q = frm_prime_left_ftsp_q * frm_prime_right_ftsp_q -> frm_prime_left_ftsp_q = 1 \/ frm_prime_right_ftsp_q = 1)) -> (exists ftcn_factor_ftsp_prime_divides_prime. (q) = (p) * ftcn_factor_ftsp_prime_divides_prime) -> p = q

prime_factor_lists_matching_by_length · checked inherited prerequisite

Exact statement in the checked dependency cone

forall l n b c m d e. ((~(n = 0) /\ ((exists ff_u_fsat_uniqueness_source_product ff_v_fsat_uniqueness_source_product. ((((exists ff_h_fsat_uniqueness_source_product_start. ff_h_fsat_uniqueness_source_product_start + S (1) = S ((S (0)) * ff_v_fsat_uniqueness_source_product)) /\ exists ff_q_fsat_uniqueness_source_product_start. ff_u_fsat_uniqueness_source_product = ff_q_fsat_uniqueness_source_product_start * S ((S (0)) * ff_v_fsat_uniqueness_source_product) + (1))) /\ ((((exists ff_h_fsat_uniqueness_source_product_terminal. ff_h_fsat_uniqueness_source_product_terminal + S (n) = S ((S (l)) * ff_v_fsat_uniqueness_source_product)) /\ exists ff_q_fsat_uniqueness_source_product_terminal. ff_u_fsat_uniqueness_source_product = ff_q_fsat_uniqueness_source_product_terminal * S ((S (l)) * ff_v_fsat_uniqueness_source_product) + (n))) /\ forall ff_i_fsat_uniqueness_source_product. (exists ff_lt_fsat_uniqueness_source_product_bound. ff_lt_fsat_uniqueness_source_product_bound + S ff_i_fsat_uniqueness_source_product = l) -> exists ff_p_fsat_uniqueness_source_product ff_r_fsat_uniqueness_source_product ff_s_fsat_uniqueness_source_product. ((((exists ff_h_fsat_uniqueness_source_product_factor. ff_h_fsat_uniqueness_source_product_factor + S (ff_p_fsat_uniqueness_source_product) = S ((S (ff_i_fsat_uniqueness_source_product)) * c)) /\ exists ff_q_fsat_uniqueness_source_product_factor. b = ff_q_fsat_uniqueness_source_product_factor * S ((S (ff_i_fsat_uniqueness_source_product)) * c) + (ff_p_fsat_uniqueness_source_product))) /\ ((((exists ff_h_fsat_uniqueness_source_product_partial. ff_h_fsat_uniqueness_source_product_partial + S (ff_r_fsat_uniqueness_source_product) = S ((S (ff_i_fsat_uniqueness_source_product)) * ff_v_fsat_uniqueness_source_product)) /\ exists ff_q_fsat_uniqueness_source_product_partial. ff_u_fsat_uniqueness_source_product = ff_q_fsat_uniqueness_source_product_partial * S ((S (ff_i_fsat_uniqueness_source_product)) * ff_v_fsat_uniqueness_source_product) + (ff_r_fsat_uniqueness_source_product))) /\ ((((exists ff_h_fsat_uniqueness_source_product_successor. ff_h_fsat_uniqueness_source_product_successor + S (ff_s_fsat_uniqueness_source_product) = S ((S (S ff_i_fsat_uniqueness_source_product)) * ff_v_fsat_uniqueness_source_product)) /\ exists ff_q_fsat_uniqueness_source_product_successor. ff_u_fsat_uniqueness_source_product = ff_q_fsat_uniqueness_source_product_successor * S ((S (S ff_i_fsat_uniqueness_source_product)) * ff_v_fsat_uniqueness_source_product) + (ff_s_fsat_uniqueness_source_product))) /\ ff_s_fsat_uniqueness_source_product = ff_r_fsat_uniqueness_source_product * ff_p_fsat_uniqueness_source_product)))))) /\ (forall ftsf_index_fsat_uniqueness_source_primes. (exists ftsf_gap_fsat_uniqueness_source_primes_bound. ftsf_gap_fsat_uniqueness_source_primes_bound + S ftsf_index_fsat_uniqueness_source_primes = (l)) -> exists ftsf_factor_fsat_uniqueness_source_primes. ((((exists ff_h_ftsf_fsat_uniqueness_source_primes_entry. ff_h_ftsf_fsat_uniqueness_source_primes_entry + S (ftsf_factor_fsat_uniqueness_source_primes) = S ((S (ftsf_index_fsat_uniqueness_source_primes)) * c)) /\ exists ff_q_ftsf_fsat_uniqueness_source_primes_entry. b = ff_q_ftsf_fsat_uniqueness_source_primes_entry * S ((S (ftsf_index_fsat_uniqueness_source_primes)) * c) + (ftsf_factor_fsat_uniqueness_source_primes))) /\ ((~(ftsf_factor_fsat_uniqueness_source_primes = 1) /\ forall frm_prime_left_ftsf_fsat_uniqueness_source_primes_prime frm_prime_right_ftsf_fsat_uniqueness_source_primes_prime. ftsf_factor_fsat_uniqueness_source_primes = frm_prime_left_ftsf_fsat_uniqueness_source_primes_prime * frm_prime_right_ftsf_fsat_uniqueness_source_primes_prime -> frm_prime_left_ftsf_fsat_uniqueness_source_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_uniqueness_source_primes_prime = 1))))))) -> ((~(n = 0) /\ ((exists ff_u_fsat_uniqueness_target_product ff_v_fsat_uniqueness_target_product. ((((exists ff_h_fsat_uniqueness_target_product_start. ff_h_fsat_uniqueness_target_product_start + S (1) = S ((S (0)) * ff_v_fsat_uniqueness_target_product)) /\ exists ff_q_fsat_uniqueness_target_product_start. ff_u_fsat_uniqueness_target_product = ff_q_fsat_uniqueness_target_product_start * S ((S (0)) * ff_v_fsat_uniqueness_target_product) + (1))) /\ ((((exists ff_h_fsat_uniqueness_target_product_terminal. ff_h_fsat_uniqueness_target_product_terminal + S (n) = S ((S (m)) * ff_v_fsat_uniqueness_target_product)) /\ exists ff_q_fsat_uniqueness_target_product_terminal. ff_u_fsat_uniqueness_target_product = ff_q_fsat_uniqueness_target_product_terminal * S ((S (m)) * ff_v_fsat_uniqueness_target_product) + (n))) /\ forall ff_i_fsat_uniqueness_target_product. (exists ff_lt_fsat_uniqueness_target_product_bound. ff_lt_fsat_uniqueness_target_product_bound + S ff_i_fsat_uniqueness_target_product = m) -> exists ff_p_fsat_uniqueness_target_product ff_r_fsat_uniqueness_target_product ff_s_fsat_uniqueness_target_product. ((((exists ff_h_fsat_uniqueness_target_product_factor. ff_h_fsat_uniqueness_target_product_factor + S (ff_p_fsat_uniqueness_target_product) = S ((S (ff_i_fsat_uniqueness_target_product)) * e)) /\ exists ff_q_fsat_uniqueness_target_product_factor. d = ff_q_fsat_uniqueness_target_product_factor * S ((S (ff_i_fsat_uniqueness_target_product)) * e) + (ff_p_fsat_uniqueness_target_product))) /\ ((((exists ff_h_fsat_uniqueness_target_product_partial. ff_h_fsat_uniqueness_target_product_partial + S (ff_r_fsat_uniqueness_target_product) = S ((S (ff_i_fsat_uniqueness_target_product)) * ff_v_fsat_uniqueness_target_product)) /\ exists ff_q_fsat_uniqueness_target_product_partial. ff_u_fsat_uniqueness_target_product = ff_q_fsat_uniqueness_target_product_partial * S ((S (ff_i_fsat_uniqueness_target_product)) * ff_v_fsat_uniqueness_target_product) + (ff_r_fsat_uniqueness_target_product))) /\ ((((exists ff_h_fsat_uniqueness_target_product_successor. ff_h_fsat_uniqueness_target_product_successor + S (ff_s_fsat_uniqueness_target_product) = S ((S (S ff_i_fsat_uniqueness_target_product)) * ff_v_fsat_uniqueness_target_product)) /\ exists ff_q_fsat_uniqueness_target_product_successor. ff_u_fsat_uniqueness_target_product = ff_q_fsat_uniqueness_target_product_successor * S ((S (S ff_i_fsat_uniqueness_target_product)) * ff_v_fsat_uniqueness_target_product) + (ff_s_fsat_uniqueness_target_product))) /\ ff_s_fsat_uniqueness_target_product = ff_r_fsat_uniqueness_target_product * ff_p_fsat_uniqueness_target_product)))))) /\ (forall ftsf_index_fsat_uniqueness_target_primes. (exists ftsf_gap_fsat_uniqueness_target_primes_bound. ftsf_gap_fsat_uniqueness_target_primes_bound + S ftsf_index_fsat_uniqueness_target_primes = (m)) -> exists ftsf_factor_fsat_uniqueness_target_primes. ((((exists ff_h_ftsf_fsat_uniqueness_target_primes_entry. ff_h_ftsf_fsat_uniqueness_target_primes_entry + S (ftsf_factor_fsat_uniqueness_target_primes) = S ((S (ftsf_index_fsat_uniqueness_target_primes)) * e)) /\ exists ff_q_ftsf_fsat_uniqueness_target_primes_entry. d = ff_q_ftsf_fsat_uniqueness_target_primes_entry * S ((S (ftsf_index_fsat_uniqueness_target_primes)) * e) + (ftsf_factor_fsat_uniqueness_target_primes))) /\ ((~(ftsf_factor_fsat_uniqueness_target_primes = 1) /\ forall frm_prime_left_ftsf_fsat_uniqueness_target_primes_prime frm_prime_right_ftsf_fsat_uniqueness_target_primes_prime. ftsf_factor_fsat_uniqueness_target_primes = frm_prime_left_ftsf_fsat_uniqueness_target_primes_prime * frm_prime_right_ftsf_fsat_uniqueness_target_primes_prime -> frm_prime_left_ftsf_fsat_uniqueness_target_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_uniqueness_target_primes_prime = 1))))))) -> (((l = m) /\ (exists pfp_u_uniqueness_result pfp_v_uniqueness_result. (((((forall pfp_i_uniqueness_resultmatchingpermutationbounded. (exists pfp_gap_uniqueness_resultmatchingpermutationboundedindex. pfp_gap_uniqueness_resultmatchingpermutationboundedindex + S (pfp_i_uniqueness_resultmatchingpermutationbounded) = (l)) -> exists pfp_a_uniqueness_resultmatchingpermutationbounded. (((exists ff_h_pfp_uniqueness_resultmatchingpermutationboundedentry. ff_h_pfp_uniqueness_resultmatchingpermutationboundedentry + S (pfp_a_uniqueness_resultmatchingpermutationbounded) = S ((S (pfp_i_uniqueness_resultmatchingpermutationbounded)) * pfp_v_uniqueness_result)) /\ exists ff_q_pfp_uniqueness_resultmatchingpermutationboundedentry. pfp_u_uniqueness_result = ff_q_pfp_uniqueness_resultmatchingpermutationboundedentry * S ((S (pfp_i_uniqueness_resultmatchingpermutationbounded)) * pfp_v_uniqueness_result) + (pfp_a_uniqueness_resultmatchingpermutationbounded))) /\ (exists pfp_gap_uniqueness_resultmatchingpermutationboundedvalue. pfp_gap_uniqueness_resultmatchingpermutationboundedvalue + S (pfp_a_uniqueness_resultmatchingpermutationbounded) = (l))) /\ (((forall pfp_i_uniqueness_resultmatchingpermutationinjective pfp_j_uniqueness_resultmatchingpermutationinjective pfp_a_uniqueness_resultmatchingpermutationinjective. (exists pfp_gap_uniqueness_resultmatchingpermutationinjectivefirst. pfp_gap_uniqueness_resultmatchingpermutationinjectivefirst + S (pfp_i_uniqueness_resultmatchingpermutationinjective) = (l)) -> (exists pfp_gap_uniqueness_resultmatchingpermutationinjectivesecond. pfp_gap_uniqueness_resultmatchingpermutationinjectivesecond + S (pfp_j_uniqueness_resultmatchingpermutationinjective) = (l)) -> (((exists ff_h_pfp_uniqueness_resultmatchingpermutationinjectiveleft. ff_h_pfp_uniqueness_resultmatchingpermutationinjectiveleft + S (pfp_a_uniqueness_resultmatchingpermutationinjective) = S ((S (pfp_i_uniqueness_resultmatchingpermutationinjective)) * pfp_v_uniqueness_result)) /\ exists ff_q_pfp_uniqueness_resultmatchingpermutationinjectiveleft. pfp_u_uniqueness_result = ff_q_pfp_uniqueness_resultmatchingpermutationinjectiveleft * S ((S (pfp_i_uniqueness_resultmatchingpermutationinjective)) * pfp_v_uniqueness_result) + (pfp_a_uniqueness_resultmatchingpermutationinjective))) -> (((exists ff_h_pfp_uniqueness_resultmatchingpermutationinjectiveright. ff_h_pfp_uniqueness_resultmatchingpermutationinjectiveright + S (pfp_a_uniqueness_resultmatchingpermutationinjective) = S ((S (pfp_j_uniqueness_resultmatchingpermutationinjective)) * pfp_v_uniqueness_result)) /\ exists ff_q_pfp_uniqueness_resultmatchingpermutationinjectiveright. pfp_u_uniqueness_result = ff_q_pfp_uniqueness_resultmatchingpermutationinjectiveright * S ((S (pfp_j_uniqueness_resultmatchingpermutationinjective)) * pfp_v_uniqueness_result) + (pfp_a_uniqueness_resultmatchingpermutationinjective))) -> pfp_i_uniqueness_resultmatchingpermutationinjective = pfp_j_uniqueness_resultmatchingpermutationinjective) /\ (forall pfp_a_uniqueness_resultmatchingpermutationsurjective. (exists pfp_gap_uniqueness_resultmatchingpermutationsurjectivevalue. pfp_gap_uniqueness_resultmatchingpermutationsurjectivevalue + S (pfp_a_uniqueness_resultmatchingpermutationsurjective) = (l)) -> exists pfp_i_uniqueness_resultmatchingpermutationsurjective. (exists pfp_gap_uniqueness_resultmatchingpermutationsurjectiveindex. pfp_gap_uniqueness_resultmatchingpermutationsurjectiveindex + S (pfp_i_uniqueness_resultmatchingpermutationsurjective) = (l)) /\ (((exists ff_h_pfp_uniqueness_resultmatchingpermutationsurjectiveentry. ff_h_pfp_uniqueness_resultmatchingpermutationsurjectiveentry + S (pfp_a_uniqueness_resultmatchingpermutationsurjective) = S ((S (pfp_i_uniqueness_resultmatchingpermutationsurjective)) * pfp_v_uniqueness_result)) /\ exists ff_q_pfp_uniqueness_resultmatchingpermutationsurjectiveentry. pfp_u_uniqueness_result = ff_q_pfp_uniqueness_resultmatchingpermutationsurjectiveentry * S ((S (pfp_i_uniqueness_resultmatchingpermutationsurjective)) * pfp_v_uniqueness_result) + (pfp_a_uniqueness_resultmatchingpermutationsurjective)))))))) /\ (forall pfp_i_uniqueness_resultmatchingmatching pfp_j_uniqueness_resultmatchingmatching pfp_a_uniqueness_resultmatchingmatching. (exists pfp_gap_uniqueness_resultmatchingmatchingbound. pfp_gap_uniqueness_resultmatchingmatchingbound + S (pfp_i_uniqueness_resultmatchingmatching) = (l)) -> (((exists ff_h_pfp_uniqueness_resultmatchingmatchingmap. ff_h_pfp_uniqueness_resultmatchingmatchingmap + S (pfp_j_uniqueness_resultmatchingmatching) = S ((S (pfp_i_uniqueness_resultmatchingmatching)) * pfp_v_uniqueness_result)) /\ exists ff_q_pfp_uniqueness_resultmatchingmatchingmap. pfp_u_uniqueness_result = ff_q_pfp_uniqueness_resultmatchingmatchingmap * S ((S (pfp_i_uniqueness_resultmatchingmatching)) * pfp_v_uniqueness_result) + (pfp_j_uniqueness_resultmatchingmatching))) -> (((exists ff_h_pfp_uniqueness_resultmatchingmatchingsource. ff_h_pfp_uniqueness_resultmatchingmatchingsource + S (pfp_a_uniqueness_resultmatchingmatching) = S ((S (pfp_i_uniqueness_resultmatchingmatching)) * c)) /\ exists ff_q_pfp_uniqueness_resultmatchingmatchingsource. b = ff_q_pfp_uniqueness_resultmatchingmatchingsource * S ((S (pfp_i_uniqueness_resultmatchingmatching)) * c) + (pfp_a_uniqueness_resultmatchingmatching))) -> (((exists ff_h_pfp_uniqueness_resultmatchingmatchingtarget. ff_h_pfp_uniqueness_resultmatchingmatchingtarget + S (pfp_a_uniqueness_resultmatchingmatching) = S ((S (pfp_j_uniqueness_resultmatchingmatching)) * e)) /\ exists ff_q_pfp_uniqueness_resultmatchingmatchingtarget. d = ff_q_pfp_uniqueness_resultmatchingmatchingtarget * S ((S (pfp_j_uniqueness_resultmatchingmatching)) * e) + (pfp_a_uniqueness_resultmatchingmatching)))))))))

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

signed_negate_symmetric · checked inherited prerequisite

Exact statement in the checked dependency cone

forall input output. (exists sn_pos_symmetric_forward sn_neg_symmetric_forward. (((input = 2 * sn_pos_symmetric_forward /\ sn_neg_symmetric_forward = 0) \/ exists sd_half_symmetric_forward_input. ((input = 2 * sd_half_symmetric_forward_input + 1 /\ sn_pos_symmetric_forward = 0) /\ sn_neg_symmetric_forward = S sd_half_symmetric_forward_input)) /\ ((output = 2 * sn_neg_symmetric_forward /\ sn_pos_symmetric_forward = 0) \/ exists sd_half_symmetric_forward_output. ((output = 2 * sd_half_symmetric_forward_output + 1 /\ sn_neg_symmetric_forward = 0) /\ sn_pos_symmetric_forward = S sd_half_symmetric_forward_output)))) -> (exists sn_pos_symmetric_reverse sn_neg_symmetric_reverse. (((output = 2 * sn_pos_symmetric_reverse /\ sn_neg_symmetric_reverse = 0) \/ exists sd_half_symmetric_reverse_input. ((output = 2 * sd_half_symmetric_reverse_input + 1 /\ sn_pos_symmetric_reverse = 0) /\ sn_neg_symmetric_reverse = S sd_half_symmetric_reverse_input)) /\ ((input = 2 * sn_neg_symmetric_reverse /\ sn_pos_symmetric_reverse = 0) \/ exists sd_half_symmetric_reverse_output. ((input = 2 * sd_half_symmetric_reverse_output + 1 /\ sn_neg_symmetric_reverse = 0) /\ sn_pos_symmetric_reverse = S sd_half_symmetric_reverse_output))))

signed_negate_zero · checked inherited prerequisite

Exact statement in the checked dependency cone

exists sn_pos_zero sn_neg_zero. (((0 = 2 * sn_pos_zero /\ sn_neg_zero = 0) \/ exists sd_half_zero_input. ((0 = 2 * sd_half_zero_input + 1 /\ sn_pos_zero = 0) /\ sn_neg_zero = S sd_half_zero_input)) /\ ((0 = 2 * sn_neg_zero /\ sn_pos_zero = 0) \/ exists sd_half_zero_output. ((0 = 2 * sd_half_zero_output + 1 /\ sn_neg_zero = 0) /\ sn_pos_zero = S sd_half_zero_output)))

squarefree_excludes_prime_square · checked inherited prerequisite

Exact statement in the checked dependency cone

forall n p. (((~((n) = 0)) /\ (forall sfd_prime_exclusion_squarefree. (~((sfd_prime_exclusion_squarefree) = 1) /\ forall pvs_left_exclusion_squarefreedomain pvs_right_exclusion_squarefreedomain. (sfd_prime_exclusion_squarefree) = pvs_left_exclusion_squarefreedomain * pvs_right_exclusion_squarefreedomain -> pvs_left_exclusion_squarefreedomain = 1 \/ pvs_right_exclusion_squarefreedomain = 1) -> (exists pvs_le_gap_exclusion_squarefreebound. pvs_le_gap_exclusion_squarefreebound + (sfd_prime_exclusion_squarefree) = (n)) -> ~(exists pvs_factor_exclusion_squarefreesquare. (n) = (sfd_prime_exclusion_squarefree * sfd_prime_exclusion_squarefree) * pvs_factor_exclusion_squarefreesquare)))) -> (~((p) = 1) /\ forall pvs_left_exclusion_prime pvs_right_exclusion_prime. (p) = pvs_left_exclusion_prime * pvs_right_exclusion_prime -> pvs_left_exclusion_prime = 1 \/ pvs_right_exclusion_prime = 1) -> (exists pvs_factor_exclusion_divisor. (n) = (p * p) * pvs_factor_exclusion_divisor) -> false

squarefree_one · checked inherited prerequisite

Exact statement in the checked dependency cone

((~((1) = 0)) /\ (forall sfd_prime_one. (~((sfd_prime_one) = 1) /\ forall pvs_left_onedomain pvs_right_onedomain. (sfd_prime_one) = pvs_left_onedomain * pvs_right_onedomain -> pvs_left_onedomain = 1 \/ pvs_right_onedomain = 1) -> (exists pvs_le_gap_onebound. pvs_le_gap_onebound + (sfd_prime_one) = (1)) -> ~(exists pvs_factor_onesquare. (1) = (sfd_prime_one * sfd_prime_one) * pvs_factor_onesquare)))

squarefree_or_prime_square_divisor · checked inherited prerequisite

Exact statement in the checked dependency cone

forall n. ~(n = 0) -> (((~((n) = 0)) /\ (forall sfd_prime_decision_squarefree. (~((sfd_prime_decision_squarefree) = 1) /\ forall pvs_left_decision_squarefreedomain pvs_right_decision_squarefreedomain. (sfd_prime_decision_squarefree) = pvs_left_decision_squarefreedomain * pvs_right_decision_squarefreedomain -> pvs_left_decision_squarefreedomain = 1 \/ pvs_right_decision_squarefreedomain = 1) -> (exists pvs_le_gap_decision_squarefreebound. pvs_le_gap_decision_squarefreebound + (sfd_prime_decision_squarefree) = (n)) -> ~(exists pvs_factor_decision_squarefreesquare. (n) = (sfd_prime_decision_squarefree * sfd_prime_decision_squarefree) * pvs_factor_decision_squarefreesquare)))) \/ exists p. (~((p) = 1) /\ forall pvs_left_decision_prime pvs_right_decision_prime. (p) = pvs_left_decision_prime * pvs_right_decision_prime -> pvs_left_decision_prime = 1 \/ pvs_right_decision_prime = 1) /\ (exists pvs_factor_decision_divisor. (n) = (p * p) * pvs_factor_decision_divisor)

successor_even_of_odd · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. (exists a. n = 2 * a + 1) -> exists b. S n = 2 * b
```
successor_odd_of_even · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. (exists a. n = 2 * a) -> exists b. S n = 2 * b + 1
```
zero_add · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. 0 + n = n
```