CD001F

finite_modular_translation_indices_permutation

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

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

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

Definition DAG

Lt(a,b) · 9ModEq(m,a,b) · 4BetaAt(b,c,i,x) · 5

Actual proof prerequisites

finite_modular_translation_index_entrymod_eq_bounded_unique · checked external prerequisitemod_eq_trans · checked external prerequisitemod_eq_symm · checked external prerequisitemod_eq_add_cancel_right · checked external prerequisite
Original expanded first-order 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)

Complete tactic proof in conservative notation

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

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.

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 (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 : ∃ v. BetaAt(r,s,i,v) ∧ (Lt(v,p) ∧ ModEq(p,i + t,v))Definitions: BetaAt(r,s,i,v)Lt(v,p)ModEq(p,i + t,v)Original native command in the exact edition
  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 : Lt(v,p) ∧ ModEq(p,i + t,v)Definitions: Lt(v,p)ModEq(p,i + t,v)Original native command in the exact edition
  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 : Lt(v,p) ∧ ModEq(p,j + t,v)Definitions: Lt(v,p)ModEq(p,j + t,v)Original native command in the exact edition
  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 defined 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 : ∃ v. BetaAt(r,s,i,v) ∧ (Lt(v,p) ∧ ModEq(p,i + t,v))
  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 : Lt(v,p) ∧ ModEq(p,i + t,v)
  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 : Lt(v,p) ∧ ModEq(p,j + t,v)
  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