EU0008

euler_multiplier_prefix_extend

Append the actual next canonical residue, preserving every earlier decoded multiplier value.

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. ∀ b. ∀ c. ∀ l. ∀ r. UnitMultiplierPrefix(a,m,b,c,l) → Lt(r,m) → ModEq(m,a · l,r) → ∃ x. ∃ y. UnitMultiplierPrefix(a,m,x,y,S l)

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

Definition DAG

CanonicalModularResidue(m,a,r) · 1UnitMultiplierPrefix(a,m,b,c,l) · 2Lt(a,b) · 2ModEq(m,a,b) · 1BetaAt(b,c,i,x) · 1

Actual proof prerequisites

beta_prefix_extend · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisite
Original expanded first-order statement 
forall a m b c l r. (forall eu_index_map_extend_old. (exists eut_gap_eu_map_extend_old_index. eut_gap_eu_map_extend_old_index + S (eu_index_map_extend_old) = (l)) -> exists eu_residue_map_extend_old. (((exists fs_h_eu_map_extend_old_at. fs_h_eu_map_extend_old_at + S (eu_residue_map_extend_old) = S ((S (eu_index_map_extend_old)) * c)) /\ exists fs_q_eu_map_extend_old_at. b = fs_q_eu_map_extend_old_at * S ((S (eu_index_map_extend_old)) * c) + (eu_residue_map_extend_old))) /\ ((exists eut_gap_eu_map_extend_old_bound. eut_gap_eu_map_extend_old_bound + S (eu_residue_map_extend_old) = (m)) /\ (exists eu_mod_left_map_extend_old_mod eu_mod_right_map_extend_old_mod. ((a)*eu_index_map_extend_old) + (m) * eu_mod_left_map_extend_old_mod = (eu_residue_map_extend_old) + (m) * eu_mod_right_map_extend_old_mod))) -> (exists eut_gap_eu_extend_bound. eut_gap_eu_extend_bound + S (r) = (m)) -> (exists eu_mod_left_extend_last_mod eu_mod_right_extend_last_mod. (a*l) + (m) * eu_mod_left_extend_last_mod = (r) + (m) * eu_mod_right_extend_last_mod) -> exists d e. (forall eu_index_map_extend_new. (exists eut_gap_eu_map_extend_new_index. eut_gap_eu_map_extend_new_index + S (eu_index_map_extend_new) = (S l)) -> exists eu_residue_map_extend_new. (((exists fs_h_eu_map_extend_new_at. fs_h_eu_map_extend_new_at + S (eu_residue_map_extend_new) = S ((S (eu_index_map_extend_new)) * e)) /\ exists fs_q_eu_map_extend_new_at. d = fs_q_eu_map_extend_new_at * S ((S (eu_index_map_extend_new)) * e) + (eu_residue_map_extend_new))) /\ ((exists eut_gap_eu_map_extend_new_bound. eut_gap_eu_map_extend_new_bound + S (eu_residue_map_extend_new) = (m)) /\ (exists eu_mod_left_map_extend_new_mod eu_mod_right_map_extend_new_mod. ((a)*eu_index_map_extend_new) + (m) * eu_mod_left_map_extend_new_mod = (eu_residue_map_extend_new) + (m) * eu_mod_right_map_extend_new_mod)))

Complete tactic proof in conservative notation

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

49 script commands · 20 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–9

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

  1. L1
    intro a
  2. L2
    intro m
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro l
  6. L6
    intro r
  7. L7
    intro h
  8. L8
    intro hr
  9. L9
    intro hmod
02Use earlier factsL10–13

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

  1. L10
    specialize beta_prefix_extend l
  2. L11
    specialize beta_prefix_extend b
  3. L12
    specialize beta_prefix_extend c
  4. L13
    specialize beta_prefix_extend r
03Separate the logical casesL14–16

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

  1. L14
    cases beta_prefix_extend
  2. L15
    cases beta_prefix_extend_witness
  3. L16
    cases beta_prefix_extend_witness_witness
04Construct an explicit witnessL17–18

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

  1. L17
    exists x
  2. L18
    exists x1
