EU001B

euler_unit_product_reindex_scale

Actual beta composition along the multiplier permutation scales precisely the factors counted by Phi.

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. ∀ r. ∀ s. ∀ b. ∀ c. ∀ z. ∀ d. Coprime(a,m) → UnitMultiplierPrefix(a,m,r,s,m) → UnitProductPrefix(m,b,c,m) → (∀ x. ∀ y. ∀ n. Lt(x,m) → BetaAt(r,s,x,y) → BetaAt(b,c,y,n) → BetaAt(z,d,x,n)) → UnitScaledPrefix(a,m,b,c,z,d,m)

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

Definition DAG

CanonicalModularResidue(m,a,r) · 1UnitMultiplierPrefix(a,m,b,c,l) · 1UnitProductFactor(m,i,v) · 2UnitProductPrefix(m,b,c,l) · 1UnitScaledPrefix(a,m,b,c,d,e,l) · 1Lt(a,b) · 1Coprime(a,b) · 1BetaAt(b,c,i,x) · 5

Actual proof prerequisites

euler_unit_product_prefix_entrybeta_at_unique · checked external prerequisiteeuler_unit_factor_scaled_congruenceeuler_nonunit_factor_unchanged_congruence
Original expanded first-order statement 
forall a m r s b c z d. (forall eut_divisor_eu_reindex_unit. (exists eut_left_eu_reindex_unit. (a) = eut_divisor_eu_reindex_unit * eut_left_eu_reindex_unit) -> (exists eut_right_eu_reindex_unit. (m) = eut_divisor_eu_reindex_unit * eut_right_eu_reindex_unit) -> eut_divisor_eu_reindex_unit = 1) -> (forall eu_index_reindex_map. (exists eut_gap_eu_reindex_map_index. eut_gap_eu_reindex_map_index + S (eu_index_reindex_map) = (m)) -> exists eu_residue_reindex_map. (((exists fs_h_eu_reindex_map_at. fs_h_eu_reindex_map_at + S (eu_residue_reindex_map) = S ((S (eu_index_reindex_map)) * s)) /\ exists fs_q_eu_reindex_map_at. r = fs_q_eu_reindex_map_at * S ((S (eu_index_reindex_map)) * s) + (eu_residue_reindex_map))) /\ ((exists eut_gap_eu_reindex_map_bound. eut_gap_eu_reindex_map_bound + S (eu_residue_reindex_map) = (m)) /\ (exists eu_mod_left_reindex_map_mod eu_mod_right_reindex_map_mod. ((a)*eu_index_reindex_map) + (m) * eu_mod_left_reindex_map_mod = (eu_residue_reindex_map) + (m) * eu_mod_right_reindex_map_mod))) -> (forall eu_factor_index_reindex_factors. (exists eut_gap_eu_reindex_factors_index. eut_gap_eu_reindex_factors_index + S (eu_factor_index_reindex_factors) = (m)) -> exists eu_factor_value_reindex_factors. (((exists fs_h_eu_reindex_factors_at. fs_h_eu_reindex_factors_at + S (eu_factor_value_reindex_factors) = S ((S (eu_factor_index_reindex_factors)) * c)) /\ exists fs_q_eu_reindex_factors_at. b = fs_q_eu_reindex_factors_at * S ((S (eu_factor_index_reindex_factors)) * c) + (eu_factor_value_reindex_factors))) /\ ((((forall eut_divisor_eu_reindex_factors_choice_coprime. (exists eut_left_eu_reindex_factors_choice_coprime. (eu_factor_index_reindex_factors) = eut_divisor_eu_reindex_factors_choice_coprime * eut_left_eu_reindex_factors_choice_coprime) -> (exists eut_right_eu_reindex_factors_choice_coprime. (m) = eut_divisor_eu_reindex_factors_choice_coprime * eut_right_eu_reindex_factors_choice_coprime) -> eut_divisor_eu_reindex_factors_choice_coprime = 1) /\ (eu_factor_value_reindex_factors)=(eu_factor_index_reindex_factors)) \/ (~(forall eut_divisor_eu_reindex_factors_choice_coprime. (exists eut_left_eu_reindex_factors_choice_coprime. (eu_factor_index_reindex_factors) = eut_divisor_eu_reindex_factors_choice_coprime * eut_left_eu_reindex_factors_choice_coprime) -> (exists eut_right_eu_reindex_factors_choice_coprime. (m) = eut_divisor_eu_reindex_factors_choice_coprime * eut_right_eu_reindex_factors_choice_coprime) -> eut_divisor_eu_reindex_factors_choice_coprime = 1) /\ (eu_factor_value_reindex_factors)=1)))) -> (forall fms_i_eu_reindex_composition fms_j_eu_reindex_composition fms_v_eu_reindex_composition. (exists fms_gap_eu_reindex_composition. fms_gap_eu_reindex_composition + S (fms_i_eu_reindex_composition) = (m)) -> (((exists fs_h_fms_eu_reindex_composition_index. fs_h_fms_eu_reindex_composition_index + S (fms_j_eu_reindex_composition) = S ((S (fms_i_eu_reindex_composition)) * s)) /\ exists fs_q_fms_eu_reindex_composition_index. r = fs_q_fms_eu_reindex_composition_index * S ((S (fms_i_eu_reindex_composition)) * s) + (fms_j_eu_reindex_composition))) -> (((exists fs_h_fms_eu_reindex_composition_source. fs_h_fms_eu_reindex_composition_source + S (fms_v_eu_reindex_composition) = S ((S (fms_j_eu_reindex_composition)) * c)) /\ exists fs_q_fms_eu_reindex_composition_source. b = fs_q_fms_eu_reindex_composition_source * S ((S (fms_j_eu_reindex_composition)) * c) + (fms_v_eu_reindex_composition))) -> (((exists fs_h_fms_eu_reindex_composition_target. fs_h_fms_eu_reindex_composition_target + S (fms_v_eu_reindex_composition) = S ((S (fms_i_eu_reindex_composition)) * d)) /\ exists fs_q_fms_eu_reindex_composition_target. z = fs_q_fms_eu_reindex_composition_target * S ((S (fms_i_eu_reindex_composition)) * d) + (fms_v_eu_reindex_composition)))) -> (forall eu_scale_index_reindex_scale eu_scale_source_reindex_scale eu_scale_target_reindex_scale. (exists eut_gap_eu_reindex_scale_index. eut_gap_eu_reindex_scale_index + S (eu_scale_index_reindex_scale) = (m)) -> (((exists fs_h_eu_reindex_scale_source. fs_h_eu_reindex_scale_source + S (eu_scale_source_reindex_scale) = S ((S (eu_scale_index_reindex_scale)) * c)) /\ exists fs_q_eu_reindex_scale_source. b = fs_q_eu_reindex_scale_source * S ((S (eu_scale_index_reindex_scale)) * c) + (eu_scale_source_reindex_scale))) -> (((exists fs_h_eu_reindex_scale_target. fs_h_eu_reindex_scale_target + S (eu_scale_target_reindex_scale) = S ((S (eu_scale_index_reindex_scale)) * d)) /\ exists fs_q_eu_reindex_scale_target. z = fs_q_eu_reindex_scale_target * S ((S (eu_scale_index_reindex_scale)) * d) + (eu_scale_target_reindex_scale))) -> (((forall eut_divisor_eu_reindex_scale_unit. (exists eut_left_eu_reindex_scale_unit. (eu_scale_index_reindex_scale) = eut_divisor_eu_reindex_scale_unit * eut_left_eu_reindex_scale_unit) -> (exists eut_right_eu_reindex_scale_unit. (m) = eut_divisor_eu_reindex_scale_unit * eut_right_eu_reindex_scale_unit) -> eut_divisor_eu_reindex_scale_unit = 1) -> (exists eu_mod_left_reindex_scale_scaled eu_mod_right_reindex_scale_scaled. ((a)*eu_scale_source_reindex_scale) + (m) * eu_mod_left_reindex_scale_scaled = (eu_scale_target_reindex_scale) + (m) * eu_mod_right_reindex_scale_scaled)) /\ (~(forall eut_divisor_eu_reindex_scale_unit. (exists eut_left_eu_reindex_scale_unit. (eu_scale_index_reindex_scale) = eut_divisor_eu_reindex_scale_unit * eut_left_eu_reindex_scale_unit) -> (exists eut_right_eu_reindex_scale_unit. (m) = eut_divisor_eu_reindex_scale_unit * eut_right_eu_reindex_scale_unit) -> eut_divisor_eu_reindex_scale_unit = 1) -> (exists eu_mod_left_reindex_scale_unchanged eu_mod_right_reindex_scale_unchanged. (eu_scale_source_reindex_scale) + (m) * eu_mod_left_reindex_scale_unchanged = (eu_scale_target_reindex_scale) + (m) * eu_mod_right_reindex_scale_unchanged))))

