EU000C

euler_multiplier_prefix_permutation

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

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

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_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))))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 27 exact native proof lines.

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

Proof neighborhood

Direct dependencies

EU000B euler_multiplier_prefix_bounded_injective finite_bounded_injective_surjective Stable theorem; checked-use authorized

Direct dependents

EU000D euler_multiplier_permutation_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

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.

Named ingredients (1)
euler multiplier prefix bounded injective

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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: BoundedPrefixInjectivePrefix
  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 exact 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 : (forall fp_i_eu_perm_bound. (exists fp_gap_eu_perm_bound_index. fp_gap_eu_perm_bound_index + S fp_i_eu_perm_bound = m) -> exists fp_value_eu_perm_bound. ((((exists ff_h_eu_perm_bound_entry. ff_h_eu_perm_bound_entry + S (fp_value_eu_perm_bound) = S ((S (fp_i_eu_perm_bound)) * c)) /\ exists ff_q_eu_perm_bound_entry. b = ff_q_eu_perm_bound_entry * S ((S (fp_i_eu_perm_bound)) * c) + (fp_value_eu_perm_bound))) /\ (exists fp_gap_eu_perm_bound_value. fp_gap_eu_perm_bound_value + S fp_value_eu_perm_bound = m))) /\ (forall fp_i_eu_perm_inj fp_j_eu_perm_inj fp_value_eu_perm_inj. (exists fp_gap_eu_perm_inj_i. fp_gap_eu_perm_inj_i + S fp_i_eu_perm_inj = m) -> (exists fp_gap_eu_perm_inj_j. fp_gap_eu_perm_inj_j + S fp_j_eu_perm_inj = m) -> (((exists ff_h_eu_perm_inj_left. ff_h_eu_perm_inj_left + S (fp_value_eu_perm_inj) = S ((S (fp_i_eu_perm_inj)) * c)) /\ exists ff_q_eu_perm_inj_left. b = ff_q_eu_perm_inj_left * S ((S (fp_i_eu_perm_inj)) * c) + (fp_value_eu_perm_inj))) -> (((exists ff_h_eu_perm_inj_right. ff_h_eu_perm_inj_right + S (fp_value_eu_perm_inj) = S ((S (fp_j_eu_perm_inj)) * c)) /\ exists ff_q_eu_perm_inj_right. b = ff_q_eu_perm_inj_right * S ((S (fp_j_eu_perm_inj)) * c) + (fp_value_eu_perm_inj))) -> fp_i_eu_perm_inj = fp_j_eu_perm_inj)
  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