CD001F

finite_modular_translation_indices_permutation

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

Canonical modular translation is a genuinely beta-coded bounded injection and hence a finite permutation.

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 r s. (forall fms_i_indices. (exists fms_gap_indices. fms_gap_indices + S (fms_i_indices) = (p)) -> 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))) -> (forall fp_i_fms_translation_bounded. (exists fp_gap_fms_translation_bounded_index. fp_gap_fms_translation_bounded_index + S fp_i_fms_translation_bounded = p) -> exists fp_value_fms_translation_bounded. ((((exists ff_h_fms_translation_bounded_entry. ff_h_fms_translation_bounded_entry + S (fp_value_fms_translation_bounded) = S ((S (fp_i_fms_translation_bounded)) * s)) /\ exists ff_q_fms_translation_bounded_entry. r = ff_q_fms_translation_bounded_entry * S ((S (fp_i_fms_translation_bounded)) * s) + (fp_value_fms_translation_bounded))) /\ (exists fp_gap_fms_translation_bounded_value. fp_gap_fms_translation_bounded_value + S fp_value_fms_translation_bounded = p))) /\ (forall fp_i_fms_translation_injective fp_j_fms_translation_injective fp_value_fms_translation_injective. (exists fp_gap_fms_translation_injective_i. fp_gap_fms_translation_injective_i + S fp_i_fms_translation_injective = p) -> (exists fp_gap_fms_translation_injective_j. fp_gap_fms_translation_injective_j + S fp_j_fms_translation_injective = p) -> (((exists ff_h_fms_translation_injective_left. ff_h_fms_translation_injective_left + S (fp_value_fms_translation_injective) = S ((S (fp_i_fms_translation_injective)) * s)) /\ exists ff_q_fms_translation_injective_left. r = ff_q_fms_translation_injective_left * S ((S (fp_i_fms_translation_injective)) * s) + (fp_value_fms_translation_injective))) -> (((exists ff_h_fms_translation_injective_right. ff_h_fms_translation_injective_right + S (fp_value_fms_translation_injective) = S ((S (fp_j_fms_translation_injective)) * s)) /\ exists ff_q_fms_translation_injective_right. r = ff_q_fms_translation_injective_right * S ((S (fp_j_fms_translation_injective)) * s) + (fp_value_fms_translation_injective))) -> fp_i_fms_translation_injective = fp_j_fms_translation_injective)

Constructive proof overview

Generated structural guide

Canonical modular translation is a genuinely beta-coded bounded injection and hence a finite permutation.

The unchanged tactic script uses 5 declared prerequisites and contains 74 exact native proof lines.

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

Proof neighborhood

Direct dependencies

CD001E finite_modular_translation_index_entry mod_eq_bounded_unique Stable theorem; checked-use authorized mod_eq_trans Stable theorem; checked-use authorized mod_eq_symm Stable theorem; checked-use authorized mod_eq_add_cancel_right Alpha 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

74 script commands · 18 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 (1)
finite modular translation index entry
01Fix variables and assumptionsL1–5

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

  1. L1
    intro p
  2. L2
    intro t
  3. L3
    intro r
  4. L4
    intro s
  5. L5
    intro hindices
02Separate the logical casesL6–6

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

  1. L6
    split
03Fix variables and assumptionsL7–8

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

  1. L7
    intro i
  2. L8
    intro hi
04Establish hvL9–12

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

  1. L9
    have hv : exists v. (((exists fs_h_fms_permutation_index. fs_h_fms_permutation_index + S (v) = S ((S (i)) * s)) /\ exists fs_q_fms_permutation_index. r = fs_q_fms_permutation_index * S ((S (i)) * s) + (v))) /\ ((exists fms_gap_lt. fms_gap_lt + S (v) = (p)) /\ (exists fms_u_mod fms_v_mod. (i+t) + (p) * fms_u_mod = (v) + (p) * fms_v_mod))
  2. L10
    specialize hindices i
  3. L11
    apply hindices
  4. L12
    exact hi