Complete tactic proof in conservative notation

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

86 script commands · 18 reading checkpoints · 4 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 unit product prefix entryeuler unit factor scaled congruenceeuler nonunit factor unchanged congruence
01Fix variables and assumptionsL1–10

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

  1. L1
    intro a
  2. L2
    intro m
  3. L3
    intro r
  4. L4
    intro s
  5. L5
    intro b
  6. L6
    intro c
  7. L7
    intro z
  8. L8
    intro d
  9. L9
    intro ha
  10. L10
    intro hmap
02Fix variables and assumptionsL11–18

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

  1. L11
    intro hfac
  2. L12
    intro hcomp
  3. L13
    intro i
  4. L14
    intro u
  5. L15
    intro v
  6. L16
    intro hi
  7. L17
    intro hu
  8. L18
    intro hv
03Establish hindexL19–22

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

  1. L19
    have hindex : ∃ j. BetaAt(r,s,i,j) ∧ CanonicalModularResidue(m,a · i,j)Definitions: BetaAt(r,s,i,j)CanonicalModularResidue(m,a · i,j)Original native command in the exact edition
  2. L20
    specialize hmap (i)
  3. L21
    apply hmap
  4. L22
    exact hi
04Separate the logical casesL23–25

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

  1. L23
    cases hindex
  2. L24
    cases hindex_witness
  3. L25
    cases hindex_witness_right
