PA005L · theorem

quadratic_residue_search_up_to

Stable checked-use theorem · independently closed

Inclusive bounded search constructively decides square congruence.

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

∀ B. ∀ p. ∀ a. ¬p = 0 → (∃ x. Le(x,B) ∧ ModEq(p,x · x,a)) ∨ (∀ x. Le(x,B) → ¬ModEq(p,x · x,a))

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

PD0001 Le PD0008 ModEq

4 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0008 ModEq

9 occurrences

Exact expanded native-PA statement
forall B p a. ~(p = 0) -> ((exists qr_x_search_yes. (exists qr_bound_search_yes. qr_bound_search_yes + qr_x_search_yes = B) /\ (exists qr_u_search_yes qr_v_search_yes. qr_x_search_yes * qr_x_search_yes + p * qr_u_search_yes = a + p * qr_v_search_yes)) \/ (forall qr_x_search_no. (exists qr_bound_search_no. qr_bound_search_no + qr_x_search_no = B) -> ~(exists qr_u_search_no qr_v_search_no. qr_x_search_no * qr_x_search_no + p * qr_u_search_no = a + p * qr_v_search_no)))

Proof neighborhood

Direct theorem prerequisites

PA005K mod_eq_decidable_nonzero PA0004 add_eq_zero_right PA000W le_eq_or_lt PA000E add_succ_left PA0001 zero_add

Direct theorem dependents

PA005M quadratic_residue_bounded_decidable_nonzero

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

91 script commands · 42 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 (5)
mod eq decidable nonzeroadd eq zero rightle eq or ltadd succ leftzero add
01Induction on BL1–4

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L1
    induction B
  2. L2
    intro p
  3. L3
    intro a
  4. L4
    intro hp
02Establish hdecL5–10

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

  1. L5
    have hdec : ModEq(p,0 · 0,a) ∨ ¬ModEq(p,0 · 0,a)Definitions: ModEq(p,0 · 0,a)Original native command in the exact edition
  2. L6
    specialize mod_eq_decidable_nonzero p
  3. L7
    specialize mod_eq_decidable_nonzero (0 * 0)
  4. L8
    specialize mod_eq_decidable_nonzero a
  5. L9
    apply mod_eq_decidable_nonzero
  6. L10
    exact hp
03Separate the logical casesL11–12

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

  1. L11
    cases hdec
  2. L12
    left
04Construct an explicit witnessL13–13

Supply the displayed value, then prove that it has the required property.

  1. L13
    exists 0
05Separate the logical casesL14–14

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

  1. L14
    split
06Construct an explicit witnessL15–15

Supply the displayed value, then prove that it has the required property.

  1. L15
    exists 0
07Calculate and transport equalitiesL16–16

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L16
    simp
08Use earlier factsL17–17

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

  1. L17
    exact hdec_left
09Separate the logical casesL18–18

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

  1. L18
    right
10Fix variables and assumptionsL19–21

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

  1. L19
    intro x
  2. L20
    intro hx
  3. L21
    intro hs
11Separate the logical casesL22–22

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

  1. L22
    cases hx
12Establish hx0L23–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.

  1. L23
    have hx0 : x = 0
  2. L24
    specialize add_eq_zero_right x1
  3. L25
    specialize add_eq_zero_right x
  4. L26
    apply add_eq_zero_right
  5. L27
    exact hx_witness
  6. L28
    apply hdec_right
  7. L29
    rewrite hx0 at hs
  8. L30
    rewrite hx0 at hs
  9. L31
    exact hs
  10. L32
    intro p
13Fix variables and assumptionsL33–34

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

  1. L33
    intro a
  2. L34
    intro hp
14Establish hprevL35–39

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

  1. L35
    have hprev : (∃ x. Le(x,B) ∧ ModEq(p,x · x,a)) ∨ (∀ x. Le(x,B) → ¬ModEq(p,x · x,a))Definitions: Le(x,B)ModEq(p,x · x,a)Original native command in the exact edition
  2. L36
    specialize IH p
  3. L37
    specialize IH a
  4. L38
    apply IH
  5. L39
    exact hp
