PA008Q

prime_scaled_inverse_exists

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

Every bounded nonzero prime residue has a bounded scaled inverse.

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.

Exact expanded PA statement

forall p a x. ((~(p = 1) /\ forall esi_prime_left_exists_prime esi_prime_right_exists_prime. p = esi_prime_left_exists_prime * esi_prime_right_exists_prime -> esi_prime_left_exists_prime = 1 \/ esi_prime_right_exists_prime = 1)) -> ~(a = 0) -> (exists esi_strict_gap_exists_target_bound. esi_strict_gap_exists_target_bound + S a = p) -> ~(x = 0) -> (exists esi_strict_gap_exists_input_bound. esi_strict_gap_exists_input_bound + S x = p) -> exists y. ((((~(x = 0) /\ (exists esi_strict_gap_exists_result_left_bound. esi_strict_gap_exists_result_left_bound + S x = p))) /\ (((~(y = 0) /\ (exists esi_strict_gap_exists_result_right_bound. esi_strict_gap_exists_result_right_bound + S y = p))) /\ (exists esi_mod_left_exists_result_mod esi_mod_right_exists_result_mod. (x * y) + p * esi_mod_left_exists_result_mod = (a) + p * esi_mod_right_exists_result_mod))))

Structural proof guide

Generated structural guide

Every bounded nonzero prime residue has a bounded scaled inverse.

Use the direct prerequisites prime_bounded_nonzero_mod_inverse, scaled_inverse_from_unit_inverse, prime_nonzero, division_remainder_exists, mul_comm, remainder_decomposition_to_mod_eq, scaled_inverse_transport_right, prime_scaled_inverse_target_nonzero as previously established PA formulas.

The proof proceeds by case analysis (6), intermediate claims (8).

Referenced ingredients

PA0063 prime_bounded_nonzero_mod_inverse PA008N scaled_inverse_from_unit_inverse PA0031 prime_nonzero PA001D division_remainder_exists PA000H mul_comm PA003C remainder_decomposition_to_mod_eq PA008O scaled_inverse_transport_right PA008P prime_scaled_inverse_target_nonzero

Proof neighborhood

Direct dependencies

PA0063 prime_bounded_nonzero_mod_inverse PA008N scaled_inverse_from_unit_inverse PA0031 prime_nonzero PA001D division_remainder_exists PA000H mul_comm PA003C remainder_decomposition_to_mod_eq PA008O scaled_inverse_transport_right PA008P prime_scaled_inverse_target_nonzero

Direct dependents

PA008R prime_scaled_inverse_prefix_extend

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

83 script commands · 17 reading checkpoints · 8 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.

Named ingredients (8)
prime bounded nonzero mod inversescaled inverse from unit inverseprime nonzerodivision remainder existsmul commremainder decomposition to mod eqscaled inverse transport rightprime scaled inverse target nonzero
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro x
  4. L4
    intro hp
  5. L5
    intro ha0
  6. L6
    intro hap
  7. L7
    intro hx0
  8. L8
    intro hxp
02Establish hinvL9–15

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

  1. L9
    have hinv : exists x1. (~(x1 = 0) /\ ((exists esi_strict_gap_exists_inverse_bound. esi_strict_gap_exists_inverse_bound + S x1 = p) /\ (exists esi_mod_left_exists_inverse_mod esi_mod_right_exists_inverse_mod. (x * x1) + p * esi_mod_left_exists_inverse_mod = (1) + p * esi_mod_right_exists_inverse_mod)))
  2. L10
    specialize prime_bounded_nonzero_mod_inverse p
  3. L11
    specialize prime_bounded_nonzero_mod_inverse x
  4. L12
    apply prime_bounded_nonzero_mod_inverse
  5. L13
    exact hp
  6. L14
    exact hx0
  7. L15
    exact hxp
03Separate the logical casesL16–18

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

  1. L16
    cases hinv
  2. L17
    cases hinv_witness
  3. L18
    cases hinv_witness_right
04Establish hrawL19–25

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

  1. L19
    have hraw : exists esi_mod_left_exists_raw esi_mod_right_exists_raw. (x * (a * x1)) + p * esi_mod_left_exists_raw = (a) + p * esi_mod_right_exists_raw
  2. L20
    specialize scaled_inverse_from_unit_inverse p
  3. L21
    specialize scaled_inverse_from_unit_inverse a
  4. L22
    specialize scaled_inverse_from_unit_inverse x
  5. L23
    specialize scaled_inverse_from_unit_inverse x1
  6. L24
    apply scaled_inverse_from_unit_inverse
  7. L25
    exact hinv_witness_right_right
