PA00BL

scaled_inverse_nonresidue_half_power_mod_predecessor

Alpha v34 checked-use theorem · independently closed; not Stable

A full nonresidue scaled-inverse prefix satisfies Euler's minus-one branch.

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 PA statement

forall p a n u v h A. p = S n -> ((~(p = 1) /\ forall esi_prime_left_enr_prime esi_prime_right_enr_prime. p = esi_prime_left_enr_prime * esi_prime_right_enr_prime -> esi_prime_left_enr_prime = 1 \/ esi_prime_right_enr_prime = 1)) -> ~(exists qr_x_enr_nonresidue. exists qr_u_enr_nonresidue qr_v_enr_nonresidue. qr_x_enr_nonresidue * qr_x_enr_nonresidue + p * qr_u_enr_nonresidue = a + p * qr_v_enr_nonresidue) -> (forall esip_index_enr_prefix. (exists esip_gap_enr_prefix_prefix_bound. esip_gap_enr_prefix_prefix_bound + S (esip_index_enr_prefix) = n) -> exists esip_mate_enr_prefix. ((((exists ff_h_esip_enr_prefix_entry. ff_h_esip_enr_prefix_entry + S (esip_mate_enr_prefix) = S ((S (esip_index_enr_prefix)) * v)) /\ exists ff_q_esip_enr_prefix_entry. u = ff_q_esip_enr_prefix_entry * S ((S (esip_index_enr_prefix)) * v) + (esip_mate_enr_prefix))) /\ ((exists esip_gap_enr_prefix_relation_index_bound. esip_gap_enr_prefix_relation_index_bound + S (esip_index_enr_prefix) = n) /\ ((((~((S esip_index_enr_prefix) = 0) /\ (exists esip_gap_enr_prefix_relation_scaled_left_bound. esip_gap_enr_prefix_relation_scaled_left_bound + S (S esip_index_enr_prefix) = p))) /\ (((~(esip_mate_enr_prefix = 0) /\ (exists esip_gap_enr_prefix_relation_scaled_right_bound. esip_gap_enr_prefix_relation_scaled_right_bound + S (esip_mate_enr_prefix) = p))) /\ (exists esi_mod_left_enr_prefix_relation_scaled_mod esi_mod_right_enr_prefix_relation_scaled_mod. ((S esip_index_enr_prefix) * esip_mate_enr_prefix) + p * esi_mod_left_enr_prefix_relation_scaled_mod = (a) + p * esi_mod_right_enr_prefix_relation_scaled_mod))))))) -> n = h + h -> (exists ff_b_enr_terminal_power ff_c_enr_terminal_power. ((forall ff_i_enr_terminal_power_repeat. (exists ff_lt_enr_terminal_power_repeat_bound. ff_lt_enr_terminal_power_repeat_bound + S ff_i_enr_terminal_power_repeat = h) -> (((exists ff_h_enr_terminal_power_repeat_decoded. ff_h_enr_terminal_power_repeat_decoded + S (a) = S ((S (ff_i_enr_terminal_power_repeat)) * ff_c_enr_terminal_power)) /\ exists ff_q_enr_terminal_power_repeat_decoded. ff_b_enr_terminal_power = ff_q_enr_terminal_power_repeat_decoded * S ((S (ff_i_enr_terminal_power_repeat)) * ff_c_enr_terminal_power) + (a)))) /\ (exists ff_u_enr_terminal_power_product ff_v_enr_terminal_power_product. ((((exists ff_h_enr_terminal_power_product_start. ff_h_enr_terminal_power_product_start + S (1) = S ((S (0)) * ff_v_enr_terminal_power_product)) /\ exists ff_q_enr_terminal_power_product_start. ff_u_enr_terminal_power_product = ff_q_enr_terminal_power_product_start * S ((S (0)) * ff_v_enr_terminal_power_product) + (1))) /\ ((((exists ff_h_enr_terminal_power_product_terminal. ff_h_enr_terminal_power_product_terminal + S (A) = S ((S (h)) * ff_v_enr_terminal_power_product)) /\ exists ff_q_enr_terminal_power_product_terminal. ff_u_enr_terminal_power_product = ff_q_enr_terminal_power_product_terminal * S ((S (h)) * ff_v_enr_terminal_power_product) + (A))) /\ forall ff_i_enr_terminal_power_product. (exists ff_lt_enr_terminal_power_product_bound. ff_lt_enr_terminal_power_product_bound + S ff_i_enr_terminal_power_product = h) -> exists ff_p_enr_terminal_power_product ff_r_enr_terminal_power_product ff_s_enr_terminal_power_product. ((((exists ff_h_enr_terminal_power_product_factor. ff_h_enr_terminal_power_product_factor + S (ff_p_enr_terminal_power_product) = S ((S (ff_i_enr_terminal_power_product)) * ff_c_enr_terminal_power)) /\ exists ff_q_enr_terminal_power_product_factor. ff_b_enr_terminal_power = ff_q_enr_terminal_power_product_factor * S ((S (ff_i_enr_terminal_power_product)) * ff_c_enr_terminal_power) + (ff_p_enr_terminal_power_product))) /\ ((((exists ff_h_enr_terminal_power_product_partial. ff_h_enr_terminal_power_product_partial + S (ff_r_enr_terminal_power_product) = S ((S (ff_i_enr_terminal_power_product)) * ff_v_enr_terminal_power_product)) /\ exists ff_q_enr_terminal_power_product_partial. ff_u_enr_terminal_power_product = ff_q_enr_terminal_power_product_partial * S ((S (ff_i_enr_terminal_power_product)) * ff_v_enr_terminal_power_product) + (ff_r_enr_terminal_power_product))) /\ ((((exists ff_h_enr_terminal_power_product_successor. ff_h_enr_terminal_power_product_successor + S (ff_s_enr_terminal_power_product) = S ((S (S ff_i_enr_terminal_power_product)) * ff_v_enr_terminal_power_product)) /\ exists ff_q_enr_terminal_power_product_successor. ff_u_enr_terminal_power_product = ff_q_enr_terminal_power_product_successor * S ((S (S ff_i_enr_terminal_power_product)) * ff_v_enr_terminal_power_product) + (ff_s_enr_terminal_power_product))) /\ ff_s_enr_terminal_power_product = ff_r_enr_terminal_power_product * ff_p_enr_terminal_power_product)))))))) -> (exists wpp_mod_left_enr_terminal_result wpp_mod_right_enr_terminal_result. (A) + p * wpp_mod_left_enr_terminal_result = (n) + p * wpp_mod_right_enr_terminal_result)