15Separate the logical casesL40–43

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

  1. L40
    cases hprev
  2. L41
    left
  3. L42
    cases hprev_left
  4. L43
    cases hprev_left_witness
16Construct an explicit witnessL44–44

Supply the displayed value, then prove that it has the required property.

  1. L44
    exists x
17Separate the logical casesL45–46

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

  1. L45
    split
  2. L46
    cases hprev_left_witness_left
18Construct an explicit witnessL47–47

Supply the displayed value, then prove that it has the required property.

  1. L47
    exists S x1
19Calculate and transport equalitiesL48–48

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L48
    trans S (x1 + x)
20Use earlier factsL49–49

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

  1. L49
    apply add_succ_left
21Calculate and transport equalitiesL50–50

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L50
    congr
22Use earlier factsL51–52

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

  1. L51
    exact hprev_left_witness_left_witness
  2. L52
    exact hprev_left_witness_right
23Establish hdecL53–58

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

  1. L53
    have hdec : ModEq(p,S B · S B,a) ∨ ¬ModEq(p,S B · S B,a)Definitions: ModEq(p,S B · S B,a)Original native command in the exact edition
  2. L54
    specialize mod_eq_decidable_nonzero p
  3. L55
    specialize mod_eq_decidable_nonzero ((S B) * (S B))
  4. L56
    specialize mod_eq_decidable_nonzero a
  5. L57
    apply mod_eq_decidable_nonzero
  6. L58
    exact hp
24Separate the logical casesL59–60

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

  1. L59
    cases hdec
  2. L60
    left
25Construct an explicit witnessL61–61

Supply the displayed value, then prove that it has the required property.

  1. L61
    exists S B
26Separate the logical casesL62–62

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

  1. L62
    split
27Construct an explicit witnessL63–63

Supply the displayed value, then prove that it has the required property.

  1. L63
    exists 0
28Calculate and transport equalitiesL64–65

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L64
    simp
  2. L65
    congr
29Use earlier factsL66–68

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

  1. L66
    specialize zero_add B
  2. L67
    exact zero_add
  3. L68
    exact hdec_left
30Separate the logical casesL69–69

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

  1. L69
    right
31Fix variables and assumptionsL70–72

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

  1. L70
    intro x
  2. L71
    intro hx
  3. L72
    intro hs
32Use earlier factsL73–74

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

  1. L73
    specialize le_eq_or_lt x
  2. L74
    specialize le_eq_or_lt (S B)
33Establish hcasesL75–77

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L75
    have hcases : x = S B ∨ Lt(x,S B)Definitions: Lt(x,S B)Original native command in the exact edition
  2. L76
    apply le_eq_or_lt
  3. L77
    exact hx
34Separate the logical casesL78–78

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

  1. L78
    cases hcases
35Use earlier factsL79–79

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

  1. L79
    apply hdec_right
36Calculate and transport equalitiesL80–81

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L80
    rewrite hcases_left at hs
  2. L81
    rewrite hcases_left at hs
37Use earlier factsL82–83

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

  1. L82
    exact hs
  2. L83
    apply hprev_right
38Separate the logical casesL84–84

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

  1. L84
    cases hcases_right
39Construct an explicit witnessL85–85

Supply the displayed value, then prove that it has the required property.

  1. L85
    exists x1
40Use earlier factsL86–86

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

  1. L86
    apply PA2
41Calculate and transport equalitiesL87–88

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L87
    trans x1 + S x
  2. L88
    symm
42Use earlier factsL89–91

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

  1. L89
    apply PA4
  2. L90
    exact hcases_right_witness
  3. L91
    exact hs

Library-wide reading audit