05Establish hp0L26–31

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

  1. L26
    have hp0 : ~(p = 0)
  2. L27
    intro hpzero
  3. L28
    specialize prime_nonzero p
  4. L29
    apply prime_nonzero
  5. L30
    exact hp
  6. L31
    exact hpzero
06Establish hdivL32–36

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

  1. L32
    have hdiv : exists q r. a * x1 = p * q + r /\ exists h. h + S r = p
  2. L33
    specialize division_remainder_exists p
  3. L34
    specialize division_remainder_exists (a * x1)
  4. L35
    apply division_remainder_exists
  5. L36
    exact hp0
07Separate the logical casesL37–39

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

  1. L37
    cases hdiv
  2. L38
    cases hdiv_witness
  3. L39
    cases hdiv_witness_witness
08Establish hdecompL40–45

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

  1. L40
    have hdecomp : a * x1 = x2 * p + x3
  2. L41
    trans p * x2 + x3
  3. L42
    exact hdiv_witness_witness_left
  4. L43
    congr
  5. L44
    apply mul_comm
  6. L45
    refl
09Establish hreducedL46–52

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

  1. L46
    have hreduced : exists esi_mod_left_exists_reduced esi_mod_right_exists_reduced. (a * x1) + p * esi_mod_left_exists_reduced = (x3) + p * esi_mod_right_exists_reduced
  2. L47
    specialize remainder_decomposition_to_mod_eq p
  3. L48
    specialize remainder_decomposition_to_mod_eq (a * x1)
  4. L49
    specialize remainder_decomposition_to_mod_eq x2
  5. L50
    specialize remainder_decomposition_to_mod_eq x3
  6. L51
    apply remainder_decomposition_to_mod_eq
  7. L52
    exact hdecomp
10Establish hfinalL53–61

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

  1. L53
    have hfinal : exists esi_mod_left_exists_final esi_mod_right_exists_final. (x * x3) + p * esi_mod_left_exists_final = (a) + p * esi_mod_right_exists_final
  2. L54
    specialize scaled_inverse_transport_right p
  3. L55
    specialize scaled_inverse_transport_right a
  4. L56
    specialize scaled_inverse_transport_right x
  5. L57
    specialize scaled_inverse_transport_right (a * x1)
  6. L58
    specialize scaled_inverse_transport_right x3
  7. L59
    apply scaled_inverse_transport_right
  8. L60
    exact hraw
  9. L61
    exact hreduced
11Establish hy0L62–71

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

  1. L62
    have hy0 : ~(x3 = 0)
  2. L63
    specialize prime_scaled_inverse_target_nonzero p
  3. L64
    specialize prime_scaled_inverse_target_nonzero a
  4. L65
    specialize prime_scaled_inverse_target_nonzero x
  5. L66
    specialize prime_scaled_inverse_target_nonzero x3
  6. L67
    intro hx3zero
  7. L68
    apply prime_scaled_inverse_target_nonzero
  8. L69
    exact hp
  9. L70
    exact ha0
  10. L71
    exact hap
12Use earlier factsL72–73

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

  1. L72
    exact hfinal
  2. L73
    exact hx3zero
13Construct an explicit witnessL74–74

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

  1. L74
    exists x3
14Separate the logical casesL75–76

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

  1. L75
    split
  2. L76
    split
15Use earlier factsL77–78

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

  1. L77
    exact hx0
  2. L78
    exact hxp
16Separate the logical casesL79–80

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

  1. L79
    split
  2. L80
    split
17Use earlier factsL81–83

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

  1. L81
    exact hy0
  2. L82
    exact hdiv_witness_witness_right
  3. L83
    exact hfinal

Library-wide reading audit

