EU000E

euler_unit_product_factor_exists

Construct the actual weighted factor by the independent decidable coprimality predicate.

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

∀ m. ∀ i. ∃ v. UnitProductFactor(m,i,v)

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

Definition DAG

UnitProductFactor(m,i,v) · 1Coprime(a,b) · 2

Actual proof prerequisites

totient_coprime_decidable · checked external prerequisite
Original expanded first-order statement 
forall m i. exists v. ((((forall eut_divisor_eu_factor_exists_coprime. (exists eut_left_eu_factor_exists_coprime. (i) = eut_divisor_eu_factor_exists_coprime * eut_left_eu_factor_exists_coprime) -> (exists eut_right_eu_factor_exists_coprime. (m) = eut_divisor_eu_factor_exists_coprime * eut_right_eu_factor_exists_coprime) -> eut_divisor_eu_factor_exists_coprime = 1) /\ (v)=(i)) \/ (~(forall eut_divisor_eu_factor_exists_coprime. (exists eut_left_eu_factor_exists_coprime. (i) = eut_divisor_eu_factor_exists_coprime * eut_left_eu_factor_exists_coprime) -> (exists eut_right_eu_factor_exists_coprime. (m) = eut_divisor_eu_factor_exists_coprime * eut_right_eu_factor_exists_coprime) -> eut_divisor_eu_factor_exists_coprime = 1) /\ (v)=1)))

Complete tactic proof in conservative notation

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

17 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.

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

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

  1. L1
    intro m
  2. L2
    intro i
02Establish hcL3–6

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

  1. L3
    have hc : Coprime(i,m) ∨ ¬Coprime(i,m)Definitions: Coprime(i,m)Original native command in the exact edition
  2. L4
    specialize totient_coprime_decidable (i)
  3. L5
    specialize totient_coprime_decidable (m)
  4. L6
    apply totient_coprime_decidable
03Separate the logical casesL7–7

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

  1. L7
    cases hc
04Construct an explicit witnessL8–8

Supply the displayed value, then prove that it has the required property.

  1. L8
    exists i
05Separate the logical casesL9–10

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

  1. L9
    left
  2. L10
    split
06Use earlier factsL11–11

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

  1. L11
    exact hc_left
07Calculate and transport equalitiesL12–12

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

  1. L12
    refl
08Construct an explicit witnessL13–13

Supply the displayed value, then prove that it has the required property.

  1. L13
    exists 1
09Separate the logical casesL14–15

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

  1. L14
    right
  2. L15
    split
10Use earlier factsL16–16

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

  1. L16
    exact hc_right
11Calculate and transport equalitiesL17–17

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

  1. L17
    refl

Library-wide reading audit

Original defined command ledger · 17 lines
  1. 0001intro m
  2. 0002intro i
  3. 0003have hc : Coprime(i,m) ∨ ¬Coprime(i,m)
  4. 0004specialize totient_coprime_decidable (i)
  5. 0005specialize totient_coprime_decidable (m)
  6. 0006apply totient_coprime_decidable
  7. 0007cases hc
  8. 0008exists i
  9. 0009left
  10. 0010split
  11. 0011exact hc_left
  12. 0012refl
  13. 0013exists 1
  14. 0014right
  15. 0015split
  16. 0016exact hc_right
  17. 0017refl