EU0002

euler_multiplier_coprime_iff

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

Multiplication by a coprime multiplier preserves and reflects precisely the unit predicate used by Phi.

Exact expanded first-order arithmetic statement

forall a m i r. (forall eut_divisor_eu_multiplier_unit. (exists eut_left_eu_multiplier_unit. (a) = eut_divisor_eu_multiplier_unit * eut_left_eu_multiplier_unit) -> (exists eut_right_eu_multiplier_unit. (m) = eut_divisor_eu_multiplier_unit * eut_right_eu_multiplier_unit) -> eut_divisor_eu_multiplier_unit = 1) -> (exists eu_mod_left_multiplier_congruence eu_mod_right_multiplier_congruence. (a*i) + (m) * eu_mod_left_multiplier_congruence = (r) + (m) * eu_mod_right_multiplier_congruence) -> (((forall eut_divisor_eu_source_unit. (exists eut_left_eu_source_unit. (i) = eut_divisor_eu_source_unit * eut_left_eu_source_unit) -> (exists eut_right_eu_source_unit. (m) = eut_divisor_eu_source_unit * eut_right_eu_source_unit) -> eut_divisor_eu_source_unit = 1) -> (forall eut_divisor_eu_target_unit. (exists eut_left_eu_target_unit. (r) = eut_divisor_eu_target_unit * eut_left_eu_target_unit) -> (exists eut_right_eu_target_unit. (m) = eut_divisor_eu_target_unit * eut_right_eu_target_unit) -> eut_divisor_eu_target_unit = 1)) /\ ((forall eut_divisor_eu_target_unit_back. (exists eut_left_eu_target_unit_back. (r) = eut_divisor_eu_target_unit_back * eut_left_eu_target_unit_back) -> (exists eut_right_eu_target_unit_back. (m) = eut_divisor_eu_target_unit_back * eut_right_eu_target_unit_back) -> eut_divisor_eu_target_unit_back = 1) -> (forall eut_divisor_eu_source_unit_back. (exists eut_left_eu_source_unit_back. (i) = eut_divisor_eu_source_unit_back * eut_left_eu_source_unit_back) -> (exists eut_right_eu_source_unit_back. (m) = eut_divisor_eu_source_unit_back * eut_right_eu_source_unit_back) -> eut_divisor_eu_source_unit_back = 1)))

Constructive proof overview

Generated structural guide

Multiplication by a coprime multiplier preserves and reflects precisely the unit predicate used by Phi.

The unchanged tactic script uses 4 declared prerequisites and contains 38 exact native proof lines.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

Proof neighborhood

Direct dependencies

EU0001 euler_coprime_mod_transport coprime_mul_left Alpha theorem; checked-use authorized totient_coprime_cancel_unit_factor Alpha theorem; checked-use authorized mod_eq_symm Alpha theorem; checked-use authorized

Direct dependents

EU0018 euler_unit_factor_scaled_congruence EU0019 euler_nonunit_factor_unchanged_congruence

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. The literal dependency-closed bundle is checked by original HA and the independently compiled Lean verifier. Public delivery grants no Alpha checked-use authority or Stable membership.

Read the argument

Proof checkpoints

38 script commands · 11 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 coprime mod transport

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–6

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

  1. L1
    intro a
  2. L2
    intro m
  3. L3
    intro i
  4. L4
    intro r
  5. L5
    intro ha
  6. L6
    intro hmod
02Separate the logical casesL7–7

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

  1. L7
    split
03Fix variables and assumptionsL8–8

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

  1. L8
    intro hi
04Use earlier factsL9–18

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

  1. L9
    specialize euler_coprime_mod_transport (m)
  2. L10
    specialize euler_coprime_mod_transport (a*i)
  3. L11
    specialize euler_coprime_mod_transport (r)
  4. L12
    apply euler_coprime_mod_transport
  5. L13
    specialize coprime_mul_left (a)
  6. L14
    specialize coprime_mul_left (i)
  7. L15
    specialize coprime_mul_left (m)
  8. L16
    apply coprime_mul_left
  9. L17
    exact ha
  10. L18
    exact hi
05Use earlier factsL19–19

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

  1. L19
    exact hmod
06Fix variables and assumptionsL20–20

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

  1. L20
    intro hr
07Use earlier factsL21–23

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

  1. L21
    specialize totient_coprime_cancel_unit_factor a
  2. L22
    specialize totient_coprime_cancel_unit_factor m
  3. L23
    specialize totient_coprime_cancel_unit_factor i
