CD0033

prime_modular_additive_orbit_hits

An actual bounded inverse proves that every nonzero prime-field step reaches every residue from a given canonical start.

Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable

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.

Sets are complete characteristic-bit codes with actual finite cardinality witnesses. The proof constructs translations and the sumset; no finite-choice oracle, supplied cardinality conclusion, or unproved polynomial-method premise is used.

Exact theorem in conservative defined notation

∀ p. ∀ d. ∀ a. ∀ z. Prime(p) → ¬d = 0 → Lt(d,p) → Lt(a,p) → ∃ x. ModEq(p,a + x · d,z)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

Lt(a,b) · 3Prime(p) · 1ModEq(m,a,b) · 4

Actual proof prerequisites

prime_bounded_nonzero_mod_inverse · checked external prerequisitefinite_modular_additive_complementmod_eq_mul_right · checked external prerequisitemod_eq_add · checked external prerequisitemod_eq_refl · checked external prerequisitemod_eq_trans · checked external prerequisitefinite_modular_add_modulusone_mul · checked external prerequisitemul_assoc · checked external prerequisitemul_comm · checked external prerequisiteadd_assoc · checked external prerequisiteadd_comm · checked external prerequisite
Original expanded first-order statement 
forall p d a z. ((~(p = 1) /\ forall frp_prime_left_cd_orbit_prime frp_prime_right_cd_orbit_prime. p = frp_prime_left_cd_orbit_prime * frp_prime_right_cd_orbit_prime -> frp_prime_left_cd_orbit_prime = 1 \/ frp_prime_right_cd_orbit_prime = 1)) -> ~(d=0) -> (exists fms_gap_lt. fms_gap_lt + S (d) = (p)) -> (exists fms_gap_lt. fms_gap_lt + S (a) = (p)) -> exists n. (exists fms_u_mod fms_v_mod. (a+n*d) + (p) * fms_u_mod = (z) + (p) * fms_v_mod)

Complete tactic proof in conservative notation

All 91 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

91 script commands · 20 reading checkpoints · 7 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)
finite modular additive complementfinite modular add modulus
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro d
  3. L3
    intro a
  4. L4
    intro z
  5. L5
    intro hp
  6. L6
    intro hd
  7. L7
    intro hdp
  8. L8
    intro hap
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 : ∃ u. ¬u = 0 ∧ (Lt(u,p) ∧ ModEq(p,d · u,1))Definitions: Lt(u,p)ModEq(p,d · u,1)Original native command in the exact edition
  2. L10
    specialize prime_bounded_nonzero_mod_inverse p
  3. L11
    specialize prime_bounded_nonzero_mod_inverse d
  4. L12
    apply prime_bounded_nonzero_mod_inverse
  5. L13
    exact hp
  6. L14
    exact hd
  7. L15
    exact hdp
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 hcompL19–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite modular additive complement.

  1. L19
    have hcomp : exists v. a+v=p
  2. L20
    specialize finite_modular_additive_complement p
  3. L21
    specialize finite_modular_additive_complement a
  4. L22
    apply finite_modular_additive_complement
  5. L23
    exact hap
05Separate the logical casesL24–24

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

  1. L24
    cases hcomp
06Construct an explicit witnessL25–25

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

  1. L25
    exists (z+x1)*x
07Establish hproductL26–26

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

  1. L26
    have hproduct : ModEq(p,(z + x1) · x · d,z + x1)Definitions: ModEq(p,(z + x1) · x · d,z + x1)Original native command in the exact edition
08Establish hscaledL27–33

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

  1. L27
    have hscaled : ModEq(p,d · x · (z + x1),1 · (z + x1))Definitions: ModEq(p,d · x · (z + x1),1 · (z + x1))Original native command in the exact edition
  2. L28
    specialize mod_eq_mul_right p
  3. L29
    specialize mod_eq_mul_right d*x
  4. L30
    specialize mod_eq_mul_right 1
  5. L31
    specialize mod_eq_mul_right z+x1
  6. L32
    apply mod_eq_mul_right
  7. L33
    exact hinv_witness_right_right
09Establish honeL34–37

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

  1. L34
    have hone : 1*(z+x1)=z+x1
  2. L35
    specialize one_mul z+x1
  3. L36
    apply one_mul
  4. L37
    rewrite hone at hscaled
10Establish heL38–47

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

  1. L38
    have he : ((z+x1)*x)*d=(d*x)*(z+x1)
  2. L39
    trans (z+x1)*(x*d)
  3. L40
    specialize mul_assoc z+x1
  4. L41
    specialize mul_assoc x
  5. L42
    specialize mul_assoc d
  6. L43
    apply mul_assoc
  7. L44
    trans (z+x1)*(d*x)
  8. L45
    congr
  9. L46
    refl
  10. L47
    specialize mul_comm x
11Use earlier factsL48–52

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

  1. L48
    specialize mul_comm d
  2. L49
    apply mul_comm
  3. L50
    specialize mul_comm z+x1
  4. L51
    specialize mul_comm d*x
  5. L52
    apply mul_comm
12Calculate and transport equalitiesL53–53

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

  1. L53
    rewrite he
13Use earlier factsL54–63

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

  1. L54
    exact hscaled
  2. L55
    specialize mod_eq_trans p
  3. L56
    specialize mod_eq_trans a+((z+x1)*x)*d
  4. L57
    specialize mod_eq_trans a+(z+x1)
  5. L58
    specialize mod_eq_trans z
  6. L59
    apply mod_eq_trans
  7. L60
    specialize mod_eq_add p
  8. L61
    specialize mod_eq_add a
  9. L62
    specialize mod_eq_add a
  10. L63
    specialize mod_eq_add ((z+x1)*x)*d
