CD0035

prime_modular_set_translation_boundary_exists

Every nonempty proper prime-field characteristic set has a witnessed boundary in each nonzero additive direction.

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

∀ b. ∀ c. ∀ p. ∀ d. ∀ a. ∀ z. Prime(p) → AllBits(b,c,p) → ModularSetMember(b,c,p,a) → Lt(z,p) → ¬BetaAt(b,c,z,1) → ¬d = 0 → Lt(d,p) → ∃ x. ∃ y. ModularTranslationBoundary(b,c,p,d,x,y)

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

Definition DAG

ModularSetMember(b,c,p,x) · 1ModularTranslationBoundary(b,c,p,d,a,r) · 2Lt(a,b) · 2Prime(p) · 1ModEq(m,a,b) · 1BetaAt(b,c,i,x) · 2AllBits(b,c,l) · 1

Actual proof prerequisites

prime_nonzero · checked external prerequisiteprime_modular_additive_orbit_hitsfinite_modular_orbit_member_or_boundary
Original expanded first-order statement 
forall b c p d a z. ((~(p = 1) /\ forall frp_prime_left_cd_boundary_prime frp_prime_right_cd_boundary_prime. p = frp_prime_left_cd_boundary_prime * frp_prime_right_cd_boundary_prime -> frp_prime_left_cd_boundary_prime = 1 \/ frp_prime_right_cd_boundary_prime = 1)) -> (forall ff_i_fms_bits. (exists ff_lt_fms_bits_bound. ff_lt_fms_bits_bound + S ff_i_fms_bits = (p)) -> exists ff_bit_fms_bits. ((((exists ff_h_fms_bits_decoded. ff_h_fms_bits_decoded + S (ff_bit_fms_bits) = S ((S (ff_i_fms_bits)) * (c))) /\ exists ff_q_fms_bits_decoded. (b) = ff_q_fms_bits_decoded * S ((S (ff_i_fms_bits)) * (c)) + (ff_bit_fms_bits))) /\ (ff_bit_fms_bits = 0 \/ ff_bit_fms_bits = 1))) -> (((exists fms_gap_member. fms_gap_member + S (a) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (a)) * c)) /\ exists fs_q_fms_member. b = fs_q_fms_member * S ((S (a)) * c) + (1))))) -> (exists fms_gap_lt. fms_gap_lt + S (z) = (p)) -> ~(((exists fs_h_cd_boundary_outside. fs_h_cd_boundary_outside + S (1) = S ((S (z)) * c)) /\ exists fs_q_cd_boundary_outside. b = fs_q_cd_boundary_outside * S ((S (z)) * c) + (1))) -> ~(d=0) -> (exists fms_gap_lt. fms_gap_lt + S (d) = (p)) -> (exists cd_source_boundary cd_target_boundary. ((((exists fms_gap_cd_boundary_source. fms_gap_cd_boundary_source + S (cd_source_boundary) = (p)) /\ (((exists fs_h_fms_cd_boundary_source. fs_h_fms_cd_boundary_source + S (1) = S ((S (cd_source_boundary)) * c)) /\ exists fs_q_fms_cd_boundary_source. b = fs_q_fms_cd_boundary_source * S ((S (cd_source_boundary)) * c) + (1))))) /\ ((exists fms_gap_cd_boundary_target. fms_gap_cd_boundary_target + S (cd_target_boundary) = (p)) /\ ((exists fms_u_cd_boundary_shift fms_v_cd_boundary_shift. (cd_source_boundary+d) + (p) * fms_u_cd_boundary_shift = (cd_target_boundary) + (p) * fms_v_cd_boundary_shift) /\ ~(((exists fs_h_cd_boundary_outside. fs_h_cd_boundary_outside + S (1) = S ((S (cd_target_boundary)) * c)) /\ exists fs_q_cd_boundary_outside. b = fs_q_cd_boundary_outside * S ((S (cd_target_boundary)) * c) + (1)))))))

Complete tactic proof in conservative notation

All 50 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

50 script commands · 11 reading checkpoints · 3 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)
prime modular additive orbit hitsfinite modular orbit member or boundary
01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro p
  4. L4
    intro d
  5. L5
    intro a
  6. L6
    intro z
  7. L7
    intro hp
  8. L8
    intro hbits
  9. L9
    intro hstart
  10. L10
    intro hz
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hout
  2. L12
    intro hd
  3. L13
    intro hdp
03Establish hpzeroL14–19

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

  1. L14
    have hpzero : ~(p=0)
  2. L15
    intro he
  3. L16
    specialize prime_nonzero p
  4. L17
    apply prime_nonzero
  5. L18
    exact hp
  6. L19
    exact he