Structural proof guide

Generated structural guide

A full nonresidue scaled-inverse prefix satisfies Euler's minus-one branch.

Use the direct prerequisites scaled_inverse_pair_order_terminal_package, scaled_pair_order_terminal_power_mod_predecessor as previously established PA formulas.

The proof proceeds by case analysis (3), intermediate claims (1).

Referenced ingredients

PA009W scaled_inverse_pair_order_terminal_package PA00BK scaled_pair_order_terminal_power_mod_predecessor

Proof neighborhood

Direct dependencies

PA009W scaled_inverse_pair_order_terminal_package PA00BK scaled_pair_order_terminal_power_mod_predecessor

Direct dependents

PA00BM quadratic_nonresidue_half_power_mod_predecessor

Formal native tactic body

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

Read the argument

Proof checkpoints

46 script commands · 7 reading checkpoints · 1 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 (2)
scaled inverse pair order terminal packagescaled pair order terminal power mod predecessor

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro n
  4. L4
    intro u
  5. L5
    intro v
  6. L6
    intro h
  7. L7
    intro A
  8. L8
    intro hpn
  9. L9
    intro hp
  10. L10
    intro hnonresidue
02Fix variables and assumptionsL11–13

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro hprefix
  2. L12
    intro heven
  3. L13
    intro hpower
