PA005R · theorem

quadratic_residue_bounded_equiv

Stable checked-use theorem · independently closed

Every square witness has an equivalent canonical bounded root.

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. ¬p = 0 → (QRes(p,a) → BoundedQRes(p,a)) ∧ (BoundedQRes(p,a) → QRes(p,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

PD0021 QRes PD0022 BoundedQRes

4 occurrences

In local proof propositions

PD0007 DivRem PD0008 ModEq

4 occurrences

Exact expanded native-PA statement
forall p a. ~(p = 0) -> (((exists qr_x_unbounded. exists qr_u_unbounded qr_v_unbounded. qr_x_unbounded * qr_x_unbounded + p * qr_u_unbounded = a + p * qr_v_unbounded) -> (exists qr_x_bounded. (exists qr_h_bounded. qr_h_bounded + S qr_x_bounded = p) /\ exists qr_u_bounded qr_v_bounded. qr_x_bounded * qr_x_bounded + p * qr_u_bounded = a + p * qr_v_bounded)) /\ ((exists qr_x_bounded. (exists qr_h_bounded. qr_h_bounded + S qr_x_bounded = p) /\ exists qr_u_bounded qr_v_bounded. qr_x_bounded * qr_x_bounded + p * qr_u_bounded = a + p * qr_v_bounded) -> (exists qr_x_unbounded. exists qr_u_unbounded qr_v_unbounded. qr_x_unbounded * qr_x_unbounded + p * qr_u_unbounded = a + p * qr_v_unbounded)))

Proof neighborhood

Direct theorem prerequisites

PA001D division_remainder_exists PA005Q square_residue_witness PA003C remainder_decomposition_to_mod_eq PA003L mod_eq_symm PA0024 mod_eq_trans PA000H mul_comm PA0001 zero_add

Direct theorem dependents

PA005S quadratic_residue_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

64 script commands · 22 reading checkpoints · 6 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 (7)
division remainder existssquare residue witnessremainder decomposition to mod eqmod eq symmmod eq transmul commzero add
01Fix variables and assumptionsL1–3

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro hp
02Separate the logical casesL4–4

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

  1. L4
    split
03Fix variables and assumptionsL5–5

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

  1. L5
    intro hunbounded
04Separate the logical casesL6–6

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

  1. L6
    cases hunbounded
05Establish hdivisionL7–11

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

  1. L7
    have hdivision : ∃ q. ∃ r. DivRem(x,p,q,r)Definitions: DivRem(x,p,q,r)Original native command in the exact edition
  2. L8
    specialize division_remainder_exists p
  3. L9
    specialize division_remainder_exists x
  4. L10
    apply division_remainder_exists
  5. L11
    exact hp
06Separate the logical casesL12–14

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

  1. L12
    cases hdivision
  2. L13
    cases hdivision_witness
  3. L14
    cases hdivision_witness_witness
07Establish hsquareL15–24

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

  1. L15
    have hsquare : exists w. x * x = p * w + x2 * x2
  2. L16
    specialize square_residue_witness p
  3. L17
    specialize square_residue_witness x
  4. L18
    specialize square_residue_witness x1
  5. L19
    specialize square_residue_witness x2
  6. L20
    specialize square_residue_witness 0
  7. L21
    specialize square_residue_witness (x2 * x2)
  8. L22
    apply square_residue_witness
  9. L23
    exact hdivision_witness_witness_left
  10. L24
    simp
08Use earlier factsL25–25

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

  1. L25
    specialize zero_add (x2 * x2)
09Calculate and transport equalitiesL26–26

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

  1. L26
    symm
10Use earlier factsL27–27

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

  1. L27
    exact zero_add
11Separate the logical casesL28–28

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

  1. L28
    cases hsquare
12Establish hdecompL29–34

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

  1. L29
    have hdecomp : x * x = x3 * p + x2 * x2
  2. L30
    trans p * x3 + x2 * x2
  3. L31
    exact hsquare_witness
  4. L32
    congr
  5. L33
    apply mul_comm
  6. L34
    refl
13Establish hxrL35–41

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

  1. L35
    have hxr : ModEq(p,x · x,x2 · x2)Definitions: ModEq(p,x · x,x2 · x2)Original native command in the exact edition
  2. L36
    specialize remainder_decomposition_to_mod_eq p
  3. L37
    specialize remainder_decomposition_to_mod_eq (x * x)
  4. L38
    specialize remainder_decomposition_to_mod_eq x3
  5. L39
    specialize remainder_decomposition_to_mod_eq (x2 * x2)
  6. L40
    apply remainder_decomposition_to_mod_eq
  7. L41
    exact hdecomp
14Establish hrxL42–47

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

  1. L42
    have hrx : ModEq(p,x2 · x2,x · x)Definitions: ModEq(p,x2 · x2,x · x)Original native command in the exact edition
  2. L43
    specialize mod_eq_symm p
  3. L44
    specialize mod_eq_symm (x * x)
  4. L45
    specialize mod_eq_symm (x2 * x2)
  5. L46
    apply mod_eq_symm
  6. L47
    exact hxr
15Establish hraL48–55

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

  1. L48
    have hra : ModEq(p,x2 · x2,a)Definitions: ModEq(p,x2 · x2,a)Original native command in the exact edition
  2. L49
    specialize mod_eq_trans p
  3. L50
    specialize mod_eq_trans (x2 * x2)
  4. L51
    specialize mod_eq_trans (x * x)
  5. L52
    specialize mod_eq_trans a
  6. L53
    apply mod_eq_trans
  7. L54
    exact hrx
  8. L55
    exact hunbounded_witness
16Construct an explicit witnessL56–56

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

  1. L56
    exists x2
17Separate the logical casesL57–57

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

  1. L57
    split
18Use earlier factsL58–59

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

  1. L58
    exact hdivision_witness_witness_right
  2. L59
    exact hra
19Fix variables and assumptionsL60–60

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

  1. L60
    intro hbounded
20Separate the logical casesL61–62

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

  1. L61
    cases hbounded
  2. L62
    cases hbounded_witness
21Construct an explicit witnessL63–63

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

  1. L63
    exists x
22Use earlier factsL64–64

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

  1. L64
    exact hbounded_witness_right

Library-wide reading audit

Original defined command ledger · 64 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro hp
  4. 0004split
  5. 0005intro hunbounded
  6. 0006cases hunbounded
  7. 0007have hdivision : ∃ q. ∃ r. DivRem(x,p,q,r)
    Exact native replay linehave hdivision : exists q r. x = p * q + r /\ exists h. h + S r = p
  8. 0008specialize division_remainder_exists p
  9. 0009specialize division_remainder_exists x
  10. 0010apply division_remainder_exists
  11. 0011exact hp
  12. 0012cases hdivision
  13. 0013cases hdivision_witness
  14. 0014cases hdivision_witness_witness
  15. 0015have hsquare : exists w. x * x = p * w + x2 * x2
  16. 0016specialize square_residue_witness p
  17. 0017specialize square_residue_witness x
  18. 0018specialize square_residue_witness x1
  19. 0019specialize square_residue_witness x2
  20. 0020specialize square_residue_witness 0
  21. 0021specialize square_residue_witness (x2 * x2)
  22. 0022apply square_residue_witness
  23. 0023exact hdivision_witness_witness_left
  24. 0024simp
  25. 0025specialize zero_add (x2 * x2)
  26. 0026symm
  27. 0027exact zero_add
  28. 0028cases hsquare
  29. 0029have hdecomp : x * x = x3 * p + x2 * x2
  30. 0030trans p * x3 + x2 * x2
  31. 0031exact hsquare_witness
  32. 0032congr
  33. 0033apply mul_comm
  34. 0034refl
  35. 0035have hxr : ModEq(p,x · x,x2 · x2)
    Exact native replay linehave hxr : exists u v. x * x + p * u = x2 * x2 + p * v
  36. 0036specialize remainder_decomposition_to_mod_eq p
  37. 0037specialize remainder_decomposition_to_mod_eq (x * x)
  38. 0038specialize remainder_decomposition_to_mod_eq x3
  39. 0039specialize remainder_decomposition_to_mod_eq (x2 * x2)
  40. 0040apply remainder_decomposition_to_mod_eq
  41. 0041exact hdecomp
  42. 0042have hrx : ModEq(p,x2 · x2,x · x)
    Exact native replay linehave hrx : exists u v. x2 * x2 + p * u = x * x + p * v
  43. 0043specialize mod_eq_symm p
  44. 0044specialize mod_eq_symm (x * x)
  45. 0045specialize mod_eq_symm (x2 * x2)
  46. 0046apply mod_eq_symm
  47. 0047exact hxr
  48. 0048have hra : ModEq(p,x2 · x2,a)
    Exact native replay linehave hra : exists u v. x2 * x2 + p * u = a + p * v
  49. 0049specialize mod_eq_trans p
  50. 0050specialize mod_eq_trans (x2 * x2)
  51. 0051specialize mod_eq_trans (x * x)
  52. 0052specialize mod_eq_trans a
  53. 0053apply mod_eq_trans
  54. 0054exact hrx
  55. 0055exact hunbounded_witness
  56. 0056exists x2
  57. 0057split
  58. 0058exact hdivision_witness_witness_right
  59. 0059exact hra
  60. 0060intro hbounded
  61. 0061cases hbounded
  62. 0062cases hbounded_witness
  63. 0063exists x
  64. 0064exact hbounded_witness_right