05Separate the logical casesL13–15

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

  1. L13
    cases hv
  2. L14
    cases hv_witness
  3. L15
    cases hv_witness_right
06Construct an explicit witnessL16–16

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

  1. L16
    exists x
07Separate the logical casesL17–17

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

  1. L17
    split
08Use earlier factsL18–19

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

  1. L18
    exact hv_witness_left
  2. L19
    exact hv_witness_right_left
09Fix variables and assumptionsL20–26

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

  1. L20
    intro i
  2. L21
    intro j
  3. L22
    intro v
  4. L23
    intro hi
  5. L24
    intro hj
  6. L25
    intro hiv
  7. L26
    intro hjv
10Establish hleftL27–36

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

  1. L27
    have hleft : (exists fms_gap_lt. fms_gap_lt + S (v) = (p)) /\ (exists fms_u_mod fms_v_mod. (i+t) + (p) * fms_u_mod = (v) + (p) * fms_v_mod)
  2. L28
    specialize finite_modular_translation_index_entry p
  3. L29
    specialize finite_modular_translation_index_entry t
  4. L30
    specialize finite_modular_translation_index_entry r
  5. L31
    specialize finite_modular_translation_index_entry s
  6. L32
    specialize finite_modular_translation_index_entry p
  7. L33
    specialize finite_modular_translation_index_entry i
  8. L34
    specialize finite_modular_translation_index_entry v
  9. L35
    apply finite_modular_translation_index_entry
  10. L36
    exact hindices
11Use earlier factsL37–38

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

  1. L37
    exact hi
  2. L38
    exact hiv
12Separate the logical casesL39–39

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

  1. L39
    cases hleft
13Establish hrightL40–49

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

  1. L40
    have hright : (exists fms_gap_lt. fms_gap_lt + S (v) = (p)) /\ (exists fms_u_mod fms_v_mod. (j+t) + (p) * fms_u_mod = (v) + (p) * fms_v_mod)
  2. L41
    specialize finite_modular_translation_index_entry p
  3. L42
    specialize finite_modular_translation_index_entry t
  4. L43
    specialize finite_modular_translation_index_entry r
  5. L44
    specialize finite_modular_translation_index_entry s
  6. L45
    specialize finite_modular_translation_index_entry p
  7. L46
    specialize finite_modular_translation_index_entry j
  8. L47
    specialize finite_modular_translation_index_entry v
  9. L48
    apply finite_modular_translation_index_entry
  10. L49
    exact hindices
14Use earlier factsL50–51

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

  1. L50
    exact hj
  2. L51
    exact hjv
15Separate the logical casesL52–52

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

  1. L52
    cases hright
16Use earlier factsL53–62

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

  1. L53
    specialize mod_eq_bounded_unique p
  2. L54
    specialize mod_eq_bounded_unique i
  3. L55
    specialize mod_eq_bounded_unique j
  4. L56
    apply mod_eq_bounded_unique
  5. L57
    exact hi
  6. L58
    exact hj
  7. L59
    specialize mod_eq_add_cancel_right p
  8. L60
    specialize mod_eq_add_cancel_right i
  9. L61
    specialize mod_eq_add_cancel_right j
  10. L62
    specialize mod_eq_add_cancel_right t
17Use earlier factsL63–72

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

  1. L63
    apply mod_eq_add_cancel_right
  2. L64
    specialize mod_eq_trans p
  3. L65
    specialize mod_eq_trans i+t
  4. L66
    specialize mod_eq_trans v
  5. L67
    specialize mod_eq_trans j+t
  6. L68
    apply mod_eq_trans
  7. L69
    exact hleft_right
  8. L70
    specialize mod_eq_symm p
  9. L71
    specialize mod_eq_symm j+t
  10. L72
    specialize mod_eq_symm v
18Use earlier factsL73–74

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

  1. L73
    apply mod_eq_symm
  2. L74
    exact hright_right

Library-wide reading audit

