PA00A7 — prime_inverse_prefix

Exact expanded PA statement

forall p n. p = S n -> ((~(p = 1) /\ forall wip_prime_left_full_prime wip_prime_right_full_prime. p = wip_prime_left_full_prime * wip_prime_right_full_prime -> wip_prime_left_full_prime = 1 \/ wip_prime_right_full_prime = 1)) -> exists b c. (forall wip_index_full_result. (exists wip_gap_full_result_prefix_bound. wip_gap_full_result_prefix_bound + S wip_index_full_result = n) -> exists wip_mate_full_result. ((((exists wip_beta_height_full_result_decoded. wip_beta_height_full_result_decoded + S (wip_mate_full_result) = S ((S (wip_index_full_result)) * c)) /\ exists wip_beta_quotient_full_result_decoded. b = wip_beta_quotient_full_result_decoded * S ((S (wip_index_full_result)) * c) + (wip_mate_full_result))) /\ ((exists wip_gap_full_result_inverse_index_bound. wip_gap_full_result_inverse_index_bound + S wip_index_full_result = n) /\ ((exists wip_gap_full_result_inverse_mate_bound. wip_gap_full_result_inverse_mate_bound + S wip_mate_full_result = n) /\ (exists wip_mod_left_full_result_inverse_mod wip_mod_right_full_result_inverse_mod. ((S wip_index_full_result) * S wip_mate_full_result) + p * wip_mod_left_full_result_inverse_mod = 1 + p * wip_mod_right_full_result_inverse_mod)))))

Structural proof guide

Generated structural guide

A prime predecessor interval has a full beta-coded inverse map.

Use the direct prerequisites le_refl, prime_inverse_prefix_exists_bounded as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA001A le_refl PA00A6 prime_inverse_prefix_exists_bounded

Proof neighborhood

Direct dependencies

PA001A le_refl PA00A6 prime_inverse_prefix_exists_bounded

Direct dependents

PA00BF prime_terminal_range_two_product_mod_one_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.