05Fix variables and assumptionsL19–20

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

  1. L19
    intro i
  2. L20
    intro hi
06Establish hsL21–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L21
    have hs : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L22
    specialize finite_lt_succ_eq_or_lt (l)
  3. L23
    specialize finite_lt_succ_eq_or_lt (i)
  4. L24
    apply finite_lt_succ_eq_or_lt
  5. L25
    exact hi
07Separate the logical casesL26–26

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

  1. L26
    cases hs
08Construct an explicit witnessL27–27

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

  1. L27
    exists r
09Separate the logical casesL28–28

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

  1. L28
    split
10Calculate and transport equalitiesL29–30

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

  1. L29
    rewrite hs_left
  2. L30
    rewrite hs_left
11Use earlier factsL31–31

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

  1. L31
    exact beta_prefix_extend_witness_witness_left
12Separate the logical casesL32–32

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

  1. L32
    split
13Use earlier factsL33–33

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

  1. L33
    exact hr
14Calculate and transport equalitiesL34–34

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

  1. L34
    rewrite hs_left
15Use earlier factsL35–35

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

  1. L35
    exact hmod
16Establish hpL36–39

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

  1. L36
    have hp : ∃ s. BetaAt(b,c,i,s) ∧ CanonicalModularResidue(m,a · i,s)Definitions: BetaAt(b,c,i,s)CanonicalModularResidue(m,a · i,s)Original native command in the exact edition
  2. L37
    specialize h (i)
  3. L38
    apply h
  4. L39
    exact hs_right
17Separate the logical casesL40–41

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

  1. L40
    cases hp
  2. L41
    cases hp_witness
18Construct an explicit witnessL42–42

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

  1. L42
    exists x2
19Separate the logical casesL43–43

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

  1. L43
    split
20Use earlier factsL44–49

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

  1. L44
    specialize beta_prefix_extend_witness_witness_right (i)
  2. L45
    specialize beta_prefix_extend_witness_witness_right (x2)
  3. L46
    apply beta_prefix_extend_witness_witness_right
  4. L47
    exact hs_right
  5. L48
    exact hp_witness_left
  6. L49
    exact hp_witness_right

Library-wide reading audit

Original defined command ledger · 49 lines
  1. 0001intro a
  2. 0002intro m
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro r
  7. 0007intro h
  8. 0008intro hr
  9. 0009intro hmod
  10. 0010specialize beta_prefix_extend l
  11. 0011specialize beta_prefix_extend b
  12. 0012specialize beta_prefix_extend c
  13. 0013specialize beta_prefix_extend r
  14. 0014cases beta_prefix_extend
  15. 0015cases beta_prefix_extend_witness
  16. 0016cases beta_prefix_extend_witness_witness
  17. 0017exists x
  18. 0018exists x1
  19. 0019intro i
  20. 0020intro hi
  21. 0021have hs : i = l ∨ Lt(i,l)
  22. 0022specialize finite_lt_succ_eq_or_lt (l)
  23. 0023specialize finite_lt_succ_eq_or_lt (i)
  24. 0024apply finite_lt_succ_eq_or_lt
  25. 0025exact hi
  26. 0026cases hs
  27. 0027exists r
  28. 0028split
  29. 0029rewrite hs_left
  30. 0030rewrite hs_left
  31. 0031exact beta_prefix_extend_witness_witness_left
  32. 0032split
  33. 0033exact hr
  34. 0034rewrite hs_left
  35. 0035exact hmod
  36. 0036have hp : ∃ s. BetaAt(b,c,i,s) ∧ CanonicalModularResidue(m,a · i,s)
  37. 0037specialize h (i)
  38. 0038apply h
  39. 0039exact hs_right
  40. 0040cases hp
  41. 0041cases hp_witness
  42. 0042exists x2
  43. 0043split
  44. 0044specialize beta_prefix_extend_witness_witness_right (i)
  45. 0045specialize beta_prefix_extend_witness_witness_right (x2)
  46. 0046apply beta_prefix_extend_witness_witness_right
  47. 0047exact hs_right
  48. 0048exact hp_witness_left
  49. 0049exact hp_witness_right