Original exact command ledger · 74 lines
  1. 0001intro p
  2. 0002intro t
  3. 0003intro r
  4. 0004intro s
  5. 0005intro hindices
  6. 0006split
  7. 0007intro i
  8. 0008intro hi
  9. 0009have hv : exists v. (((exists fs_h_fms_permutation_index. fs_h_fms_permutation_index + S (v) = S ((S (i)) * s)) /\ exists fs_q_fms_permutation_index. r = fs_q_fms_permutation_index * S ((S (i)) * s) + (v))) /\ ((exists fms_gap_lt. fms_gap_lt + S (v) = (p)) /\ (exists fms_u_mod fms_v_mod. (i+t) + (p) * fms_u_mod = (v) + (p) * fms_v_mod))
  10. 0010specialize hindices i
  11. 0011apply hindices
  12. 0012exact hi
  13. 0013cases hv
  14. 0014cases hv_witness
  15. 0015cases hv_witness_right
  16. 0016exists x
  17. 0017split
  18. 0018exact hv_witness_left
  19. 0019exact hv_witness_right_left
  20. 0020intro i
  21. 0021intro j
  22. 0022intro v
  23. 0023intro hi
  24. 0024intro hj
  25. 0025intro hiv
  26. 0026intro hjv
  27. 0027have hleft : (exists fms_gap_lt. fms_gap_lt + S (v) = (p)) /\ (exists fms_u_mod fms_v_mod. (i+t) + (p) * fms_u_mod = (v) + (p) * fms_v_mod)
  28. 0028specialize finite_modular_translation_index_entry p
  29. 0029specialize finite_modular_translation_index_entry t
  30. 0030specialize finite_modular_translation_index_entry r
  31. 0031specialize finite_modular_translation_index_entry s
  32. 0032specialize finite_modular_translation_index_entry p
  33. 0033specialize finite_modular_translation_index_entry i
  34. 0034specialize finite_modular_translation_index_entry v
  35. 0035apply finite_modular_translation_index_entry
  36. 0036exact hindices
  37. 0037exact hi
  38. 0038exact hiv
  39. 0039cases hleft
  40. 0040have hright : (exists fms_gap_lt. fms_gap_lt + S (v) = (p)) /\ (exists fms_u_mod fms_v_mod. (j+t) + (p) * fms_u_mod = (v) + (p) * fms_v_mod)
  41. 0041specialize finite_modular_translation_index_entry p
  42. 0042specialize finite_modular_translation_index_entry t
  43. 0043specialize finite_modular_translation_index_entry r
  44. 0044specialize finite_modular_translation_index_entry s
  45. 0045specialize finite_modular_translation_index_entry p
  46. 0046specialize finite_modular_translation_index_entry j
  47. 0047specialize finite_modular_translation_index_entry v
  48. 0048apply finite_modular_translation_index_entry
  49. 0049exact hindices
  50. 0050exact hj
  51. 0051exact hjv
  52. 0052cases hright
  53. 0053specialize mod_eq_bounded_unique p
  54. 0054specialize mod_eq_bounded_unique i
  55. 0055specialize mod_eq_bounded_unique j
  56. 0056apply mod_eq_bounded_unique
  57. 0057exact hi
  58. 0058exact hj
  59. 0059specialize mod_eq_add_cancel_right p
  60. 0060specialize mod_eq_add_cancel_right i
  61. 0061specialize mod_eq_add_cancel_right j
  62. 0062specialize mod_eq_add_cancel_right t
  63. 0063apply mod_eq_add_cancel_right
  64. 0064specialize mod_eq_trans p
  65. 0065specialize mod_eq_trans i+t
  66. 0066specialize mod_eq_trans v
  67. 0067specialize mod_eq_trans j+t
  68. 0068apply mod_eq_trans
  69. 0069exact hleft_right
  70. 0070specialize mod_eq_symm p
  71. 0071specialize mod_eq_symm j+t
  72. 0072specialize mod_eq_symm v
  73. 0073apply mod_eq_symm
  74. 0074exact hright_right