PA00BN · theorem

bounded_euler_criterion_dichotomy

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

Every bounded nonzero input lands constructively in exactly the appropriate Euler endpoint.

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) → n = h + h → Pow(a,h,A) → QRes(p,a) ∧ ModEq(p,A,1) ∨ ¬QRes(p,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

7 occurrences

In local proof propositions

PD0003 Dvd PD0021 QRes

3 occurrences

Exact expanded native-PA statement
forall p a n h A. p = S n -> ((~(p = 1) /\ forall esi_prime_left_ecb_prime esi_prime_right_ecb_prime. p = esi_prime_left_ecb_prime * esi_prime_right_ecb_prime -> esi_prime_left_ecb_prime = 1 \/ esi_prime_right_ecb_prime = 1)) -> ~(a = 0) -> (exists wpo_gap_ecb_a_lt_p. wpo_gap_ecb_a_lt_p + S (a) = p) -> n = h + h -> (exists ff_b_ecb_power ff_c_ecb_power. ((forall ff_i_ecb_power_repeat. (exists ff_lt_ecb_power_repeat_bound. ff_lt_ecb_power_repeat_bound + S ff_i_ecb_power_repeat = h) -> (((exists ff_h_ecb_power_repeat_decoded. ff_h_ecb_power_repeat_decoded + S (a) = S ((S (ff_i_ecb_power_repeat)) * ff_c_ecb_power)) /\ exists ff_q_ecb_power_repeat_decoded. ff_b_ecb_power = ff_q_ecb_power_repeat_decoded * S ((S (ff_i_ecb_power_repeat)) * ff_c_ecb_power) + (a)))) /\ (exists ff_u_ecb_power_product ff_v_ecb_power_product. ((((exists ff_h_ecb_power_product_start. ff_h_ecb_power_product_start + S (1) = S ((S (0)) * ff_v_ecb_power_product)) /\ exists ff_q_ecb_power_product_start. ff_u_ecb_power_product = ff_q_ecb_power_product_start * S ((S (0)) * ff_v_ecb_power_product) + (1))) /\ ((((exists ff_h_ecb_power_product_terminal. ff_h_ecb_power_product_terminal + S (A) = S ((S (h)) * ff_v_ecb_power_product)) /\ exists ff_q_ecb_power_product_terminal. ff_u_ecb_power_product = ff_q_ecb_power_product_terminal * S ((S (h)) * ff_v_ecb_power_product) + (A))) /\ forall ff_i_ecb_power_product. (exists ff_lt_ecb_power_product_bound. ff_lt_ecb_power_product_bound + S ff_i_ecb_power_product = h) -> exists ff_p_ecb_power_product ff_r_ecb_power_product ff_s_ecb_power_product. ((((exists ff_h_ecb_power_product_factor. ff_h_ecb_power_product_factor + S (ff_p_ecb_power_product) = S ((S (ff_i_ecb_power_product)) * ff_c_ecb_power)) /\ exists ff_q_ecb_power_product_factor. ff_b_ecb_power = ff_q_ecb_power_product_factor * S ((S (ff_i_ecb_power_product)) * ff_c_ecb_power) + (ff_p_ecb_power_product))) /\ ((((exists ff_h_ecb_power_product_partial. ff_h_ecb_power_product_partial + S (ff_r_ecb_power_product) = S ((S (ff_i_ecb_power_product)) * ff_v_ecb_power_product)) /\ exists ff_q_ecb_power_product_partial. ff_u_ecb_power_product = ff_q_ecb_power_product_partial * S ((S (ff_i_ecb_power_product)) * ff_v_ecb_power_product) + (ff_r_ecb_power_product))) /\ ((((exists ff_h_ecb_power_product_successor. ff_h_ecb_power_product_successor + S (ff_s_ecb_power_product) = S ((S (S ff_i_ecb_power_product)) * ff_v_ecb_power_product)) /\ exists ff_q_ecb_power_product_successor. ff_u_ecb_power_product = ff_q_ecb_power_product_successor * S ((S (S ff_i_ecb_power_product)) * ff_v_ecb_power_product) + (ff_s_ecb_power_product))) /\ ff_s_ecb_power_product = ff_r_ecb_power_product * ff_p_ecb_power_product)))))))) -> ((((exists qr_x_ecb_qres. exists qr_u_ecb_qres qr_v_ecb_qres. qr_x_ecb_qres * qr_x_ecb_qres + p * qr_u_ecb_qres = a + p * qr_v_ecb_qres) /\ (exists wpp_mod_left_ecb_mod_one wpp_mod_right_ecb_mod_one. (A) + p * wpp_mod_left_ecb_mod_one = (1) + p * wpp_mod_right_ecb_mod_one)) \/ ((~(exists qr_x_ecb_qres. exists qr_u_ecb_qres qr_v_ecb_qres. qr_x_ecb_qres * qr_x_ecb_qres + p * qr_u_ecb_qres = a + p * qr_v_ecb_qres)) /\ (exists wpp_mod_left_ecb_mod_predecessor wpp_mod_right_ecb_mod_predecessor. (A) + p * wpp_mod_left_ecb_mod_predecessor = (n) + p * wpp_mod_right_ecb_mod_predecessor))))

Proof neighborhood

Direct theorem prerequisites

PA0031 prime_nonzero PA0089 bounded_nonzero_not_divides PA005S quadratic_residue_decidable_nonzero PA008M quadratic_residue_half_power_mod_one PA00BM quadratic_nonresidue_half_power_mod_predecessor PA000E add_succ_left PA000H mul_comm PA0001 zero_add

Direct theorem dependents

PA00BQ bounded_euler_criterion_residue_iff PA00BS bounded_euler_criterion_nonresidue_iff

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

72 script commands · 13 reading checkpoints · 5 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 (6)
prime nonzerobounded nonzero not dividesquadratic residue decidable nonzeroquadratic residue half power mod onequadratic nonresidue half power mod predecessormul comm
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 heven
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hpower
03Establish hp0L12–17

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

  1. L12
    have hp0 : ~(p = 0)
  2. L13
    intro hpzero
  3. L14
    specialize prime_nonzero p
  4. L15
    apply prime_nonzero
  5. L16
    exact hp
  6. L17
    exact hpzero
04Establish hnotdivL18–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bounded nonzero not divides.

  1. L18
    have hnotdiv : ¬Dvd(p,a)Definitions: Dvd(p,a)Original native command in the exact edition
  2. L19
    intro hdiv
  3. L20
    specialize bounded_nonzero_not_divides p
  4. L21
    specialize bounded_nonzero_not_divides a
  5. L22
    apply bounded_nonzero_not_divides
  6. L23
    exact ha0
  7. L24
    exact hap
  8. L25
    exact hdiv
05Establish hdoubleL26–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul comm.

  1. L26
    have hdouble : h + h = 2 * h
  2. L27
    trans h * 2
  3. L28
    simp [zero_add]
  4. L29
    specialize mul_comm h
  5. L30
    specialize mul_comm 2
  6. L31
    apply mul_comm
06Establish hoddL32–37

Establish this local claim before using it. It is not an additional assumption.

  1. L32
    have hodd : p = 2 * h + 1
  2. L33
    trans S n
  3. L34
    exact hpn
  4. L35
    rewrite heven
  5. L36
    rewrite hdouble
  6. L37
    simp [add_succ_left]
07Establish hdecL38–42

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply quadratic residue decidable nonzero.

  1. L38
    have hdec : QRes(p,a) ∨ ¬QRes(p,a)Definitions: QRes(p,a)Original native command in the exact edition
  2. L39
    specialize quadratic_residue_decidable_nonzero p
  3. L40
    specialize quadratic_residue_decidable_nonzero a
  4. L41
    apply quadratic_residue_decidable_nonzero
  5. L42
    exact hp0
08Separate the logical casesL43–45

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

  1. L43
    cases hdec
  2. L44
    left
  3. L45
    split
09Use earlier factsL46–55

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

  1. L46
    exact hdec_left
  2. L47
    specialize quadratic_residue_half_power_mod_one p
  3. L48
    specialize quadratic_residue_half_power_mod_one h
  4. L49
    specialize quadratic_residue_half_power_mod_one a
  5. L50
    specialize quadratic_residue_half_power_mod_one A
  6. L51
    apply quadratic_residue_half_power_mod_one
  7. L52
    exact hodd
  8. L53
    exact hp
  9. L54
    exact hnotdiv
  10. L55
    exact hdec_left
10Use earlier factsL56–56

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

  1. L56
    exact hpower
11Separate the logical casesL57–58

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

  1. L57
    right
  2. L58
    split
12Use earlier factsL59–68

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

  1. L59
    exact hdec_right
  2. L60
    specialize quadratic_nonresidue_half_power_mod_predecessor p
  3. L61
    specialize quadratic_nonresidue_half_power_mod_predecessor a
  4. L62
    specialize quadratic_nonresidue_half_power_mod_predecessor n
  5. L63
    specialize quadratic_nonresidue_half_power_mod_predecessor h
  6. L64
    specialize quadratic_nonresidue_half_power_mod_predecessor A
  7. L65
    apply quadratic_nonresidue_half_power_mod_predecessor
  8. L66
    exact hpn
  9. L67
    exact hp
  10. L68
    exact ha0
13Use earlier factsL69–72

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

  1. L69
    exact hap
  2. L70
    exact hdec_right
  3. L71
    exact heven
  4. L72
    exact hpower

Library-wide reading audit

Original defined command ledger · 72 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 heven
  11. 0011intro hpower
  12. 0012have hp0 : ~(p = 0)
  13. 0013intro hpzero
  14. 0014specialize prime_nonzero p
  15. 0015apply prime_nonzero
  16. 0016exact hp
  17. 0017exact hpzero
  18. 0018have hnotdiv : ¬Dvd(p,a)
    Exact native replay linehave hnotdiv : ~(exists frm_factor_ecb_not_divisor. a = p * frm_factor_ecb_not_divisor)
  19. 0019intro hdiv
  20. 0020specialize bounded_nonzero_not_divides p
  21. 0021specialize bounded_nonzero_not_divides a
  22. 0022apply bounded_nonzero_not_divides
  23. 0023exact ha0
  24. 0024exact hap
  25. 0025exact hdiv
  26. 0026have hdouble : h + h = 2 * h
  27. 0027trans h * 2
  28. 0028simp [zero_add]
  29. 0029specialize mul_comm h
  30. 0030specialize mul_comm 2
  31. 0031apply mul_comm
  32. 0032have hodd : p = 2 * h + 1
  33. 0033trans S n
  34. 0034exact hpn
  35. 0035rewrite heven
  36. 0036rewrite hdouble
  37. 0037simp [add_succ_left]
  38. 0038have hdec : QRes(p,a) ∨ ¬QRes(p,a)
    Exact native replay linehave hdec : (exists qr_x_ecb_qres. exists qr_u_ecb_qres qr_v_ecb_qres. qr_x_ecb_qres * qr_x_ecb_qres + p * qr_u_ecb_qres = a + p * qr_v_ecb_qres) \/ ~(exists qr_x_ecb_qres. exists qr_u_ecb_qres qr_v_ecb_qres. qr_x_ecb_qres * qr_x_ecb_qres + p * qr_u_ecb_qres = a + p * qr_v_ecb_qres)
  39. 0039specialize quadratic_residue_decidable_nonzero p
  40. 0040specialize quadratic_residue_decidable_nonzero a
  41. 0041apply quadratic_residue_decidable_nonzero
  42. 0042exact hp0
  43. 0043cases hdec
  44. 0044left
  45. 0045split
  46. 0046exact hdec_left
  47. 0047specialize quadratic_residue_half_power_mod_one p
  48. 0048specialize quadratic_residue_half_power_mod_one h
  49. 0049specialize quadratic_residue_half_power_mod_one a
  50. 0050specialize quadratic_residue_half_power_mod_one A
  51. 0051apply quadratic_residue_half_power_mod_one
  52. 0052exact hodd
  53. 0053exact hp
  54. 0054exact hnotdiv
  55. 0055exact hdec_left
  56. 0056exact hpower
  57. 0057right
  58. 0058split
  59. 0059exact hdec_right
  60. 0060specialize quadratic_nonresidue_half_power_mod_predecessor p
  61. 0061specialize quadratic_nonresidue_half_power_mod_predecessor a
  62. 0062specialize quadratic_nonresidue_half_power_mod_predecessor n
  63. 0063specialize quadratic_nonresidue_half_power_mod_predecessor h
  64. 0064specialize quadratic_nonresidue_half_power_mod_predecessor A
  65. 0065apply quadratic_nonresidue_half_power_mod_predecessor
  66. 0066exact hpn
  67. 0067exact hp
  68. 0068exact ha0
  69. 0069exact hap
  70. 0070exact hdec_right
  71. 0071exact heven
  72. 0072exact hpower