EU000B

euler_multiplier_prefix_bounded_injective

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

Alpha v34 checked-use · first admitted v31 · 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.

The exact G014 theorem covers m>1 and genuinely invertible a. Phi counts coprime residues independently of the conclusion. The broader coprime theorem handles m=1 by congruence, not by asserting that one is a canonical remainder. Multiplicative-order and RSA statements are not claimed.

Exact theorem in conservative defined notation

∀ a. ∀ m. ∀ b. ∀ c. ¬m = 0 → Coprime(a,m) → UnitMultiplierPrefix(a,m,b,c,m) → BoundedPrefix(b,c,m) ∧ InjectivePrefix(b,c,m)

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

Definition DAG

CanonicalModularResidue(m,a,r) · 3UnitMultiplierPrefix(a,m,b,c,l) · 1Coprime(a,b) · 1BetaAt(b,c,i,x) · 1BoundedPrefix(b,c,l) · 1InjectivePrefix(b,c,l) · 1

Actual proof prerequisites

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

Complete tactic proof in conservative notation

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

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.

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)
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 : ∃ v. BetaAt(b,c,i,v) ∧ CanonicalModularResidue(m,a · i,v)Definitions: BetaAt(b,c,i,v)CanonicalModularResidue(m,a · i,v)Original native command in the exact edition
  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 : CanonicalModularResidue(m,a · i,v)Definitions: CanonicalModularResidue(m,a · i,v)Original native command in the exact edition
  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 : CanonicalModularResidue(m,a · j,v)Definitions: CanonicalModularResidue(m,a · j,v)Original native command in the exact edition
  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 defined 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 : ∃ v. BetaAt(b,c,i,v) ∧ CanonicalModularResidue(m,a · i,v)
  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 : CanonicalModularResidue(m,a · i,v)
  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 : CanonicalModularResidue(m,a · j,v)
  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