04Establish horbitL20–28

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

  1. L20
    have horbit : ∃ n. ModEq(p,a + n · d,z)Definitions: ModEq(p,a + n · d,z)Original native command in the exact edition
  2. L21
    specialize prime_modular_additive_orbit_hits p
  3. L22
    specialize prime_modular_additive_orbit_hits d
  4. L23
    specialize prime_modular_additive_orbit_hits a
  5. L24
    specialize prime_modular_additive_orbit_hits z
  6. L25
    apply prime_modular_additive_orbit_hits
  7. L26
    exact hp
  8. L27
    exact hd
  9. L28
    exact hdp
05Separate the logical casesL29–29

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

  1. L29
    cases hstart
06Use earlier factsL30–30

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

  1. L30
    exact hstart_left
07Separate the logical casesL31–31

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

  1. L31
    cases horbit
08Establish hcaseL32–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite modular orbit member or boundary.

  1. L32
    have hcase : BetaAt(b,c,z,1) ∨ (∃ x. ∃ y. ModularTranslationBoundary(b,c,p,d,x,y))Definitions: BetaAt(b,c,z,1)ModularTranslationBoundary(b,c,p,d,x,y)Original native command in the exact edition
  2. L33
    specialize finite_modular_orbit_member_or_boundary b
  3. L34
    specialize finite_modular_orbit_member_or_boundary c
  4. L35
    specialize finite_modular_orbit_member_or_boundary p
  5. L36
    specialize finite_modular_orbit_member_or_boundary d
  6. L37
    specialize finite_modular_orbit_member_or_boundary a
  7. L38
    specialize finite_modular_orbit_member_or_boundary x
  8. L39
    specialize finite_modular_orbit_member_or_boundary z
  9. L40
    apply finite_modular_orbit_member_or_boundary
  10. L41
    exact hpzero
09Use earlier factsL42–45

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

  1. L42
    exact hbits
  2. L43
    exact hstart
  3. L44
    exact hz
  4. L45
    exact horbit_witness
10Separate the logical casesL46–47

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

  1. L46
    cases hcase
  2. L47
    exfalso
11Use earlier factsL48–50

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

  1. L48
    apply hout
  2. L49
    exact hcase_left
  3. L50
    exact hcase_right

Library-wide reading audit

Original defined command ledger · 50 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro p
  4. 0004intro d
  5. 0005intro a
  6. 0006intro z
  7. 0007intro hp
  8. 0008intro hbits
  9. 0009intro hstart
  10. 0010intro hz
  11. 0011intro hout
  12. 0012intro hd
  13. 0013intro hdp
  14. 0014have hpzero : ~(p=0)
  15. 0015intro he
  16. 0016specialize prime_nonzero p
  17. 0017apply prime_nonzero
  18. 0018exact hp
  19. 0019exact he
  20. 0020have horbit : ∃ n. ModEq(p,a + n · d,z)
  21. 0021specialize prime_modular_additive_orbit_hits p
  22. 0022specialize prime_modular_additive_orbit_hits d
  23. 0023specialize prime_modular_additive_orbit_hits a
  24. 0024specialize prime_modular_additive_orbit_hits z
  25. 0025apply prime_modular_additive_orbit_hits
  26. 0026exact hp
  27. 0027exact hd
  28. 0028exact hdp
  29. 0029cases hstart
  30. 0030exact hstart_left
  31. 0031cases horbit
  32. 0032have hcase : BetaAt(b,c,z,1) ∨ (∃ x. ∃ y. ModularTranslationBoundary(b,c,p,d,x,y))
  33. 0033specialize finite_modular_orbit_member_or_boundary b
  34. 0034specialize finite_modular_orbit_member_or_boundary c
  35. 0035specialize finite_modular_orbit_member_or_boundary p
  36. 0036specialize finite_modular_orbit_member_or_boundary d
  37. 0037specialize finite_modular_orbit_member_or_boundary a
  38. 0038specialize finite_modular_orbit_member_or_boundary x
  39. 0039specialize finite_modular_orbit_member_or_boundary z
  40. 0040apply finite_modular_orbit_member_or_boundary
  41. 0041exact hpzero
  42. 0042exact hbits
  43. 0043exact hstart
  44. 0044exact hz
  45. 0045exact horbit_witness
  46. 0046cases hcase
  47. 0047exfalso
  48. 0048apply hout
  49. 0049exact hcase_left
  50. 0050exact hcase_right