14Use earlier factsL64–69

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

  1. L64
    specialize mod_eq_add z+x1
  2. L65
    apply mod_eq_add
  3. L66
    specialize mod_eq_refl p
  4. L67
    specialize mod_eq_refl a
  5. L68
    apply mod_eq_refl
  6. L69
    exact hproduct
15Establish heL70–79

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

  1. L70
    have he : a+(z+x1)=z+(a+x1)
  2. L71
    trans (a+z)+x1
  3. L72
    symm
  4. L73
    specialize add_assoc a
  5. L74
    specialize add_assoc z
  6. L75
    specialize add_assoc x1
  7. L76
    apply add_assoc
  8. L77
    trans (z+a)+x1
  9. L78
    congr
  10. L79
    specialize add_comm a
16Use earlier factsL80–81

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

  1. L80
    specialize add_comm z
  2. L81
    apply add_comm
17Calculate and transport equalitiesL82–82

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

  1. L82
    refl
18Use earlier factsL83–86

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

  1. L83
    specialize add_assoc z
  2. L84
    specialize add_assoc a
  3. L85
    specialize add_assoc x1
  4. L86
    apply add_assoc
19Calculate and transport equalitiesL87–88

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

  1. L87
    rewrite he
  2. L88
    rewrite hcomp_witness
20Use earlier factsL89–91

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

  1. L89
    specialize finite_modular_add_modulus p
  2. L90
    specialize finite_modular_add_modulus z
  3. L91
    apply finite_modular_add_modulus

Library-wide reading audit

Original defined command ledger · 91 lines
  1. 0001intro p
  2. 0002intro d
  3. 0003intro a
  4. 0004intro z
  5. 0005intro hp
  6. 0006intro hd
  7. 0007intro hdp
  8. 0008intro hap
  9. 0009have hinv : ∃ u. ¬u = 0 ∧ (Lt(u,p) ∧ ModEq(p,d · u,1))
  10. 0010specialize prime_bounded_nonzero_mod_inverse p
  11. 0011specialize prime_bounded_nonzero_mod_inverse d
  12. 0012apply prime_bounded_nonzero_mod_inverse
  13. 0013exact hp
  14. 0014exact hd
  15. 0015exact hdp
  16. 0016cases hinv
  17. 0017cases hinv_witness
  18. 0018cases hinv_witness_right
  19. 0019have hcomp : exists v. a+v=p
  20. 0020specialize finite_modular_additive_complement p
  21. 0021specialize finite_modular_additive_complement a
  22. 0022apply finite_modular_additive_complement
  23. 0023exact hap
  24. 0024cases hcomp
  25. 0025exists (z+x1)*x
  26. 0026have hproduct : ModEq(p,(z + x1) · x · d,z + x1)
  27. 0027have hscaled : ModEq(p,d · x · (z + x1),1 · (z + x1))
  28. 0028specialize mod_eq_mul_right p
  29. 0029specialize mod_eq_mul_right d*x
  30. 0030specialize mod_eq_mul_right 1
  31. 0031specialize mod_eq_mul_right z+x1
  32. 0032apply mod_eq_mul_right
  33. 0033exact hinv_witness_right_right
  34. 0034have hone : 1*(z+x1)=z+x1
  35. 0035specialize one_mul z+x1
  36. 0036apply one_mul
  37. 0037rewrite hone at hscaled
  38. 0038have he : ((z+x1)*x)*d=(d*x)*(z+x1)
  39. 0039trans (z+x1)*(x*d)
  40. 0040specialize mul_assoc z+x1
  41. 0041specialize mul_assoc x
  42. 0042specialize mul_assoc d
  43. 0043apply mul_assoc
  44. 0044trans (z+x1)*(d*x)
  45. 0045congr
  46. 0046refl
  47. 0047specialize mul_comm x
  48. 0048specialize mul_comm d
  49. 0049apply mul_comm
  50. 0050specialize mul_comm z+x1
  51. 0051specialize mul_comm d*x
  52. 0052apply mul_comm
  53. 0053rewrite he
  54. 0054exact hscaled
  55. 0055specialize mod_eq_trans p
  56. 0056specialize mod_eq_trans a+((z+x1)*x)*d
  57. 0057specialize mod_eq_trans a+(z+x1)
  58. 0058specialize mod_eq_trans z
  59. 0059apply mod_eq_trans
  60. 0060specialize mod_eq_add p
  61. 0061specialize mod_eq_add a
  62. 0062specialize mod_eq_add a
  63. 0063specialize mod_eq_add ((z+x1)*x)*d
  64. 0064specialize mod_eq_add z+x1
  65. 0065apply mod_eq_add
  66. 0066specialize mod_eq_refl p
  67. 0067specialize mod_eq_refl a
  68. 0068apply mod_eq_refl
  69. 0069exact hproduct
  70. 0070have he : a+(z+x1)=z+(a+x1)
  71. 0071trans (a+z)+x1
  72. 0072symm
  73. 0073specialize add_assoc a
  74. 0074specialize add_assoc z
  75. 0075specialize add_assoc x1
  76. 0076apply add_assoc
  77. 0077trans (z+a)+x1
  78. 0078congr
  79. 0079specialize add_comm a
  80. 0080specialize add_comm z
  81. 0081apply add_comm
  82. 0082refl
  83. 0083specialize add_assoc z
  84. 0084specialize add_assoc a
  85. 0085specialize add_assoc x1
  86. 0086apply add_assoc
  87. 0087rewrite he
  88. 0088rewrite hcomp_witness
  89. 0089specialize finite_modular_add_modulus p
  90. 0090specialize finite_modular_add_modulus z
  91. 0091apply finite_modular_add_modulus