CD001D

finite_modular_translation_indices_exists

Construct actual canonical modular-translation indices by a range code and genuine quotient/remainder recoding.

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. ∀ t. ∀ l. ¬p = 0 → ∃ x. ∃ y. ∀ z. Lt(z,l) → ∃ n. BetaAt(x,y,z,n) ∧ (Lt(n,p) ∧ ModEq(p,z + t,n))

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

Definition DAG

Lt(a,b) · 6ModEq(m,a,b) · 1BetaAt(b,c,i,x) · 8

Actual proof prerequisites

beta_range_exists · checked external prerequisitebeta_division_prefix_exists · checked external prerequisitebeta_at_unique · checked external prerequisiteremainder_decomposition_to_mod_eq · checked external prerequisiteadd_comm · checked external prerequisitemul_comm · checked external prerequisite
Original expanded first-order statement 
forall p t l. ~(p=0) -> exists r s. (forall fms_i_indices. (exists fms_gap_indices. fms_gap_indices + S (fms_i_indices) = (l)) -> exists fms_j_indices. (((exists fs_h_fms_indices_entry. fs_h_fms_indices_entry + S (fms_j_indices) = S ((S (fms_i_indices)) * s)) /\ exists fs_q_fms_indices_entry. r = fs_q_fms_indices_entry * S ((S (fms_i_indices)) * s) + (fms_j_indices))) /\ ((exists fms_gap_indices_bound. fms_gap_indices_bound + S (fms_j_indices) = (p)) /\ (exists fms_u_indices fms_v_indices. (fms_i_indices+t) + (p) * fms_u_indices = (fms_j_indices) + (p) * fms_v_indices)))

Complete tactic proof in conservative notation

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

71 script commands · 25 reading checkpoints · 4 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.

01Fix variables and assumptionsL1–4

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

  1. L1
    intro p
  2. L2
    intro t
  3. L3
    intro l
  4. L4
    intro hp
02Establish hrangeL5–8

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

  1. L5
    have hrange : ∃ b. ∃ c. ∀ ff_i_fms_translation_range. Lt(ff_i_fms_translation_range,l) → BetaAt(b,c,ff_i_fms_translation_range,t + ff_i_fms_translation_range)Definitions: Lt(ff_i_fms_translation_range,l)BetaAt(b,c,ff_i_fms_translation_range,t + ff_i_fms_translation_range)Original native command in the exact edition
  2. L6
    specialize beta_range_exists t
  3. L7
    specialize beta_range_exists l
  4. L8
    apply beta_range_exists
03Separate the logical casesL9–10

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

  1. L9
    cases hrange
  2. L10
    cases hrange_witness
04Establish hdivisionL11–17

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

  1. L11
    have hdivision : ∃ qb. ∃ qc. ∃ rb. ∃ rc. ∀ fdp_index_fms_translation_division. Lt(fdp_index_fms_translation_division,l) → ∃ y. ∃ z. ∃ n. BetaAt(x,x1,fdp_index_fms_translation_division,y) ∧ (BetaAt(qb,qc,fdp_index_fms_translation_division,z) ∧ (BetaAt(rb,rc,fdp_index_fms_translation_division,n) ∧ (y = p · z + n ∧ Lt(n,p))))Definitions: Lt(fdp_index_fms_translation_division,l)BetaAt(x,x1,fdp_index_fms_translation_division,y)BetaAt(qb,qc,fdp_index_fms_translation_division,z)BetaAt(rb,rc,fdp_index_fms_translation_division,n)Lt(n,p)Original native command in the exact edition
  2. L12
    specialize beta_division_prefix_exists p
  3. L13
    specialize beta_division_prefix_exists x
  4. L14
    specialize beta_division_prefix_exists x1
  5. L15
    specialize beta_division_prefix_exists l
  6. L16
    apply beta_division_prefix_exists
  7. L17
    exact hp