03Establish hterminalL14–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply scaled inverse pair order terminal package.

  1. L14
    have hterminal : ∃ b. ∃ c. (∀ x. ∀ y. ∀ z. Lt(x,h + h) → BetaAt(b,c,x,y) → BetaAt(u,v,y,S z) → ContainsPrefix(b,c,h + h,z)) ∧ ((∀ x. Lt(x,h + h) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,n)) ∧ InjectivePrefix(b,c,h + h)) ∧ (∀ x. Lt(x,h) → ∃ y. ∃ z. BetaAt(b,c,x + x,y) ∧ (BetaAt(b,c,S (x + x),z) ∧ BetaAt(u,v,y,S z)))Definitions: LtBetaAtInjectivePrefixContainsPrefix
  2. L15
    specialize scaled_inverse_pair_order_terminal_package p
  3. L16
    specialize scaled_inverse_pair_order_terminal_package a
  4. L17
    specialize scaled_inverse_pair_order_terminal_package n
  5. L18
    specialize scaled_inverse_pair_order_terminal_package u
  6. L19
    specialize scaled_inverse_pair_order_terminal_package v
  7. L20
    specialize scaled_inverse_pair_order_terminal_package h
  8. L21
    apply scaled_inverse_pair_order_terminal_package
  9. L22
    exact hpn
  10. L23
    exact hp
04Use earlier factsL24–26

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

  1. L24
    exact hnonresidue
  2. L25
    exact hprefix
  3. L26
    exact heven
05Separate the logical casesL27–29

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

  1. L27
    cases hterminal
  2. L28
    cases hterminal_witness
  3. L29
    cases hterminal_witness_witness
06Use earlier factsL30–39

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

  1. L30
    specialize scaled_pair_order_terminal_power_mod_predecessor p
  2. L31
    specialize scaled_pair_order_terminal_power_mod_predecessor a
  3. L32
    specialize scaled_pair_order_terminal_power_mod_predecessor n
  4. L33
    specialize scaled_pair_order_terminal_power_mod_predecessor u
  5. L34
    specialize scaled_pair_order_terminal_power_mod_predecessor v
  6. L35
    specialize scaled_pair_order_terminal_power_mod_predecessor x
  7. L36
    specialize scaled_pair_order_terminal_power_mod_predecessor x1
  8. L37
    specialize scaled_pair_order_terminal_power_mod_predecessor h
  9. L38
    specialize scaled_pair_order_terminal_power_mod_predecessor A
  10. L39
    apply scaled_pair_order_terminal_power_mod_predecessor
07Use earlier factsL40–46

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

  1. L40
    exact hpn
  2. L41
    exact hp
  3. L42
    exact hprefix
  4. L43
    exact heven
  5. L44
    exact hterminal_witness_witness_left
  6. L45
    exact hterminal_witness_witness_right
  7. L46
    exact hpower

Library-wide reading audit

