EU000B

euler_multiplier_prefix_bounded_injective

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

Coprime modular cancellation makes the genuinely constructed full multiplier map a bounded injection.

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 expanded first-order arithmetic statement

forall a m b c. ~(m=0) -> (forall eut_divisor_eu_permutation_unit. (exists eut_left_eu_permutation_unit. (a) = eut_divisor_eu_permutation_unit * eut_left_eu_permutation_unit) -> (exists eut_right_eu_permutation_unit. (m) = eut_divisor_eu_permutation_unit * eut_right_eu_permutation_unit) -> eut_divisor_eu_permutation_unit = 1) -> (forall eu_index_map_full. (exists eut_gap_eu_map_full_index. eut_gap_eu_map_full_index + S (eu_index_map_full) = (m)) -> exists eu_residue_map_full. (((exists fs_h_eu_map_full_at. fs_h_eu_map_full_at + S (eu_residue_map_full) = S ((S (eu_index_map_full)) * c)) /\ exists fs_q_eu_map_full_at. b = fs_q_eu_map_full_at * S ((S (eu_index_map_full)) * c) + (eu_residue_map_full))) /\ ((exists eut_gap_eu_map_full_bound. eut_gap_eu_map_full_bound + S (eu_residue_map_full) = (m)) /\ (exists eu_mod_left_map_full_mod eu_mod_right_map_full_mod. ((a)*eu_index_map_full) + (m) * eu_mod_left_map_full_mod = (eu_residue_map_full) + (m) * eu_mod_right_map_full_mod))) -> (forall fp_i_eu_bounded. (exists fp_gap_eu_bounded_index. fp_gap_eu_bounded_index + S fp_i_eu_bounded = m) -> exists fp_value_eu_bounded. ((((exists ff_h_eu_bounded_entry. ff_h_eu_bounded_entry + S (fp_value_eu_bounded) = S ((S (fp_i_eu_bounded)) * c)) /\ exists ff_q_eu_bounded_entry. b = ff_q_eu_bounded_entry * S ((S (fp_i_eu_bounded)) * c) + (fp_value_eu_bounded))) /\ (exists fp_gap_eu_bounded_value. fp_gap_eu_bounded_value + S fp_value_eu_bounded = m))) /\ (forall fp_i_eu_injective fp_j_eu_injective fp_value_eu_injective. (exists fp_gap_eu_injective_i. fp_gap_eu_injective_i + S fp_i_eu_injective = m) -> (exists fp_gap_eu_injective_j. fp_gap_eu_injective_j + S fp_j_eu_injective = m) -> (((exists ff_h_eu_injective_left. ff_h_eu_injective_left + S (fp_value_eu_injective) = S ((S (fp_i_eu_injective)) * c)) /\ exists ff_q_eu_injective_left. b = ff_q_eu_injective_left * S ((S (fp_i_eu_injective)) * c) + (fp_value_eu_injective))) -> (((exists ff_h_eu_injective_right. ff_h_eu_injective_right + S (fp_value_eu_injective) = S ((S (fp_j_eu_injective)) * c)) /\ exists ff_q_eu_injective_right. b = ff_q_eu_injective_right * S ((S (fp_j_eu_injective)) * c) + (fp_value_eu_injective))) -> fp_i_eu_injective = fp_j_eu_injective)

Constructive proof overview

Generated structural guide

Coprime modular cancellation makes the genuinely constructed full multiplier map a bounded injection.

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

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

Proof neighborhood

Direct dependencies

EU000A euler_multiplier_prefix_entry mod_eq_bounded_unique Stable theorem; checked-use authorized mod_eq_cancel_coprime Stable theorem; checked-use authorized mod_eq_trans Stable theorem; checked-use authorized mod_eq_symm Stable theorem; checked-use authorized

Direct dependents

EU000C euler_multiplier_prefix_permutation

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

78 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)
euler multiplier prefix entry
01Fix variables and assumptionsL1–7

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

  1. L1
    intro a
  2. L2
    intro m
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro hm
  6. L6
    intro ha
  7. L7
    intro h
02Separate the logical casesL8–8

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

  1. L8
    split
03Fix variables and assumptionsL9–10

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

  1. L9
    intro i
  2. L10
    intro hi
04Establish hpL11–14

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

  1. L11
    have hp : exists v. (((exists fs_h_eu_bounded_entry. fs_h_eu_bounded_entry + S (v) = S ((S (i)) * c)) /\ exists fs_q_eu_bounded_entry. b = fs_q_eu_bounded_entry * S ((S (i)) * c) + (v))) /\ ((exists eut_gap_eu_bounded_value. eut_gap_eu_bounded_value + S (v) = (m)) /\ (exists eu_mod_left_bounded_mod eu_mod_right_bounded_mod. (a*i) + (m) * eu_mod_left_bounded_mod = (v) + (m) * eu_mod_right_bounded_mod))
  2. L12
    specialize h (i)
  3. L13
    apply h
  4. L14
    exact hi
