EU0009

euler_multiplier_prefix_exists

HA induction builds the complete beta-coded multiplier prefix; no map or bijection is supplied as a premise.

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

∀ a. ∀ m. ∀ l. ¬m = 0 → ∃ x. ∃ y. UnitMultiplierPrefix(a,m,x,y,l)

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

Definition DAG

CanonicalModularResidue(m,a,r) · 1UnitMultiplierPrefix(a,m,b,c,l) · 2

Actual proof prerequisites

euler_multiplier_prefix_emptyeuler_multiplier_residue_existseuler_multiplier_prefix_extend
Original expanded first-order statement 
forall a m l. ~(m=0) -> exists b c. (forall eu_index_map_exists. (exists eut_gap_eu_map_exists_index. eut_gap_eu_map_exists_index + S (eu_index_map_exists) = (l)) -> exists eu_residue_map_exists. (((exists fs_h_eu_map_exists_at. fs_h_eu_map_exists_at + S (eu_residue_map_exists) = S ((S (eu_index_map_exists)) * c)) /\ exists fs_q_eu_map_exists_at. b = fs_q_eu_map_exists_at * S ((S (eu_index_map_exists)) * c) + (eu_residue_map_exists))) /\ ((exists eut_gap_eu_map_exists_bound. eut_gap_eu_map_exists_bound + S (eu_residue_map_exists) = (m)) /\ (exists eu_mod_left_map_exists_mod eu_mod_right_map_exists_mod. ((a)*eu_index_map_exists) + (m) * eu_mod_left_map_exists_mod = (eu_residue_map_exists) + (m) * eu_mod_right_map_exists_mod)))

Complete tactic proof in conservative notation

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

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

Named ingredients (3)
euler multiplier prefix emptyeuler multiplier residue existseuler multiplier prefix extend
01Fix variables and assumptionsL1–2

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

  1. L1
    intro a
  2. L2
    intro m
02Induction on lL3–4

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L3
    induction l
  2. L4
    intro hm
03Construct an explicit witnessL5–6

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

  1. L5
    exists 0
  2. L6
    exists 0
04Use earlier factsL7–11

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

  1. L7
    specialize euler_multiplier_prefix_empty (a)
  2. L8
    specialize euler_multiplier_prefix_empty (m)
  3. L9
    specialize euler_multiplier_prefix_empty (0)
  4. L10
    specialize euler_multiplier_prefix_empty (0)
  5. L11
    apply euler_multiplier_prefix_empty
05Fix variables and assumptionsL12–12

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

  1. L12
    intro hm
06Establish hpL13–15

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

  1. L13
    have hp : ∃ b. ∃ c. UnitMultiplierPrefix(a,m,b,c,l)Definitions: UnitMultiplierPrefix(a,m,b,c,l)Original native command in the exact edition
  2. L14
    apply IH
  3. L15
    exact hm
07Separate the logical casesL16–17

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

  1. L16
    cases hp
  2. L17
    cases hp_witness
08Establish hrL18–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euler multiplier residue exists.

  1. L18
    have hr : ∃ r. CanonicalModularResidue(m,a · l,r)Definitions: CanonicalModularResidue(m,a · l,r)Original native command in the exact edition
  2. L19
    specialize euler_multiplier_residue_exists (a)
  3. L20
    specialize euler_multiplier_residue_exists (m)
  4. L21
    specialize euler_multiplier_residue_exists (l)
  5. L22
    apply euler_multiplier_residue_exists
  6. L23
    exact hm
09Separate the logical casesL24–25

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

  1. L24
    cases hr
  2. L25
    cases hr_witness
10Use earlier factsL26–35

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

  1. L26
    specialize euler_multiplier_prefix_extend (a)
  2. L27
    specialize euler_multiplier_prefix_extend (m)
  3. L28
    specialize euler_multiplier_prefix_extend (x)
  4. L29
    specialize euler_multiplier_prefix_extend (x1)
  5. L30
    specialize euler_multiplier_prefix_extend (l)
  6. L31
    specialize euler_multiplier_prefix_extend (x2)
  7. L32
    apply euler_multiplier_prefix_extend
  8. L33
    exact hp_witness_witness
  9. L34
    exact hr_witness_left
  10. L35
    exact hr_witness_right

Library-wide reading audit

Original defined command ledger · 35 lines
  1. 0001intro a
  2. 0002intro m
  3. 0003induction l
  4. 0004intro hm
  5. 0005exists 0
  6. 0006exists 0
  7. 0007specialize euler_multiplier_prefix_empty (a)
  8. 0008specialize euler_multiplier_prefix_empty (m)
  9. 0009specialize euler_multiplier_prefix_empty (0)
  10. 0010specialize euler_multiplier_prefix_empty (0)
  11. 0011apply euler_multiplier_prefix_empty
  12. 0012intro hm
  13. 0013have hp : ∃ b. ∃ c. UnitMultiplierPrefix(a,m,b,c,l)
  14. 0014apply IH
  15. 0015exact hm
  16. 0016cases hp
  17. 0017cases hp_witness
  18. 0018have hr : ∃ r. CanonicalModularResidue(m,a · l,r)
  19. 0019specialize euler_multiplier_residue_exists (a)
  20. 0020specialize euler_multiplier_residue_exists (m)
  21. 0021specialize euler_multiplier_residue_exists (l)
  22. 0022apply euler_multiplier_residue_exists
  23. 0023exact hm
  24. 0024cases hr
  25. 0025cases hr_witness
  26. 0026specialize euler_multiplier_prefix_extend (a)
  27. 0027specialize euler_multiplier_prefix_extend (m)
  28. 0028specialize euler_multiplier_prefix_extend (x)
  29. 0029specialize euler_multiplier_prefix_extend (x1)
  30. 0030specialize euler_multiplier_prefix_extend (l)
  31. 0031specialize euler_multiplier_prefix_extend (x2)
  32. 0032apply euler_multiplier_prefix_extend
  33. 0033exact hp_witness_witness
  34. 0034exact hr_witness_left
  35. 0035exact hr_witness_right