Original defined command ledger · 91 lines
  1. 0001induction B
  2. 0002intro p
  3. 0003intro a
  4. 0004intro hp
  5. 0005have hdec : ModEq(p,0 · 0,a) ∨ ¬ModEq(p,0 · 0,a)
    Exact native replay linehave hdec : (exists u v. 0 * 0 + p * u = a + p * v) \/ ~(exists u v. 0 * 0 + p * u = a + p * v)
  6. 0006specialize mod_eq_decidable_nonzero p
  7. 0007specialize mod_eq_decidable_nonzero (0 * 0)
  8. 0008specialize mod_eq_decidable_nonzero a
  9. 0009apply mod_eq_decidable_nonzero
  10. 0010exact hp
  11. 0011cases hdec
  12. 0012left
  13. 0013exists 0
  14. 0014split
  15. 0015exists 0
  16. 0016simp
  17. 0017exact hdec_left
  18. 0018right
  19. 0019intro x
  20. 0020intro hx
  21. 0021intro hs
  22. 0022cases hx
  23. 0023have hx0 : x = 0
  24. 0024specialize add_eq_zero_right x1
  25. 0025specialize add_eq_zero_right x
  26. 0026apply add_eq_zero_right
  27. 0027exact hx_witness
  28. 0028apply hdec_right
  29. 0029rewrite hx0 at hs
  30. 0030rewrite hx0 at hs
  31. 0031exact hs
  32. 0032intro p
  33. 0033intro a
  34. 0034intro hp
  35. 0035have hprev : (∃ x. Le(x,B) ∧ ModEq(p,x · x,a)) ∨ (∀ x. Le(x,B) → ¬ModEq(p,x · x,a))
    Exact native replay linehave hprev : (exists x. (exists h. h + x = B) /\ exists u v. x * x + p * u = a + p * v) \/ (forall x. (exists h. h + x = B) -> ~(exists u v. x * x + p * u = a + p * v))
  36. 0036specialize IH p
  37. 0037specialize IH a
  38. 0038apply IH
  39. 0039exact hp
  40. 0040cases hprev
  41. 0041left
  42. 0042cases hprev_left
  43. 0043cases hprev_left_witness
  44. 0044exists x
  45. 0045split
  46. 0046cases hprev_left_witness_left
  47. 0047exists S x1
  48. 0048trans S (x1 + x)
  49. 0049apply add_succ_left
  50. 0050congr
  51. 0051exact hprev_left_witness_left_witness
  52. 0052exact hprev_left_witness_right
  53. 0053have hdec : ModEq(p,S B · S B,a) ∨ ¬ModEq(p,S B · S B,a)
    Exact native replay linehave hdec : (exists u v. (S B) * (S B) + p * u = a + p * v) \/ ~(exists u v. (S B) * (S B) + p * u = a + p * v)
  54. 0054specialize mod_eq_decidable_nonzero p
  55. 0055specialize mod_eq_decidable_nonzero ((S B) * (S B))
  56. 0056specialize mod_eq_decidable_nonzero a
  57. 0057apply mod_eq_decidable_nonzero
  58. 0058exact hp
  59. 0059cases hdec
  60. 0060left
  61. 0061exists S B
  62. 0062split
  63. 0063exists 0
  64. 0064simp
  65. 0065congr
  66. 0066specialize zero_add B
  67. 0067exact zero_add
  68. 0068exact hdec_left
  69. 0069right
  70. 0070intro x
  71. 0071intro hx
  72. 0072intro hs
  73. 0073specialize le_eq_or_lt x
  74. 0074specialize le_eq_or_lt (S B)
  75. 0075have hcases : x = S B ∨ Lt(x,S B)
    Exact native replay linehave hcases : x = S B \/ exists k. k + S x = S B
  76. 0076apply le_eq_or_lt
  77. 0077exact hx
  78. 0078cases hcases
  79. 0079apply hdec_right
  80. 0080rewrite hcases_left at hs
  81. 0081rewrite hcases_left at hs
  82. 0082exact hs
  83. 0083apply hprev_right
  84. 0084cases hcases_right
  85. 0085exists x1
  86. 0086apply PA2
  87. 0087trans x1 + S x
  88. 0088symm
  89. 0089apply PA4
  90. 0090exact hcases_right_witness
  91. 0091exact hs