05Separate the logical casesL15–17

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

  1. L15
    cases hp
  2. L16
    cases hp_witness
  3. L17
    cases hp_witness_right
06Construct an explicit witnessL18–18

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

  1. L18
    exists x
07Separate the logical casesL19–19

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

  1. L19
    split
08Use earlier factsL20–21

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

  1. L20
    exact hp_witness_left
  2. L21
    exact hp_witness_right_left
09Fix variables and assumptionsL22–28

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

  1. L22
    intro i
  2. L23
    intro j
  3. L24
    intro v
  4. L25
    intro hi
  5. L26
    intro hj
  6. L27
    intro hiv
  7. L28
    intro hjv
10Establish hlL29–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euler multiplier prefix entry.

  1. L29
    have hl : (exists eut_gap_eu_left_bound. eut_gap_eu_left_bound + S (v) = (m)) /\ (exists eu_mod_left_left_mod eu_mod_right_left_mod. (a*i) + (m) * eu_mod_left_left_mod = (v) + (m) * eu_mod_right_left_mod)
  2. L30
    specialize euler_multiplier_prefix_entry (a)
  3. L31
    specialize euler_multiplier_prefix_entry (m)
  4. L32
    specialize euler_multiplier_prefix_entry (b)
  5. L33
    specialize euler_multiplier_prefix_entry (c)
  6. L34
    specialize euler_multiplier_prefix_entry (m)
  7. L35
    specialize euler_multiplier_prefix_entry (i)
  8. L36
    specialize euler_multiplier_prefix_entry (v)
  9. L37
    apply euler_multiplier_prefix_entry
  10. L38
    exact h
11Use earlier factsL39–40

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

  1. L39
    exact hi
  2. L40
    exact hiv
12Separate the logical casesL41–41

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

  1. L41
    cases hl
13Establish hrL42–51

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euler multiplier prefix entry.

  1. L42
    have hr : (exists eut_gap_eu_right_bound. eut_gap_eu_right_bound + S (v) = (m)) /\ (exists eu_mod_left_right_mod eu_mod_right_right_mod. (a*j) + (m) * eu_mod_left_right_mod = (v) + (m) * eu_mod_right_right_mod)
  2. L43
    specialize euler_multiplier_prefix_entry (a)
  3. L44
    specialize euler_multiplier_prefix_entry (m)
  4. L45
    specialize euler_multiplier_prefix_entry (b)
  5. L46
    specialize euler_multiplier_prefix_entry (c)
  6. L47
    specialize euler_multiplier_prefix_entry (m)
  7. L48
    specialize euler_multiplier_prefix_entry (j)
  8. L49
    specialize euler_multiplier_prefix_entry (v)
  9. L50
    apply euler_multiplier_prefix_entry
  10. L51
    exact h
14Use earlier factsL52–53

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

  1. L52
    exact hj
  2. L53
    exact hjv
15Separate the logical casesL54–54

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

  1. L54
    cases hr
16Use earlier factsL55–64

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

  1. L55
    specialize mod_eq_bounded_unique (m)
  2. L56
    specialize mod_eq_bounded_unique (i)
  3. L57
    specialize mod_eq_bounded_unique (j)
  4. L58
    apply mod_eq_bounded_unique
  5. L59
    exact hi
  6. L60
    exact hj
  7. L61
    specialize mod_eq_cancel_coprime (m)
  8. L62
    specialize mod_eq_cancel_coprime (a)
  9. L63
    specialize mod_eq_cancel_coprime (i)
  10. L64
    specialize mod_eq_cancel_coprime (j)
17Use earlier factsL65–74

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

  1. L65
    apply mod_eq_cancel_coprime
  2. L66
    exact hm
  3. L67
    exact ha
  4. L68
    specialize mod_eq_trans (m)
  5. L69
    specialize mod_eq_trans (a*i)
  6. L70
    specialize mod_eq_trans (v)
  7. L71
    specialize mod_eq_trans (a*j)
  8. L72
    apply mod_eq_trans
  9. L73
    exact hl_right
  10. L74
    specialize mod_eq_symm (m)
18Use earlier factsL75–78

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

  1. L75
    specialize mod_eq_symm (a*j)
  2. L76
    specialize mod_eq_symm (v)
  3. L77
    apply mod_eq_symm
  4. L78
    exact hr_right

