EU0001

euler_coprime_mod_transport

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

Balanced congruence transports actual common-divisor coprimality, even at modulus zero or one.

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 m a b. (forall eut_divisor_eu_transport_old. (exists eut_left_eu_transport_old. (a) = eut_divisor_eu_transport_old * eut_left_eu_transport_old) -> (exists eut_right_eu_transport_old. (m) = eut_divisor_eu_transport_old * eut_right_eu_transport_old) -> eut_divisor_eu_transport_old = 1) -> (exists eu_mod_left_transport eu_mod_right_transport. (a) + (m) * eu_mod_left_transport = (b) + (m) * eu_mod_right_transport) -> (forall eut_divisor_eu_transport_new. (exists eut_left_eu_transport_new. (b) = eut_divisor_eu_transport_new * eut_left_eu_transport_new) -> (exists eut_right_eu_transport_new. (m) = eut_divisor_eu_transport_new * eut_right_eu_transport_new) -> eut_divisor_eu_transport_new = 1)

Constructive proof overview

Generated structural guide

Balanced congruence transports actual common-divisor coprimality, even at modulus zero or one.

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

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

Proof neighborhood

Direct dependencies

totient_coprime_periodic Alpha theorem; checked-use authorized add_comm Stable theorem; checked-use authorized

Direct dependents

EU0002 euler_multiplier_coprime_iff

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

31 script commands · 10 reading checkpoints · 2 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.

01Fix variables and assumptionsL1–5

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

  1. L1
    intro m
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro hc
  5. L5
    intro hmod
02Separate the logical casesL6–7

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

  1. L6
    cases hmod
  2. L7
    cases hmod_witness
03Establish hpL8–11

Establish this local claim before using it. It is not an additional assumption.

  1. L8
    have hp : (forall eut_divisor_eu_transport_periodic. (exists eut_left_eu_transport_periodic. (m*x+a) = eut_divisor_eu_transport_periodic * eut_left_eu_transport_periodic) -> (exists eut_right_eu_transport_periodic. (m) = eut_divisor_eu_transport_periodic * eut_right_eu_transport_periodic) -> eut_divisor_eu_transport_periodic = 1)
  2. L9
    specialize totient_coprime_periodic m
  3. L10
    specialize totient_coprime_periodic x
  4. L11
    specialize totient_coprime_periodic a
04Separate the logical casesL12–12

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

  1. L12
    cases totient_coprime_periodic
05Use earlier factsL13–14

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

  1. L13
    apply totient_coprime_periodic_right
  2. L14
    exact hc
06Establish heL15–24

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

  1. L15
    have he : m*x+a=m*x1+b
  2. L16
    trans a+m*x
  3. L17
    specialize add_comm (m*x)
  4. L18
    specialize add_comm (a)
  5. L19
    apply add_comm
  6. L20
    trans b+m*x1
  7. L21
    exact hmod_witness_witness
  8. L22
    specialize add_comm (b)
  9. L23
    specialize add_comm (m*x1)
  10. L24
    apply add_comm
07Calculate and transport equalitiesL25–25

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L25
    rewrite he at hp
08Use earlier factsL26–28

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

  1. L26
    specialize totient_coprime_periodic m
  2. L27
    specialize totient_coprime_periodic x1
  3. L28
    specialize totient_coprime_periodic b
09Separate the logical casesL29–29

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

  1. L29
    cases totient_coprime_periodic
10Use earlier factsL30–31

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

  1. L30
    apply totient_coprime_periodic_left
  2. L31
    exact hp

Library-wide reading audit

Original exact command ledger · 31 lines
  1. 0001intro m
  2. 0002intro a
  3. 0003intro b
  4. 0004intro hc
  5. 0005intro hmod
  6. 0006cases hmod
  7. 0007cases hmod_witness
  8. 0008have hp : (forall eut_divisor_eu_transport_periodic. (exists eut_left_eu_transport_periodic. (m*x+a) = eut_divisor_eu_transport_periodic * eut_left_eu_transport_periodic) -> (exists eut_right_eu_transport_periodic. (m) = eut_divisor_eu_transport_periodic * eut_right_eu_transport_periodic) -> eut_divisor_eu_transport_periodic = 1)
  9. 0009specialize totient_coprime_periodic m
  10. 0010specialize totient_coprime_periodic x
  11. 0011specialize totient_coprime_periodic a
  12. 0012cases totient_coprime_periodic
  13. 0013apply totient_coprime_periodic_right
  14. 0014exact hc
  15. 0015have he : m*x+a=m*x1+b
  16. 0016trans a+m*x
  17. 0017specialize add_comm (m*x)
  18. 0018specialize add_comm (a)
  19. 0019apply add_comm
  20. 0020trans b+m*x1
  21. 0021exact hmod_witness_witness
  22. 0022specialize add_comm (b)
  23. 0023specialize add_comm (m*x1)
  24. 0024apply add_comm
  25. 0025rewrite he at hp
  26. 0026specialize totient_coprime_periodic m
  27. 0027specialize totient_coprime_periodic x1
  28. 0028specialize totient_coprime_periodic b
  29. 0029cases totient_coprime_periodic
  30. 0030apply totient_coprime_periodic_left
  31. 0031exact hp