PA005M · theorem

quadratic_residue_bounded_decidable_nonzero

Stable checked-use theorem · independently closed

A nonzero modulus admits a finite constructive residue search.

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 → BoundedQRes(p,a) ∨ ¬BoundedQRes(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

PD0022 BoundedQRes

2 occurrences

In local proof propositions

PD0001 Le PD0008 ModEq

4 occurrences

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

Proof neighborhood

Direct theorem prerequisites

PA001V nonzero_is_succ PA005L quadratic_residue_search_up_to

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

46 script commands · 25 reading checkpoints · 2 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)
nonzero is succquadratic residue search up to
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
02Establish hsL4–7

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

  1. L4
    have hs : exists B. p = S B
  2. L5
    specialize nonzero_is_succ p
  3. L6
    apply nonzero_is_succ
  4. L7
    exact hp
03Separate the logical casesL8–8

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

  1. L8
    cases hs
04Establish hsearchL9–14

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

  1. L9
    have hsearch : (∃ y. Le(y,x) ∧ ModEq(p,y · y,a)) ∨ (∀ y. Le(y,x) → ¬ModEq(p,y · y,a))Definitions: Le(y,x)ModEq(p,y · y,a)Original native command in the exact edition
  2. L10
    specialize quadratic_residue_search_up_to x
  3. L11
    specialize quadratic_residue_search_up_to p
  4. L12
    specialize quadratic_residue_search_up_to a
  5. L13
    apply quadratic_residue_search_up_to
  6. L14
    exact hp
05Separate the logical casesL15–18

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

  1. L15
    cases hsearch
  2. L16
    left
  3. L17
    cases hsearch_left
  4. L18
    cases hsearch_left_witness
06Construct an explicit witnessL19–19

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

  1. L19
    exists x1
07Separate the logical casesL20–21

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

  1. L20
    split
  2. L21
    cases hsearch_left_witness_left
08Construct an explicit witnessL22–22

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

  1. L22
    exists x2
09Calculate and transport equalitiesL23–23

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

  1. L23
    trans S (x2 + x1)
10Use earlier factsL24–24

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

  1. L24
    apply PA4
11Calculate and transport equalitiesL25–26

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

  1. L25
    trans S x
  2. L26
    congr
12Use earlier factsL27–27

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

  1. L27
    exact hsearch_left_witness_left_witness
13Calculate and transport equalitiesL28–28

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

  1. L28
    symm
14Use earlier factsL29–30

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

  1. L29
    exact hs_witness
  2. L30
    exact hsearch_left_witness_right
15Separate the logical casesL31–31

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

  1. L31
    right
16Fix variables and assumptionsL32–32

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

  1. L32
    intro hbounded
17Separate the logical casesL33–34

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

  1. L33
    cases hbounded
  2. L34
    cases hbounded_witness
18Use earlier factsL35–36

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

  1. L35
    specialize hsearch_right x1
  2. L36
    apply hsearch_right
19Separate the logical casesL37–37

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

  1. L37
    cases hbounded_witness_left
20Construct an explicit witnessL38–38

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

  1. L38
    exists x2
21Use earlier factsL39–39

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

  1. L39
    apply PA2
22Calculate and transport equalitiesL40–41

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

  1. L40
    trans x2 + S x1
  2. L41
    symm
23Use earlier factsL42–42

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

  1. L42
    apply PA4
24Calculate and transport equalitiesL43–43

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

  1. L43
    trans p
25Use earlier factsL44–46

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

  1. L44
    exact hbounded_witness_left_witness
  2. L45
    exact hs_witness
  3. L46
    exact hbounded_witness_right

Library-wide reading audit

Original defined command ledger · 46 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro hp
  4. 0004have hs : exists B. p = S B
  5. 0005specialize nonzero_is_succ p
  6. 0006apply nonzero_is_succ
  7. 0007exact hp
  8. 0008cases hs
  9. 0009have hsearch : (∃ y. Le(y,x) ∧ ModEq(p,y · y,a)) ∨ (∀ y. Le(y,x) → ¬ModEq(p,y · y,a))
    Exact native replay linehave hsearch : (exists r. (exists h. h + r = x) /\ exists u v. r * r + p * u = a + p * v) \/ (forall r. (exists h. h + r = x) -> ~(exists u v. r * r + p * u = a + p * v))
  10. 0010specialize quadratic_residue_search_up_to x
  11. 0011specialize quadratic_residue_search_up_to p
  12. 0012specialize quadratic_residue_search_up_to a
  13. 0013apply quadratic_residue_search_up_to
  14. 0014exact hp
  15. 0015cases hsearch
  16. 0016left
  17. 0017cases hsearch_left
  18. 0018cases hsearch_left_witness
  19. 0019exists x1
  20. 0020split
  21. 0021cases hsearch_left_witness_left
  22. 0022exists x2
  23. 0023trans S (x2 + x1)
  24. 0024apply PA4
  25. 0025trans S x
  26. 0026congr
  27. 0027exact hsearch_left_witness_left_witness
  28. 0028symm
  29. 0029exact hs_witness
  30. 0030exact hsearch_left_witness_right
  31. 0031right
  32. 0032intro hbounded
  33. 0033cases hbounded
  34. 0034cases hbounded_witness
  35. 0035specialize hsearch_right x1
  36. 0036apply hsearch_right
  37. 0037cases hbounded_witness_left
  38. 0038exists x2
  39. 0039apply PA2
  40. 0040trans x2 + S x1
  41. 0041symm
  42. 0042apply PA4
  43. 0043trans p
  44. 0044exact hbounded_witness_left_witness
  45. 0045exact hs_witness
  46. 0046exact hbounded_witness_right