08Establish hcL24–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply totient coprime cancel unit factor.

  1. L24
    have hc : (Coprime(a · i,m) → Coprime(i,m)) ∧ (Coprime(i,m) → Coprime(a · i,m))Definitions: Coprime
  2. L25
    apply totient_coprime_cancel_unit_factor
  3. L26
    exact ha
09Separate the logical casesL27–27

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

  1. L27
    cases hc
10Use earlier factsL28–37

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

  1. L28
    apply hc_left
  2. L29
    specialize euler_coprime_mod_transport (m)
  3. L30
    specialize euler_coprime_mod_transport (r)
  4. L31
    specialize euler_coprime_mod_transport (a*i)
  5. L32
    apply euler_coprime_mod_transport
  6. L33
    exact hr
  7. L34
    specialize mod_eq_symm (m)
  8. L35
    specialize mod_eq_symm (a*i)
  9. L36
    specialize mod_eq_symm (r)
  10. L37
    apply mod_eq_symm
11Use earlier factsL38–38

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

  1. L38
    exact hmod

Library-wide reading audit

Original exact command ledger · 38 lines
  1. 0001intro a
  2. 0002intro m
  3. 0003intro i
  4. 0004intro r
  5. 0005intro ha
  6. 0006intro hmod
  7. 0007split
  8. 0008intro hi
  9. 0009specialize euler_coprime_mod_transport (m)
  10. 0010specialize euler_coprime_mod_transport (a*i)
  11. 0011specialize euler_coprime_mod_transport (r)
  12. 0012apply euler_coprime_mod_transport
  13. 0013specialize coprime_mul_left (a)
  14. 0014specialize coprime_mul_left (i)
  15. 0015specialize coprime_mul_left (m)
  16. 0016apply coprime_mul_left
  17. 0017exact ha
  18. 0018exact hi
  19. 0019exact hmod
  20. 0020intro hr
  21. 0021specialize totient_coprime_cancel_unit_factor a
  22. 0022specialize totient_coprime_cancel_unit_factor m
  23. 0023specialize totient_coprime_cancel_unit_factor i
  24. 0024have hc : ((forall eut_divisor_eu_cancel_product. (exists eut_left_eu_cancel_product. (a*i) = eut_divisor_eu_cancel_product * eut_left_eu_cancel_product) -> (exists eut_right_eu_cancel_product. (m) = eut_divisor_eu_cancel_product * eut_right_eu_cancel_product) -> eut_divisor_eu_cancel_product = 1) -> (forall eut_divisor_eu_cancel_factor. (exists eut_left_eu_cancel_factor. (i) = eut_divisor_eu_cancel_factor * eut_left_eu_cancel_factor) -> (exists eut_right_eu_cancel_factor. (m) = eut_divisor_eu_cancel_factor * eut_right_eu_cancel_factor) -> eut_divisor_eu_cancel_factor = 1)) /\ ((forall eut_divisor_eu_cancel_factor_back. (exists eut_left_eu_cancel_factor_back. (i) = eut_divisor_eu_cancel_factor_back * eut_left_eu_cancel_factor_back) -> (exists eut_right_eu_cancel_factor_back. (m) = eut_divisor_eu_cancel_factor_back * eut_right_eu_cancel_factor_back) -> eut_divisor_eu_cancel_factor_back = 1) -> (forall eut_divisor_eu_cancel_product_back. (exists eut_left_eu_cancel_product_back. (a*i) = eut_divisor_eu_cancel_product_back * eut_left_eu_cancel_product_back) -> (exists eut_right_eu_cancel_product_back. (m) = eut_divisor_eu_cancel_product_back * eut_right_eu_cancel_product_back) -> eut_divisor_eu_cancel_product_back = 1))
  25. 0025apply totient_coprime_cancel_unit_factor
  26. 0026exact ha
  27. 0027cases hc
  28. 0028apply hc_left
  29. 0029specialize euler_coprime_mod_transport (m)
  30. 0030specialize euler_coprime_mod_transport (r)
  31. 0031specialize euler_coprime_mod_transport (a*i)
  32. 0032apply euler_coprime_mod_transport
  33. 0033exact hr
  34. 0034specialize mod_eq_symm (m)
  35. 0035specialize mod_eq_symm (a*i)
  36. 0036specialize mod_eq_symm (r)
  37. 0037apply mod_eq_symm
  38. 0038exact hmod