CD001D

finite_modular_translation_indices_exists

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

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

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 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)))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 6 declared prerequisites and contains 71 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_range_exists Stable theorem; checked-use authorized beta_division_prefix_exists Alpha theorem; checked-use authorized beta_at_unique Stable theorem; checked-use authorized remainder_decomposition_to_mod_eq Stable theorem; checked-use authorized add_comm Stable theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized

Direct dependents

CD0022 finite_modular_set_pullback_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

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.

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–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 : exists b c. forall ff_i_fms_translation_range. (exists ff_lt_fms_translation_range_bound. ff_lt_fms_translation_range_bound + S ff_i_fms_translation_range = l) -> (((exists ff_h_fms_translation_range_decoded. ff_h_fms_translation_range_decoded + S (t + ff_i_fms_translation_range) = S ((S (ff_i_fms_translation_range)) * c)) /\ exists ff_q_fms_translation_range_decoded. b = ff_q_fms_translation_range_decoded * S ((S (ff_i_fms_translation_range)) * c) + (t + ff_i_fms_translation_range)))
  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: LtBetaAt
  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: LtBetaAt
  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 exact command ledger · 71 lines
  1. 0001intro p
  2. 0002intro t
  3. 0003intro l
  4. 0004intro hp
  5. 0005have hrange : exists b c. forall ff_i_fms_translation_range. (exists ff_lt_fms_translation_range_bound. ff_lt_fms_translation_range_bound + S ff_i_fms_translation_range = l) -> (((exists ff_h_fms_translation_range_decoded. ff_h_fms_translation_range_decoded + S (t + ff_i_fms_translation_range) = S ((S (ff_i_fms_translation_range)) * c)) /\ exists ff_q_fms_translation_range_decoded. b = ff_q_fms_translation_range_decoded * S ((S (ff_i_fms_translation_range)) * c) + (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 : exists qb qc rb rc. forall fdp_index_fms_translation_division. (exists gsp_lt_gap_fms_translation_division_index_bound. gsp_lt_gap_fms_translation_division_index_bound + S fdp_index_fms_translation_division = l) -> exists fdp_value_fms_translation_division fdp_quotient_fms_translation_division fdp_remainder_fms_translation_division. (((exists ff_h_fdp_fms_translation_division_source. ff_h_fdp_fms_translation_division_source + S (fdp_value_fms_translation_division) = S ((S (fdp_index_fms_translation_division)) * x1)) /\ exists ff_q_fdp_fms_translation_division_source. x = ff_q_fdp_fms_translation_division_source * S ((S (fdp_index_fms_translation_division)) * x1) + (fdp_value_fms_translation_division))) /\ ((((exists ff_h_fdp_fms_translation_division_quotient_entry. ff_h_fdp_fms_translation_division_quotient_entry + S (fdp_quotient_fms_translation_division) = S ((S (fdp_index_fms_translation_division)) * qc)) /\ exists ff_q_fdp_fms_translation_division_quotient_entry. qb = ff_q_fdp_fms_translation_division_quotient_entry * S ((S (fdp_index_fms_translation_division)) * qc) + (fdp_quotient_fms_translation_division))) /\ ((((exists ff_h_fdp_fms_translation_division_remainder_entry. ff_h_fdp_fms_translation_division_remainder_entry + S (fdp_remainder_fms_translation_division) = S ((S (fdp_index_fms_translation_division)) * rc)) /\ exists ff_q_fdp_fms_translation_division_remainder_entry. rb = ff_q_fdp_fms_translation_division_remainder_entry * S ((S (fdp_index_fms_translation_division)) * rc) + (fdp_remainder_fms_translation_division))) /\ (fdp_value_fms_translation_division = p * fdp_quotient_fms_translation_division + fdp_remainder_fms_translation_division /\ (exists gsp_lt_gap_fms_translation_division_remainder_bound. gsp_lt_gap_fms_translation_division_remainder_bound + S fdp_remainder_fms_translation_division = 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 : exists a q v. (((exists fs_h_fms_tindex_source. fs_h_fms_tindex_source + S (a) = S ((S (i)) * x1)) /\ exists fs_q_fms_tindex_source. x = fs_q_fms_tindex_source * S ((S (i)) * x1) + (a))) /\ ((((exists fs_h_fms_tindex_quotient. fs_h_fms_tindex_quotient + S (q) = S ((S (i)) * x3)) /\ exists fs_q_fms_tindex_quotient. x2 = fs_q_fms_tindex_quotient * S ((S (i)) * x3) + (q))) /\ ((((exists fs_h_fms_tindex_remainder. fs_h_fms_tindex_remainder + S (v) = S ((S (i)) * x5)) /\ exists fs_q_fms_tindex_remainder. x4 = fs_q_fms_tindex_remainder * S ((S (i)) * x5) + (v))) /\ (a=p*q+v /\ (exists fms_gap_lt. fms_gap_lt + S (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