Library-wide reading audit

Original exact command ledger · 78 lines
  1. 0001intro a
  2. 0002intro m
  3. 0003intro b
  4. 0004intro c
  5. 0005intro hm
  6. 0006intro ha
  7. 0007intro h
  8. 0008split
  9. 0009intro i
  10. 0010intro hi
  11. 0011have hp : exists v. (((exists fs_h_eu_bounded_entry. fs_h_eu_bounded_entry + S (v) = S ((S (i)) * c)) /\ exists fs_q_eu_bounded_entry. b = fs_q_eu_bounded_entry * S ((S (i)) * c) + (v))) /\ ((exists eut_gap_eu_bounded_value. eut_gap_eu_bounded_value + S (v) = (m)) /\ (exists eu_mod_left_bounded_mod eu_mod_right_bounded_mod. (a*i) + (m) * eu_mod_left_bounded_mod = (v) + (m) * eu_mod_right_bounded_mod))
  12. 0012specialize h (i)
  13. 0013apply h
  14. 0014exact hi
  15. 0015cases hp
  16. 0016cases hp_witness
  17. 0017cases hp_witness_right
  18. 0018exists x
  19. 0019split
  20. 0020exact hp_witness_left
  21. 0021exact hp_witness_right_left
  22. 0022intro i
  23. 0023intro j
  24. 0024intro v
  25. 0025intro hi
  26. 0026intro hj
  27. 0027intro hiv
  28. 0028intro hjv
  29. 0029have hl : (exists eut_gap_eu_left_bound. eut_gap_eu_left_bound + S (v) = (m)) /\ (exists eu_mod_left_left_mod eu_mod_right_left_mod. (a*i) + (m) * eu_mod_left_left_mod = (v) + (m) * eu_mod_right_left_mod)
  30. 0030specialize euler_multiplier_prefix_entry (a)
  31. 0031specialize euler_multiplier_prefix_entry (m)
  32. 0032specialize euler_multiplier_prefix_entry (b)
  33. 0033specialize euler_multiplier_prefix_entry (c)
  34. 0034specialize euler_multiplier_prefix_entry (m)
  35. 0035specialize euler_multiplier_prefix_entry (i)
  36. 0036specialize euler_multiplier_prefix_entry (v)
  37. 0037apply euler_multiplier_prefix_entry
  38. 0038exact h
  39. 0039exact hi
  40. 0040exact hiv
  41. 0041cases hl
  42. 0042have hr : (exists eut_gap_eu_right_bound. eut_gap_eu_right_bound + S (v) = (m)) /\ (exists eu_mod_left_right_mod eu_mod_right_right_mod. (a*j) + (m) * eu_mod_left_right_mod = (v) + (m) * eu_mod_right_right_mod)
  43. 0043specialize euler_multiplier_prefix_entry (a)
  44. 0044specialize euler_multiplier_prefix_entry (m)
  45. 0045specialize euler_multiplier_prefix_entry (b)
  46. 0046specialize euler_multiplier_prefix_entry (c)
  47. 0047specialize euler_multiplier_prefix_entry (m)
  48. 0048specialize euler_multiplier_prefix_entry (j)
  49. 0049specialize euler_multiplier_prefix_entry (v)
  50. 0050apply euler_multiplier_prefix_entry
  51. 0051exact h
  52. 0052exact hj
  53. 0053exact hjv
  54. 0054cases hr
  55. 0055specialize mod_eq_bounded_unique (m)
  56. 0056specialize mod_eq_bounded_unique (i)
  57. 0057specialize mod_eq_bounded_unique (j)
  58. 0058apply mod_eq_bounded_unique
  59. 0059exact hi
  60. 0060exact hj
  61. 0061specialize mod_eq_cancel_coprime (m)
  62. 0062specialize mod_eq_cancel_coprime (a)
  63. 0063specialize mod_eq_cancel_coprime (i)
  64. 0064specialize mod_eq_cancel_coprime (j)
  65. 0065apply mod_eq_cancel_coprime
  66. 0066exact hm
  67. 0067exact ha
  68. 0068specialize mod_eq_trans (m)
  69. 0069specialize mod_eq_trans (a*i)
  70. 0070specialize mod_eq_trans (v)
  71. 0071specialize mod_eq_trans (a*j)
  72. 0072apply mod_eq_trans
  73. 0073exact hl_right
  74. 0074specialize mod_eq_symm (m)
  75. 0075specialize mod_eq_symm (a*j)
  76. 0076specialize mod_eq_symm (v)
  77. 0077apply mod_eq_symm
  78. 0078exact hr_right