05Separate the logical casesL18–21

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

  1. L18
    cases hdivision
  2. L19
    cases hdivision_witness
  3. L20
    cases hdivision_witness_witness
  4. L21
    cases hdivision_witness_witness_witness
06Construct an explicit witnessL22–23

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

  1. L22
    exists x4
  2. L23
    exists x5
07Fix variables and assumptionsL24–25

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

  1. L24
    intro i
  2. L25
    intro hi
08Establish hentryL26–29

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

  1. L26
    have hentry : ∃ a. ∃ q. ∃ v. BetaAt(x,x1,i,a) ∧ (BetaAt(x2,x3,i,q) ∧ (BetaAt(x4,x5,i,v) ∧ (a = p · q + v ∧ Lt(v,p))))Definitions: BetaAt(x,x1,i,a)BetaAt(x2,x3,i,q)BetaAt(x4,x5,i,v)Lt(v,p)Original native command in the exact edition
  2. L27
    specialize hdivision_witness_witness_witness_witness i
  3. L28
    apply hdivision_witness_witness_witness_witness
  4. L29
    exact hi
09Separate the logical casesL30–36

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

  1. L30
    cases hentry
  2. L31
    cases hentry_witness
  3. L32
    cases hentry_witness_witness
  4. L33
    cases hentry_witness_witness_witness
  5. L34
    cases hentry_witness_witness_witness_right
  6. L35
    cases hentry_witness_witness_witness_right_right
  7. L36
    cases hentry_witness_witness_witness_right_right_right
10Establish heL37–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L37
    have he : x6=t+i
  2. L38
    specialize beta_at_unique x
  3. L39
    specialize beta_at_unique x1
  4. L40
    specialize beta_at_unique i
  5. L41
    specialize beta_at_unique x6
  6. L42
    specialize beta_at_unique t+i
  7. L43
    apply beta_at_unique
  8. L44
    exact hentry_witness_witness_witness_left
  9. L45
    specialize hrange_witness_witness i
  10. L46
    apply hrange_witness_witness
11Use earlier factsL47–47

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

  1. L47
    exact hi
12Construct an explicit witnessL48–48

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

  1. L48
    exists x8
13Separate the logical casesL49–49

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

  1. L49
    split
14Use earlier factsL50–50

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

  1. L50
    exact hentry_witness_witness_witness_right_right_left
15Separate the logical casesL51–51

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

  1. L51
    split
16Use earlier factsL52–57

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

  1. L52
    exact hentry_witness_witness_witness_right_right_right_right
  2. L53
    specialize remainder_decomposition_to_mod_eq p
  3. L54
    specialize remainder_decomposition_to_mod_eq i+t
  4. L55
    specialize remainder_decomposition_to_mod_eq x7
  5. L56
    specialize remainder_decomposition_to_mod_eq x8
  6. L57
    apply remainder_decomposition_to_mod_eq
17Calculate and transport equalitiesL58–58

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

  1. L58
    trans t+i
18Use earlier factsL59–61

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

  1. L59
    specialize add_comm i
  2. L60
    specialize add_comm t
  3. L61
    apply add_comm
19Calculate and transport equalitiesL62–63

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

  1. L62
    trans x6
  2. L63
    symm
20Use earlier factsL64–64

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

  1. L64
    exact he
21Calculate and transport equalitiesL65–65

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

  1. L65
    trans p*x7+x8
22Use earlier factsL66–66

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

  1. L66
    exact hentry_witness_witness_witness_right_right_right_left
23Calculate and transport equalitiesL67–67

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

  1. L67
    congr
24Use earlier factsL68–70

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

  1. L68
    specialize mul_comm p
  2. L69
    specialize mul_comm x7
  3. L70
    apply mul_comm
25Calculate and transport equalitiesL71–71

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

  1. L71
    refl

Library-wide reading audit