05Establish hsourceL26–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euler unit product prefix entry.

  1. L26
    have hsource : UnitProductFactor(m,i,u)Definitions: UnitProductFactor(m,i,u)Original native command in the exact edition
  2. L27
    specialize euler_unit_product_prefix_entry (m)
  3. L28
    specialize euler_unit_product_prefix_entry (b)
  4. L29
    specialize euler_unit_product_prefix_entry (c)
  5. L30
    specialize euler_unit_product_prefix_entry (m)
  6. L31
    specialize euler_unit_product_prefix_entry (i)
  7. L32
    specialize euler_unit_product_prefix_entry (u)
  8. L33
    apply euler_unit_product_prefix_entry
  9. L34
    exact hfac
  10. L35
    exact hi
06Use earlier factsL36–36

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

  1. L36
    exact hu
07Establish htargetL37–40

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

  1. L37
    have htarget : ∃ w. BetaAt(b,c,x,w) ∧ UnitProductFactor(m,x,w)Definitions: BetaAt(b,c,x,w)UnitProductFactor(m,x,w)Original native command in the exact edition
  2. L38
    specialize hfac (x)
  3. L39
    apply hfac
  4. L40
    exact hindex_witness_right_left
08Separate the logical casesL41–42

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

  1. L41
    cases htarget
  2. L42
    cases htarget_witness
09Establish heL43–52

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

  1. L43
    have he : x1=v
  2. L44
    specialize beta_at_unique (z)
  3. L45
    specialize beta_at_unique (d)
  4. L46
    specialize beta_at_unique (i)
  5. L47
    specialize beta_at_unique (x1)
  6. L48
    specialize beta_at_unique (v)
  7. L49
    apply beta_at_unique
  8. L50
    specialize hcomp (i)
  9. L51
    specialize hcomp (x)
  10. L52
    specialize hcomp (x1)
10Use earlier factsL53–57

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

  1. L53
    apply hcomp
  2. L54
    exact hi
  3. L55
    exact hindex_witness_left
  4. L56
    exact htarget_witness_left
  5. L57
    exact hv
11Calculate and transport equalitiesL58–59

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

  1. L58
    rewrite he at htarget_witness_right
  2. L59
    rewrite he at htarget_witness_right
12Separate the logical casesL60–60

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

  1. L60
    split
13Fix variables and assumptionsL61–61

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

  1. L61
    intro hunit
14Use earlier factsL62–71

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

  1. L62
    specialize euler_unit_factor_scaled_congruence (a)
  2. L63
    specialize euler_unit_factor_scaled_congruence (m)
  3. L64
    specialize euler_unit_factor_scaled_congruence (i)
  4. L65
    specialize euler_unit_factor_scaled_congruence (x)
  5. L66
    specialize euler_unit_factor_scaled_congruence (u)
  6. L67
    specialize euler_unit_factor_scaled_congruence (v)
  7. L68
    apply euler_unit_factor_scaled_congruence
  8. L69
    exact ha
  9. L70
    exact hindex_witness_right_right
  10. L71
    exact hsource
15Use earlier factsL72–73

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

  1. L72
    exact htarget_witness_right
  2. L73
    exact hunit
16Fix variables and assumptionsL74–74

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

  1. L74
    intro hnot
