EU000C

euler_multiplier_prefix_permutation

The multiplier map has actual bounded, injective, and surjective prefix evidence, not an assumed permutation label.

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) → PermutationPrefix(b,c,m)

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

Definition DAG

PermutationPrefix(b,c,l) · 1UnitMultiplierPrefix(a,m,b,c,l) · 1Coprime(a,b) · 1BoundedPrefix(b,c,l) · 1InjectivePrefix(b,c,l) · 1

Actual proof prerequisites

euler_multiplier_prefix_bounded_injectivefinite_bounded_injective_surjective · checked external prerequisite
Original expanded first-order statement 
forall a m b c. ~(m=0) -> (forall eut_divisor_eu_permutation_coprime. (exists eut_left_eu_permutation_coprime. (a) = eut_divisor_eu_permutation_coprime * eut_left_eu_permutation_coprime) -> (exists eut_right_eu_permutation_coprime. (m) = eut_divisor_eu_permutation_coprime * eut_right_eu_permutation_coprime) -> eut_divisor_eu_permutation_coprime = 1) -> (forall eu_index_permutation_map. (exists eut_gap_eu_permutation_map_index. eut_gap_eu_permutation_map_index + S (eu_index_permutation_map) = (m)) -> exists eu_residue_permutation_map. (((exists fs_h_eu_permutation_map_at. fs_h_eu_permutation_map_at + S (eu_residue_permutation_map) = S ((S (eu_index_permutation_map)) * c)) /\ exists fs_q_eu_permutation_map_at. b = fs_q_eu_permutation_map_at * S ((S (eu_index_permutation_map)) * c) + (eu_residue_permutation_map))) /\ ((exists eut_gap_eu_permutation_map_bound. eut_gap_eu_permutation_map_bound + S (eu_residue_permutation_map) = (m)) /\ (exists eu_mod_left_permutation_map_mod eu_mod_right_permutation_map_mod. ((a)*eu_index_permutation_map) + (m) * eu_mod_left_permutation_map_mod = (eu_residue_permutation_map) + (m) * eu_mod_right_permutation_map_mod))) -> (((forall fp_i_eu_actual_permutation_bounded. (exists fp_gap_eu_actual_permutation_bounded_index. fp_gap_eu_actual_permutation_bounded_index + S fp_i_eu_actual_permutation_bounded = m) -> exists fp_value_eu_actual_permutation_bounded. ((((exists ff_h_eu_actual_permutation_bounded_entry. ff_h_eu_actual_permutation_bounded_entry + S (fp_value_eu_actual_permutation_bounded) = S ((S (fp_i_eu_actual_permutation_bounded)) * c)) /\ exists ff_q_eu_actual_permutation_bounded_entry. b = ff_q_eu_actual_permutation_bounded_entry * S ((S (fp_i_eu_actual_permutation_bounded)) * c) + (fp_value_eu_actual_permutation_bounded))) /\ (exists fp_gap_eu_actual_permutation_bounded_value. fp_gap_eu_actual_permutation_bounded_value + S fp_value_eu_actual_permutation_bounded = m))) /\ ((forall fp_i_eu_actual_permutation_injective fp_j_eu_actual_permutation_injective fp_value_eu_actual_permutation_injective. (exists fp_gap_eu_actual_permutation_injective_i. fp_gap_eu_actual_permutation_injective_i + S fp_i_eu_actual_permutation_injective = m) -> (exists fp_gap_eu_actual_permutation_injective_j. fp_gap_eu_actual_permutation_injective_j + S fp_j_eu_actual_permutation_injective = m) -> (((exists ff_h_eu_actual_permutation_injective_left. ff_h_eu_actual_permutation_injective_left + S (fp_value_eu_actual_permutation_injective) = S ((S (fp_i_eu_actual_permutation_injective)) * c)) /\ exists ff_q_eu_actual_permutation_injective_left. b = ff_q_eu_actual_permutation_injective_left * S ((S (fp_i_eu_actual_permutation_injective)) * c) + (fp_value_eu_actual_permutation_injective))) -> (((exists ff_h_eu_actual_permutation_injective_right. ff_h_eu_actual_permutation_injective_right + S (fp_value_eu_actual_permutation_injective) = S ((S (fp_j_eu_actual_permutation_injective)) * c)) /\ exists ff_q_eu_actual_permutation_injective_right. b = ff_q_eu_actual_permutation_injective_right * S ((S (fp_j_eu_actual_permutation_injective)) * c) + (fp_value_eu_actual_permutation_injective))) -> fp_i_eu_actual_permutation_injective = fp_j_eu_actual_permutation_injective) /\ (forall fp_value_eu_actual_permutation_surjective. (exists fp_gap_eu_actual_permutation_surjective_value. fp_gap_eu_actual_permutation_surjective_value + S fp_value_eu_actual_permutation_surjective = m) -> exists fp_i_eu_actual_permutation_surjective. ((exists fp_gap_eu_actual_permutation_surjective_index. fp_gap_eu_actual_permutation_surjective_index + S fp_i_eu_actual_permutation_surjective = m) /\ (((exists ff_h_eu_actual_permutation_surjective_entry. ff_h_eu_actual_permutation_surjective_entry + S (fp_value_eu_actual_permutation_surjective) = S ((S (fp_i_eu_actual_permutation_surjective)) * c)) /\ exists ff_q_eu_actual_permutation_surjective_entry. b = ff_q_eu_actual_permutation_surjective_entry * S ((S (fp_i_eu_actual_permutation_surjective)) * c) + (fp_value_eu_actual_permutation_surjective))))))))