Original defined command ledger · 71 lines
  1. 0001intro p
  2. 0002intro t
  3. 0003intro l
  4. 0004intro hp
  5. 0005have hrange : ∃ b. ∃ c. ∀ ff_i_fms_translation_range. Lt(ff_i_fms_translation_range,l) → BetaAt(b,c,ff_i_fms_translation_range,t + ff_i_fms_translation_range)
  6. 0006specialize beta_range_exists t
  7. 0007specialize beta_range_exists l
  8. 0008apply beta_range_exists
  9. 0009cases hrange
  10. 0010cases hrange_witness
  11. 0011have hdivision : ∃ qb. ∃ qc. ∃ rb. ∃ rc. ∀ fdp_index_fms_translation_division. Lt(fdp_index_fms_translation_division,l) → ∃ y. ∃ z. ∃ n. BetaAt(x,x1,fdp_index_fms_translation_division,y) ∧ (BetaAt(qb,qc,fdp_index_fms_translation_division,z) ∧ (BetaAt(rb,rc,fdp_index_fms_translation_division,n) ∧ (y = p · z + n ∧ Lt(n,p))))
  12. 0012specialize beta_division_prefix_exists p
  13. 0013specialize beta_division_prefix_exists x
  14. 0014specialize beta_division_prefix_exists x1
  15. 0015specialize beta_division_prefix_exists l
  16. 0016apply beta_division_prefix_exists
  17. 0017exact hp
  18. 0018cases hdivision
  19. 0019cases hdivision_witness
  20. 0020cases hdivision_witness_witness
  21. 0021cases hdivision_witness_witness_witness
  22. 0022exists x4
  23. 0023exists x5
  24. 0024intro i
  25. 0025intro hi
  26. 0026have hentry : ∃ a. ∃ q. ∃ v. BetaAt(x,x1,i,a) ∧ (BetaAt(x2,x3,i,q) ∧ (BetaAt(x4,x5,i,v) ∧ (a = p · q + v ∧ Lt(v,p))))
  27. 0027specialize hdivision_witness_witness_witness_witness i
  28. 0028apply hdivision_witness_witness_witness_witness
  29. 0029exact hi
  30. 0030cases hentry
  31. 0031cases hentry_witness
  32. 0032cases hentry_witness_witness
  33. 0033cases hentry_witness_witness_witness
  34. 0034cases hentry_witness_witness_witness_right
  35. 0035cases hentry_witness_witness_witness_right_right
  36. 0036cases hentry_witness_witness_witness_right_right_right
  37. 0037have he : x6=t+i
  38. 0038specialize beta_at_unique x
  39. 0039specialize beta_at_unique x1
  40. 0040specialize beta_at_unique i
  41. 0041specialize beta_at_unique x6
  42. 0042specialize beta_at_unique t+i
  43. 0043apply beta_at_unique
  44. 0044exact hentry_witness_witness_witness_left
  45. 0045specialize hrange_witness_witness i
  46. 0046apply hrange_witness_witness
  47. 0047exact hi
  48. 0048exists x8
  49. 0049split
  50. 0050exact hentry_witness_witness_witness_right_right_left
  51. 0051split
  52. 0052exact hentry_witness_witness_witness_right_right_right_right
  53. 0053specialize remainder_decomposition_to_mod_eq p
  54. 0054specialize remainder_decomposition_to_mod_eq i+t
  55. 0055specialize remainder_decomposition_to_mod_eq x7
  56. 0056specialize remainder_decomposition_to_mod_eq x8
  57. 0057apply remainder_decomposition_to_mod_eq
  58. 0058trans t+i
  59. 0059specialize add_comm i
  60. 0060specialize add_comm t
  61. 0061apply add_comm
  62. 0062trans x6
  63. 0063symm
  64. 0064exact he
  65. 0065trans p*x7+x8
  66. 0066exact hentry_witness_witness_witness_right_right_right_left
  67. 0067congr
  68. 0068specialize mul_comm p
  69. 0069specialize mul_comm x7
  70. 0070apply mul_comm
  71. 0071refl