Original exact command ledger · 83 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro x
  4. 0004intro hp
  5. 0005intro ha0
  6. 0006intro hap
  7. 0007intro hx0
  8. 0008intro hxp
  9. 0009have hinv : exists x1. (~(x1 = 0) /\ ((exists esi_strict_gap_exists_inverse_bound. esi_strict_gap_exists_inverse_bound + S x1 = p) /\ (exists esi_mod_left_exists_inverse_mod esi_mod_right_exists_inverse_mod. (x * x1) + p * esi_mod_left_exists_inverse_mod = (1) + p * esi_mod_right_exists_inverse_mod)))
  10. 0010specialize prime_bounded_nonzero_mod_inverse p
  11. 0011specialize prime_bounded_nonzero_mod_inverse x
  12. 0012apply prime_bounded_nonzero_mod_inverse
  13. 0013exact hp
  14. 0014exact hx0
  15. 0015exact hxp
  16. 0016cases hinv
  17. 0017cases hinv_witness
  18. 0018cases hinv_witness_right
  19. 0019have hraw : exists esi_mod_left_exists_raw esi_mod_right_exists_raw. (x * (a * x1)) + p * esi_mod_left_exists_raw = (a) + p * esi_mod_right_exists_raw
  20. 0020specialize scaled_inverse_from_unit_inverse p
  21. 0021specialize scaled_inverse_from_unit_inverse a
  22. 0022specialize scaled_inverse_from_unit_inverse x
  23. 0023specialize scaled_inverse_from_unit_inverse x1
  24. 0024apply scaled_inverse_from_unit_inverse
  25. 0025exact hinv_witness_right_right
  26. 0026have hp0 : ~(p = 0)
  27. 0027intro hpzero
  28. 0028specialize prime_nonzero p
  29. 0029apply prime_nonzero
  30. 0030exact hp
  31. 0031exact hpzero
  32. 0032have hdiv : exists q r. a * x1 = p * q + r /\ exists h. h + S r = p
  33. 0033specialize division_remainder_exists p
  34. 0034specialize division_remainder_exists (a * x1)
  35. 0035apply division_remainder_exists
  36. 0036exact hp0
  37. 0037cases hdiv
  38. 0038cases hdiv_witness
  39. 0039cases hdiv_witness_witness
  40. 0040have hdecomp : a * x1 = x2 * p + x3
  41. 0041trans p * x2 + x3
  42. 0042exact hdiv_witness_witness_left
  43. 0043congr
  44. 0044apply mul_comm
  45. 0045refl
  46. 0046have hreduced : exists esi_mod_left_exists_reduced esi_mod_right_exists_reduced. (a * x1) + p * esi_mod_left_exists_reduced = (x3) + p * esi_mod_right_exists_reduced
  47. 0047specialize remainder_decomposition_to_mod_eq p
  48. 0048specialize remainder_decomposition_to_mod_eq (a * x1)
  49. 0049specialize remainder_decomposition_to_mod_eq x2
  50. 0050specialize remainder_decomposition_to_mod_eq x3
  51. 0051apply remainder_decomposition_to_mod_eq
  52. 0052exact hdecomp
  53. 0053have hfinal : exists esi_mod_left_exists_final esi_mod_right_exists_final. (x * x3) + p * esi_mod_left_exists_final = (a) + p * esi_mod_right_exists_final
  54. 0054specialize scaled_inverse_transport_right p
  55. 0055specialize scaled_inverse_transport_right a
  56. 0056specialize scaled_inverse_transport_right x
  57. 0057specialize scaled_inverse_transport_right (a * x1)
  58. 0058specialize scaled_inverse_transport_right x3
  59. 0059apply scaled_inverse_transport_right
  60. 0060exact hraw
  61. 0061exact hreduced
  62. 0062have hy0 : ~(x3 = 0)
  63. 0063specialize prime_scaled_inverse_target_nonzero p
  64. 0064specialize prime_scaled_inverse_target_nonzero a
  65. 0065specialize prime_scaled_inverse_target_nonzero x
  66. 0066specialize prime_scaled_inverse_target_nonzero x3
  67. 0067intro hx3zero
  68. 0068apply prime_scaled_inverse_target_nonzero
  69. 0069exact hp
  70. 0070exact ha0
  71. 0071exact hap
  72. 0072exact hfinal
  73. 0073exact hx3zero
  74. 0074exists x3
  75. 0075split
  76. 0076split
  77. 0077exact hx0
  78. 0078exact hxp
  79. 0079split
  80. 0080split
  81. 0081exact hy0
  82. 0082exact hdiv_witness_witness_right
  83. 0083exact hfinal