Original exact command ledger · 46 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro n
  4. 0004intro u
  5. 0005intro v
  6. 0006intro h
  7. 0007intro A
  8. 0008intro hpn
  9. 0009intro hp
  10. 0010intro hnonresidue
  11. 0011intro hprefix
  12. 0012intro heven
  13. 0013intro hpower
  14. 0014have hterminal : exists b c. (((forall espo_position_enr_terminal_state_closed espo_source_enr_terminal_state_closed espo_mate_enr_terminal_state_closed. (exists wpo_gap_enr_terminal_state_closed_position_bound. wpo_gap_enr_terminal_state_closed_position_bound + S (espo_position_enr_terminal_state_closed) = h + h) -> (((exists wpo_beta_height_enr_terminal_state_closed_source_entry. wpo_beta_height_enr_terminal_state_closed_source_entry + S (espo_source_enr_terminal_state_closed) = S ((S (espo_position_enr_terminal_state_closed)) * c)) /\ exists wpo_beta_quotient_enr_terminal_state_closed_source_entry. b = wpo_beta_quotient_enr_terminal_state_closed_source_entry * S ((S (espo_position_enr_terminal_state_closed)) * c) + (espo_source_enr_terminal_state_closed))) -> (((exists wpo_beta_height_enr_terminal_state_closed_scaled_entry. wpo_beta_height_enr_terminal_state_closed_scaled_entry + S (S espo_mate_enr_terminal_state_closed) = S ((S (espo_source_enr_terminal_state_closed)) * v)) /\ exists wpo_beta_quotient_enr_terminal_state_closed_scaled_entry. u = wpo_beta_quotient_enr_terminal_state_closed_scaled_entry * S ((S (espo_source_enr_terminal_state_closed)) * v) + (S espo_mate_enr_terminal_state_closed))) -> exists espo_mate_position_enr_terminal_state_closed. ((exists wpo_gap_enr_terminal_state_closed_mate_bound. wpo_gap_enr_terminal_state_closed_mate_bound + S (espo_mate_position_enr_terminal_state_closed) = h + h) /\ (((exists wpo_beta_height_enr_terminal_state_closed_mate_entry. wpo_beta_height_enr_terminal_state_closed_mate_entry + S (espo_mate_enr_terminal_state_closed) = S ((S (espo_mate_position_enr_terminal_state_closed)) * c)) /\ exists wpo_beta_quotient_enr_terminal_state_closed_mate_entry. b = wpo_beta_quotient_enr_terminal_state_closed_mate_entry * S ((S (espo_mate_position_enr_terminal_state_closed)) * c) + (espo_mate_enr_terminal_state_closed))))) /\ (((forall fom_index_enr_terminal_state_bounded. (exists fom_gap_enr_terminal_state_bounded_index_bound. fom_gap_enr_terminal_state_bounded_index_bound + S (fom_index_enr_terminal_state_bounded) = h + h) -> exists fom_value_enr_terminal_state_bounded. ((((exists fom_beta_height_enr_terminal_state_bounded_entry. fom_beta_height_enr_terminal_state_bounded_entry + S (fom_value_enr_terminal_state_bounded) = S ((S (fom_index_enr_terminal_state_bounded)) * c)) /\ exists fom_beta_quotient_enr_terminal_state_bounded_entry. b = fom_beta_quotient_enr_terminal_state_bounded_entry * S ((S (fom_index_enr_terminal_state_bounded)) * c) + (fom_value_enr_terminal_state_bounded))) /\ (exists fom_gap_enr_terminal_state_bounded_value_bound. fom_gap_enr_terminal_state_bounded_value_bound + S (fom_value_enr_terminal_state_bounded) = n))) /\ (forall wpo_injective_left_enr_terminal_state_injective wpo_injective_right_enr_terminal_state_injective wpo_injective_value_enr_terminal_state_injective. (exists wpo_gap_enr_terminal_state_injective_left_bound. wpo_gap_enr_terminal_state_injective_left_bound + S (wpo_injective_left_enr_terminal_state_injective) = h + h) -> (exists wpo_gap_enr_terminal_state_injective_right_bound. wpo_gap_enr_terminal_state_injective_right_bound + S (wpo_injective_right_enr_terminal_state_injective) = h + h) -> (((exists wpo_beta_height_enr_terminal_state_injective_left_entry. wpo_beta_height_enr_terminal_state_injective_left_entry + S (wpo_injective_value_enr_terminal_state_injective) = S ((S (wpo_injective_left_enr_terminal_state_injective)) * c)) /\ exists wpo_beta_quotient_enr_terminal_state_injective_left_entry. b = wpo_beta_quotient_enr_terminal_state_injective_left_entry * S ((S (wpo_injective_left_enr_terminal_state_injective)) * c) + (wpo_injective_value_enr_terminal_state_injective))) -> (((exists wpo_beta_height_enr_terminal_state_injective_right_entry. wpo_beta_height_enr_terminal_state_injective_right_entry + S (wpo_injective_value_enr_terminal_state_injective) = S ((S (wpo_injective_right_enr_terminal_state_injective)) * c)) /\ exists wpo_beta_quotient_enr_terminal_state_injective_right_entry. b = wpo_beta_quotient_enr_terminal_state_injective_right_entry * S ((S (wpo_injective_right_enr_terminal_state_injective)) * c) + (wpo_injective_value_enr_terminal_state_injective))) -> wpo_injective_left_enr_terminal_state_injective = wpo_injective_right_enr_terminal_state_injective))))) /\ (forall espi_pair_enr_history. (exists wpo_gap_enr_history_pair_bound. wpo_gap_enr_history_pair_bound + S (espi_pair_enr_history) = h) -> exists espi_left_enr_history espi_right_enr_history. (((((exists wpo_beta_height_enr_history_left_entry. wpo_beta_height_enr_history_left_entry + S (espi_left_enr_history) = S ((S (espi_pair_enr_history + espi_pair_enr_history)) * c)) /\ exists wpo_beta_quotient_enr_history_left_entry. b = wpo_beta_quotient_enr_history_left_entry * S ((S (espi_pair_enr_history + espi_pair_enr_history)) * c) + (espi_left_enr_history))) /\ (((((exists wpo_beta_height_enr_history_right_entry. wpo_beta_height_enr_history_right_entry + S (espi_right_enr_history) = S ((S (S (espi_pair_enr_history + espi_pair_enr_history))) * c)) /\ exists wpo_beta_quotient_enr_history_right_entry. b = wpo_beta_quotient_enr_history_right_entry * S ((S (S (espi_pair_enr_history + espi_pair_enr_history))) * c) + (espi_right_enr_history))) /\ (((exists wpo_beta_height_enr_history_scaled_edge. wpo_beta_height_enr_history_scaled_edge + S (S espi_right_enr_history) = S ((S (espi_left_enr_history)) * v)) /\ exists wpo_beta_quotient_enr_history_scaled_edge. u = wpo_beta_quotient_enr_history_scaled_edge * S ((S (espi_left_enr_history)) * v) + (S espi_right_enr_history))))))))
  15. 0015specialize scaled_inverse_pair_order_terminal_package p
  16. 0016specialize scaled_inverse_pair_order_terminal_package a
  17. 0017specialize scaled_inverse_pair_order_terminal_package n
  18. 0018specialize scaled_inverse_pair_order_terminal_package u
  19. 0019specialize scaled_inverse_pair_order_terminal_package v
  20. 0020specialize scaled_inverse_pair_order_terminal_package h
  21. 0021apply scaled_inverse_pair_order_terminal_package
  22. 0022exact hpn
  23. 0023exact hp
  24. 0024exact hnonresidue
  25. 0025exact hprefix
  26. 0026exact heven
  27. 0027cases hterminal
  28. 0028cases hterminal_witness
  29. 0029cases hterminal_witness_witness
  30. 0030specialize scaled_pair_order_terminal_power_mod_predecessor p
  31. 0031specialize scaled_pair_order_terminal_power_mod_predecessor a
  32. 0032specialize scaled_pair_order_terminal_power_mod_predecessor n
  33. 0033specialize scaled_pair_order_terminal_power_mod_predecessor u
  34. 0034specialize scaled_pair_order_terminal_power_mod_predecessor v
  35. 0035specialize scaled_pair_order_terminal_power_mod_predecessor x
  36. 0036specialize scaled_pair_order_terminal_power_mod_predecessor x1
  37. 0037specialize scaled_pair_order_terminal_power_mod_predecessor h
  38. 0038specialize scaled_pair_order_terminal_power_mod_predecessor A
  39. 0039apply scaled_pair_order_terminal_power_mod_predecessor
  40. 0040exact hpn
  41. 0041exact hp
  42. 0042exact hprefix
  43. 0043exact heven
  44. 0044exact hterminal_witness_witness_left
  45. 0045exact hterminal_witness_witness_right
  46. 0046exact hpower