CD0035

prime_modular_set_translation_boundary_exists

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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 first-order arithmetic 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)))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 3 declared prerequisites and contains 50 exact native proof lines.

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

Proof neighborhood

Direct dependencies

prime_nonzero Stable theorem; checked-use authorized CD0033 prime_modular_additive_orbit_hits CD0034 finite_modular_orbit_member_or_boundary

Direct dependents

CD0041 prime_modular_normalized_boundary_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

Named ingredients (2)
prime modular additive orbit hitsfinite modular orbit member or boundary

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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 : exists n. exists fms_u_mod fms_v_mod. (a+n*d) + (p) * fms_u_mod = (z) + (p) * fms_v_mod
  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: ModularTranslationBoundaryBetaAt
  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 exact 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 : exists n. exists fms_u_mod fms_v_mod. (a+n*d) + (p) * fms_u_mod = (z) + (p) * fms_v_mod
  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 : (((exists fs_h_cd_boundary_final. fs_h_cd_boundary_final + S (1) = S ((S (z)) * c)) /\ exists fs_q_cd_boundary_final. b = fs_q_cd_boundary_final * S ((S (z)) * c) + (1))) \/ (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)))))))
  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