Complete tactic proof in conservative notation

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

27 script commands · 6 reading checkpoints · 1 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 bounded injective
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 hc
  7. L7
    intro h
02Establish hpL8–16

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

  1. L8
    have hp : BoundedPrefix(b,c,m) ∧ InjectivePrefix(b,c,m)Definitions: BoundedPrefix(b,c,m)InjectivePrefix(b,c,m)Original native command in the exact edition
  2. L9
    specialize euler_multiplier_prefix_bounded_injective (a)
  3. L10
    specialize euler_multiplier_prefix_bounded_injective (m)
  4. L11
    specialize euler_multiplier_prefix_bounded_injective (b)
  5. L12
    specialize euler_multiplier_prefix_bounded_injective (c)
  6. L13
    apply euler_multiplier_prefix_bounded_injective
  7. L14
    exact hm
  8. L15
    exact hc
  9. L16
    exact h
03Separate the logical casesL17–18

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

  1. L17
    cases hp
  2. L18
    split
04Use earlier factsL19–19

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

  1. L19
    exact hp_left
05Separate the logical casesL20–20

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

  1. L20
    split
06Use earlier factsL21–27

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

  1. L21
    exact hp_right
  2. L22
    specialize finite_bounded_injective_surjective (m)
  3. L23
    specialize finite_bounded_injective_surjective (b)
  4. L24
    specialize finite_bounded_injective_surjective (c)
  5. L25
    apply finite_bounded_injective_surjective
  6. L26
    exact hp_left
  7. L27
    exact hp_right

Library-wide reading audit

Original defined command ledger · 27 lines
  1. 0001intro a
  2. 0002intro m
  3. 0003intro b
  4. 0004intro c
  5. 0005intro hm
  6. 0006intro hc
  7. 0007intro h
  8. 0008have hp : BoundedPrefix(b,c,m) ∧ InjectivePrefix(b,c,m)
  9. 0009specialize euler_multiplier_prefix_bounded_injective (a)
  10. 0010specialize euler_multiplier_prefix_bounded_injective (m)
  11. 0011specialize euler_multiplier_prefix_bounded_injective (b)
  12. 0012specialize euler_multiplier_prefix_bounded_injective (c)
  13. 0013apply euler_multiplier_prefix_bounded_injective
  14. 0014exact hm
  15. 0015exact hc
  16. 0016exact h
  17. 0017cases hp
  18. 0018split
  19. 0019exact hp_left
  20. 0020split
  21. 0021exact hp_right
  22. 0022specialize finite_bounded_injective_surjective (m)
  23. 0023specialize finite_bounded_injective_surjective (b)
  24. 0024specialize finite_bounded_injective_surjective (c)
  25. 0025apply finite_bounded_injective_surjective
  26. 0026exact hp_left
  27. 0027exact hp_right