EU0001

euler_coprime_mod_transport

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.

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

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

The exact G014 theorem is proved in this research checkpoint for m>1 and genuinely invertible a. Phi counts coprime residues independently of the conclusion. The broader coprime theorem also handles m=1 by congruence, not by asserting that one is a canonical remainder. No multiplicative-order or RSA theorem is claimed. The published atlas and Alpha membership are unchanged.

Exact theorem in conservative defined notation

∀ m. ∀ a. ∀ b. Coprime(a,m) → ModEq(m,a,b) → Coprime(b,m)

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

Definition DAG

Coprime(a,b) · 3ModEq(m,a,b) · 1

Actual proof prerequisites

totient_coprime_periodic · checked external prerequisiteadd_comm · checked external prerequisite
Original expanded first-order 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)

Complete tactic proof in conservative notation

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

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 : Coprime(m · x + a,m)Definitions: Coprime(m · x + a,m)Original native command in the exact edition
  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 defined 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 : Coprime(m · x + a,m)
  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