17Use earlier factsL75–84

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

  1. L75
    specialize euler_nonunit_factor_unchanged_congruence (a)
  2. L76
    specialize euler_nonunit_factor_unchanged_congruence (m)
  3. L77
    specialize euler_nonunit_factor_unchanged_congruence (i)
  4. L78
    specialize euler_nonunit_factor_unchanged_congruence (x)
  5. L79
    specialize euler_nonunit_factor_unchanged_congruence (u)
  6. L80
    specialize euler_nonunit_factor_unchanged_congruence (v)
  7. L81
    apply euler_nonunit_factor_unchanged_congruence
  8. L82
    exact ha
  9. L83
    exact hindex_witness_right_right
  10. L84
    exact hsource
18Use earlier factsL85–86

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

  1. L85
    exact htarget_witness_right
  2. L86
    exact hnot

Library-wide reading audit

Original defined command ledger · 86 lines
  1. 0001intro a
  2. 0002intro m
  3. 0003intro r
  4. 0004intro s
  5. 0005intro b
  6. 0006intro c
  7. 0007intro z
  8. 0008intro d
  9. 0009intro ha
  10. 0010intro hmap
  11. 0011intro hfac
  12. 0012intro hcomp
  13. 0013intro i
  14. 0014intro u
  15. 0015intro v
  16. 0016intro hi
  17. 0017intro hu
  18. 0018intro hv
  19. 0019have hindex : ∃ j. BetaAt(r,s,i,j) ∧ CanonicalModularResidue(m,a · i,j)
  20. 0020specialize hmap (i)
  21. 0021apply hmap
  22. 0022exact hi
  23. 0023cases hindex
  24. 0024cases hindex_witness
  25. 0025cases hindex_witness_right
  26. 0026have hsource : UnitProductFactor(m,i,u)
  27. 0027specialize euler_unit_product_prefix_entry (m)
  28. 0028specialize euler_unit_product_prefix_entry (b)
  29. 0029specialize euler_unit_product_prefix_entry (c)
  30. 0030specialize euler_unit_product_prefix_entry (m)
  31. 0031specialize euler_unit_product_prefix_entry (i)
  32. 0032specialize euler_unit_product_prefix_entry (u)
  33. 0033apply euler_unit_product_prefix_entry
  34. 0034exact hfac
  35. 0035exact hi
  36. 0036exact hu
  37. 0037have htarget : ∃ w. BetaAt(b,c,x,w) ∧ UnitProductFactor(m,x,w)
  38. 0038specialize hfac (x)
  39. 0039apply hfac
  40. 0040exact hindex_witness_right_left
  41. 0041cases htarget
  42. 0042cases htarget_witness
  43. 0043have he : x1=v
  44. 0044specialize beta_at_unique (z)
  45. 0045specialize beta_at_unique (d)
  46. 0046specialize beta_at_unique (i)
  47. 0047specialize beta_at_unique (x1)
  48. 0048specialize beta_at_unique (v)
  49. 0049apply beta_at_unique
  50. 0050specialize hcomp (i)
  51. 0051specialize hcomp (x)
  52. 0052specialize hcomp (x1)
  53. 0053apply hcomp
  54. 0054exact hi
  55. 0055exact hindex_witness_left
  56. 0056exact htarget_witness_left
  57. 0057exact hv
  58. 0058rewrite he at htarget_witness_right
  59. 0059rewrite he at htarget_witness_right
  60. 0060split
  61. 0061intro hunit
  62. 0062specialize euler_unit_factor_scaled_congruence (a)
  63. 0063specialize euler_unit_factor_scaled_congruence (m)
  64. 0064specialize euler_unit_factor_scaled_congruence (i)
  65. 0065specialize euler_unit_factor_scaled_congruence (x)
  66. 0066specialize euler_unit_factor_scaled_congruence (u)
  67. 0067specialize euler_unit_factor_scaled_congruence (v)
  68. 0068apply euler_unit_factor_scaled_congruence
  69. 0069exact ha
  70. 0070exact hindex_witness_right_right
  71. 0071exact hsource
  72. 0072exact htarget_witness_right
  73. 0073exact hunit
  74. 0074intro hnot
  75. 0075specialize euler_nonunit_factor_unchanged_congruence (a)
  76. 0076specialize euler_nonunit_factor_unchanged_congruence (m)
  77. 0077specialize euler_nonunit_factor_unchanged_congruence (i)
  78. 0078specialize euler_nonunit_factor_unchanged_congruence (x)
  79. 0079specialize euler_nonunit_factor_unchanged_congruence (u)
  80. 0080specialize euler_nonunit_factor_unchanged_congruence (v)
  81. 0081apply euler_nonunit_factor_unchanged_congruence
  82. 0082exact ha
  83. 0083exact hindex_witness_right_right
  84. 0084exact hsource
  85. 0085exact htarget_witness_right
  86. 0086exact hnot