PA00BM · theorem

quadratic_nonresidue_half_power_mod_predecessor

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

For a reduced nonzero nonresidue, a^((p-1)/2) is p-1 modulo p.

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.

Statement with defined notation

∀ p. ∀ a. ∀ n. ∀ h. ∀ A. p = S n → Prime(p) → ¬a = 0 → Lt(a,p) → ¬QRes(p,a) → n = h + h → Pow(a,h,A) → ModEq(p,A,n)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0004 Prime PD0008 ModEq PD0020 Pow PD0021 QRes

5 occurrences

In local proof propositions

PD0039 ScaledInversePrefix

1 occurrences

Exact expanded native-PA statement
forall p a n 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)) -> ~(a = 0) -> (exists wpo_gap_enr_target_bound. wpo_gap_enr_target_bound + S (a) = p) -> ~(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) -> 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)

Proof neighborhood

Direct theorem prerequisites

PA008T prime_scaled_inverse_prefix_exists PA00BL scaled_inverse_nonresidue_half_power_mod_predecessor

Direct theorem dependents

PA00BN bounded_euler_criterion_dichotomy

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

37 script commands · 6 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
prime scaled inverse prefix existsscaled inverse nonresidue half power mod predecessor
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 h
  5. L5
    intro A
  6. L6
    intro hpn
  7. L7
    intro hp
  8. L8
    intro ha0
  9. L9
    intro hap
  10. L10
    intro hnonresidue
02Fix variables and assumptionsL11–12

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

  1. L11
    intro heven
  2. L12
    intro hpower
03Establish hprefix_existsL13–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime scaled inverse prefix exists.

  1. L13
    have hprefix_exists : ∃ u. ∃ v. ScaledInversePrefix(p,a,n,u,v,n)Definitions: ScaledInversePrefix(p,a,n,u,v,n)Original native command in the exact edition
  2. L14
    specialize prime_scaled_inverse_prefix_exists p
  3. L15
    specialize prime_scaled_inverse_prefix_exists a
  4. L16
    specialize prime_scaled_inverse_prefix_exists n
  5. L17
    apply prime_scaled_inverse_prefix_exists
  6. L18
    exact hpn
  7. L19
    exact hp
  8. L20
    exact ha0
  9. L21
    exact hap
04Separate the logical casesL22–23

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

  1. L22
    cases hprefix_exists
  2. L23
    cases hprefix_exists_witness
05Use earlier factsL24–33

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

  1. L24
    specialize scaled_inverse_nonresidue_half_power_mod_predecessor p
  2. L25
    specialize scaled_inverse_nonresidue_half_power_mod_predecessor a
  3. L26
    specialize scaled_inverse_nonresidue_half_power_mod_predecessor n
  4. L27
    specialize scaled_inverse_nonresidue_half_power_mod_predecessor x
  5. L28
    specialize scaled_inverse_nonresidue_half_power_mod_predecessor x1
  6. L29
    specialize scaled_inverse_nonresidue_half_power_mod_predecessor h
  7. L30
    specialize scaled_inverse_nonresidue_half_power_mod_predecessor A
  8. L31
    apply scaled_inverse_nonresidue_half_power_mod_predecessor
  9. L32
    exact hpn
  10. L33
    exact hp
06Use earlier factsL34–37

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

  1. L34
    exact hnonresidue
  2. L35
    exact hprefix_exists_witness_witness
  3. L36
    exact heven
  4. L37
    exact hpower

Library-wide reading audit

Original defined command ledger · 37 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro n
  4. 0004intro h
  5. 0005intro A
  6. 0006intro hpn
  7. 0007intro hp
  8. 0008intro ha0
  9. 0009intro hap
  10. 0010intro hnonresidue
  11. 0011intro heven
  12. 0012intro hpower
  13. 0013have hprefix_exists : ∃ u. ∃ v. ScaledInversePrefix(p,a,n,u,v,n)
    Exact native replay linehave hprefix_exists : exists u v. (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)))))))
  14. 0014specialize prime_scaled_inverse_prefix_exists p
  15. 0015specialize prime_scaled_inverse_prefix_exists a
  16. 0016specialize prime_scaled_inverse_prefix_exists n
  17. 0017apply prime_scaled_inverse_prefix_exists
  18. 0018exact hpn
  19. 0019exact hp
  20. 0020exact ha0
  21. 0021exact hap
  22. 0022cases hprefix_exists
  23. 0023cases hprefix_exists_witness
  24. 0024specialize scaled_inverse_nonresidue_half_power_mod_predecessor p
  25. 0025specialize scaled_inverse_nonresidue_half_power_mod_predecessor a
  26. 0026specialize scaled_inverse_nonresidue_half_power_mod_predecessor n
  27. 0027specialize scaled_inverse_nonresidue_half_power_mod_predecessor x
  28. 0028specialize scaled_inverse_nonresidue_half_power_mod_predecessor x1
  29. 0029specialize scaled_inverse_nonresidue_half_power_mod_predecessor h
  30. 0030specialize scaled_inverse_nonresidue_half_power_mod_predecessor A
  31. 0031apply scaled_inverse_nonresidue_half_power_mod_predecessor
  32. 0032exact hpn
  33. 0033exact hp
  34. 0034exact hnonresidue
  35. 0035exact hprefix_exists_witness_witness
  36. 0036exact heven
  37. 0037exact hpower