EU001F

euler_coprime_totient_power_value

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

For every positive modulus and any actual Phi and Pow values, construct all finite permutation/product witnesses and prove the Euler congruence by coprime cancellation.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Exact expanded first-order arithmetic statement

forall a m t w. ~(m=0) -> (forall eut_divisor_eu_endpoint_coprime. (exists eut_left_eu_endpoint_coprime. (a) = eut_divisor_eu_endpoint_coprime * eut_left_eu_endpoint_coprime) -> (exists eut_right_eu_endpoint_coprime. (m) = eut_divisor_eu_endpoint_coprime * eut_right_eu_endpoint_coprime) -> eut_divisor_eu_endpoint_coprime = 1) -> ((~((m)=0) /\ (exists eut_code_eu_endpoint_phi_count eut_scale_eu_endpoint_phi_count. (forall eut_index_eu_endpoint_phi_count_mask. (exists eut_gap_eu_endpoint_phi_count_mask_bound. eut_gap_eu_endpoint_phi_count_mask_bound + S (eut_index_eu_endpoint_phi_count_mask) = (m)) -> exists eut_bit_eu_endpoint_phi_count_mask. (((exists fs_h_eut_eu_endpoint_phi_count_mask_entry. fs_h_eut_eu_endpoint_phi_count_mask_entry + S (eut_bit_eu_endpoint_phi_count_mask) = S ((S (eut_index_eu_endpoint_phi_count_mask)) * eut_scale_eu_endpoint_phi_count)) /\ exists fs_q_eut_eu_endpoint_phi_count_mask_entry. eut_code_eu_endpoint_phi_count = fs_q_eut_eu_endpoint_phi_count_mask_entry * S ((S (eut_index_eu_endpoint_phi_count_mask)) * eut_scale_eu_endpoint_phi_count) + (eut_bit_eu_endpoint_phi_count_mask))) /\ ((((forall eut_divisor_eu_endpoint_phi_count_mask_choice_coprime. (exists eut_left_eu_endpoint_phi_count_mask_choice_coprime. (eut_index_eu_endpoint_phi_count_mask) = eut_divisor_eu_endpoint_phi_count_mask_choice_coprime * eut_left_eu_endpoint_phi_count_mask_choice_coprime) -> (exists eut_right_eu_endpoint_phi_count_mask_choice_coprime. (m) = eut_divisor_eu_endpoint_phi_count_mask_choice_coprime * eut_right_eu_endpoint_phi_count_mask_choice_coprime) -> eut_divisor_eu_endpoint_phi_count_mask_choice_coprime = 1) /\ (eut_bit_eu_endpoint_phi_count_mask) = 1) \/ (~(forall eut_divisor_eu_endpoint_phi_count_mask_choice_coprime. (exists eut_left_eu_endpoint_phi_count_mask_choice_coprime. (eut_index_eu_endpoint_phi_count_mask) = eut_divisor_eu_endpoint_phi_count_mask_choice_coprime * eut_left_eu_endpoint_phi_count_mask_choice_coprime) -> (exists eut_right_eu_endpoint_phi_count_mask_choice_coprime. (m) = eut_divisor_eu_endpoint_phi_count_mask_choice_coprime * eut_right_eu_endpoint_phi_count_mask_choice_coprime) -> eut_divisor_eu_endpoint_phi_count_mask_choice_coprime = 1) /\ (eut_bit_eu_endpoint_phi_count_mask) = 0)))) /\ (exists fs_u_eut_eu_endpoint_phi_count_sum fs_v_eut_eu_endpoint_phi_count_sum. ((((exists fs_h_eut_eu_endpoint_phi_count_sum_body_start. fs_h_eut_eu_endpoint_phi_count_sum_body_start + S (0) = S ((S (0)) * fs_v_eut_eu_endpoint_phi_count_sum)) /\ exists fs_q_eut_eu_endpoint_phi_count_sum_body_start. fs_u_eut_eu_endpoint_phi_count_sum = fs_q_eut_eu_endpoint_phi_count_sum_body_start * S ((S (0)) * fs_v_eut_eu_endpoint_phi_count_sum) + (0))) /\ ((((exists fs_h_eut_eu_endpoint_phi_count_sum_body_terminal. fs_h_eut_eu_endpoint_phi_count_sum_body_terminal + S (t) = S ((S (m)) * fs_v_eut_eu_endpoint_phi_count_sum)) /\ exists fs_q_eut_eu_endpoint_phi_count_sum_body_terminal. fs_u_eut_eu_endpoint_phi_count_sum = fs_q_eut_eu_endpoint_phi_count_sum_body_terminal * S ((S (m)) * fs_v_eut_eu_endpoint_phi_count_sum) + (t))) /\ forall fs_i_eut_eu_endpoint_phi_count_sum_body_steps. (exists fs_lt_eut_eu_endpoint_phi_count_sum_body_steps_bound. fs_lt_eut_eu_endpoint_phi_count_sum_body_steps_bound + S fs_i_eut_eu_endpoint_phi_count_sum_body_steps = m) -> exists fs_a_eut_eu_endpoint_phi_count_sum_body_steps fs_r_eut_eu_endpoint_phi_count_sum_body_steps fs_s_eut_eu_endpoint_phi_count_sum_body_steps. ((((exists fs_h_eut_eu_endpoint_phi_count_sum_body_steps_summand. fs_h_eut_eu_endpoint_phi_count_sum_body_steps_summand + S (fs_a_eut_eu_endpoint_phi_count_sum_body_steps) = S ((S (fs_i_eut_eu_endpoint_phi_count_sum_body_steps)) * eut_scale_eu_endpoint_phi_count)) /\ exists fs_q_eut_eu_endpoint_phi_count_sum_body_steps_summand. eut_code_eu_endpoint_phi_count = fs_q_eut_eu_endpoint_phi_count_sum_body_steps_summand * S ((S (fs_i_eut_eu_endpoint_phi_count_sum_body_steps)) * eut_scale_eu_endpoint_phi_count) + (fs_a_eut_eu_endpoint_phi_count_sum_body_steps))) /\ ((((exists fs_h_eut_eu_endpoint_phi_count_sum_body_steps_partial. fs_h_eut_eu_endpoint_phi_count_sum_body_steps_partial + S (fs_r_eut_eu_endpoint_phi_count_sum_body_steps) = S ((S (fs_i_eut_eu_endpoint_phi_count_sum_body_steps)) * fs_v_eut_eu_endpoint_phi_count_sum)) /\ exists fs_q_eut_eu_endpoint_phi_count_sum_body_steps_partial. fs_u_eut_eu_endpoint_phi_count_sum = fs_q_eut_eu_endpoint_phi_count_sum_body_steps_partial * S ((S (fs_i_eut_eu_endpoint_phi_count_sum_body_steps)) * fs_v_eut_eu_endpoint_phi_count_sum) + (fs_r_eut_eu_endpoint_phi_count_sum_body_steps))) /\ ((((exists fs_h_eut_eu_endpoint_phi_count_sum_body_steps_successor. fs_h_eut_eu_endpoint_phi_count_sum_body_steps_successor + S (fs_s_eut_eu_endpoint_phi_count_sum_body_steps) = S ((S (S fs_i_eut_eu_endpoint_phi_count_sum_body_steps)) * fs_v_eut_eu_endpoint_phi_count_sum)) /\ exists fs_q_eut_eu_endpoint_phi_count_sum_body_steps_successor. fs_u_eut_eu_endpoint_phi_count_sum = fs_q_eut_eu_endpoint_phi_count_sum_body_steps_successor * S ((S (S fs_i_eut_eu_endpoint_phi_count_sum_body_steps)) * fs_v_eut_eu_endpoint_phi_count_sum) + (fs_s_eut_eu_endpoint_phi_count_sum_body_steps))) /\ fs_s_eut_eu_endpoint_phi_count_sum_body_steps = fs_r_eut_eu_endpoint_phi_count_sum_body_steps + fs_a_eut_eu_endpoint_phi_count_sum_body_steps))))))))) -> (exists pa_b_euta_eu_endpoint_power pa_c_euta_eu_endpoint_power. ((forall pa_i_euta_eu_endpoint_power_repeat. (exists pa_lt_euta_eu_endpoint_power_repeat_bound. pa_lt_euta_eu_endpoint_power_repeat_bound + S pa_i_euta_eu_endpoint_power_repeat = t) -> (((exists pa_h_euta_eu_endpoint_power_repeat_decoded. pa_h_euta_eu_endpoint_power_repeat_decoded + S (a) = S ((S (pa_i_euta_eu_endpoint_power_repeat)) * pa_c_euta_eu_endpoint_power)) /\ exists pa_q_euta_eu_endpoint_power_repeat_decoded. pa_b_euta_eu_endpoint_power = pa_q_euta_eu_endpoint_power_repeat_decoded * S ((S (pa_i_euta_eu_endpoint_power_repeat)) * pa_c_euta_eu_endpoint_power) + (a)))) /\ (exists pa_u_euta_eu_endpoint_power_product pa_v_euta_eu_endpoint_power_product. ((((exists pa_h_euta_eu_endpoint_power_product_start. pa_h_euta_eu_endpoint_power_product_start + S (1) = S ((S (0)) * pa_v_euta_eu_endpoint_power_product)) /\ exists pa_q_euta_eu_endpoint_power_product_start. pa_u_euta_eu_endpoint_power_product = pa_q_euta_eu_endpoint_power_product_start * S ((S (0)) * pa_v_euta_eu_endpoint_power_product) + (1))) /\ ((((exists pa_h_euta_eu_endpoint_power_product_terminal. pa_h_euta_eu_endpoint_power_product_terminal + S (w) = S ((S (t)) * pa_v_euta_eu_endpoint_power_product)) /\ exists pa_q_euta_eu_endpoint_power_product_terminal. pa_u_euta_eu_endpoint_power_product = pa_q_euta_eu_endpoint_power_product_terminal * S ((S (t)) * pa_v_euta_eu_endpoint_power_product) + (w))) /\ forall pa_i_euta_eu_endpoint_power_product. (exists pa_lt_euta_eu_endpoint_power_product_bound. pa_lt_euta_eu_endpoint_power_product_bound + S pa_i_euta_eu_endpoint_power_product = t) -> exists pa_p_euta_eu_endpoint_power_product pa_r_euta_eu_endpoint_power_product pa_s_euta_eu_endpoint_power_product. ((((exists pa_h_euta_eu_endpoint_power_product_factor. pa_h_euta_eu_endpoint_power_product_factor + S (pa_p_euta_eu_endpoint_power_product) = S ((S (pa_i_euta_eu_endpoint_power_product)) * pa_c_euta_eu_endpoint_power)) /\ exists pa_q_euta_eu_endpoint_power_product_factor. pa_b_euta_eu_endpoint_power = pa_q_euta_eu_endpoint_power_product_factor * S ((S (pa_i_euta_eu_endpoint_power_product)) * pa_c_euta_eu_endpoint_power) + (pa_p_euta_eu_endpoint_power_product))) /\ ((((exists pa_h_euta_eu_endpoint_power_product_partial. pa_h_euta_eu_endpoint_power_product_partial + S (pa_r_euta_eu_endpoint_power_product) = S ((S (pa_i_euta_eu_endpoint_power_product)) * pa_v_euta_eu_endpoint_power_product)) /\ exists pa_q_euta_eu_endpoint_power_product_partial. pa_u_euta_eu_endpoint_power_product = pa_q_euta_eu_endpoint_power_product_partial * S ((S (pa_i_euta_eu_endpoint_power_product)) * pa_v_euta_eu_endpoint_power_product) + (pa_r_euta_eu_endpoint_power_product))) /\ ((((exists pa_h_euta_eu_endpoint_power_product_successor. pa_h_euta_eu_endpoint_power_product_successor + S (pa_s_euta_eu_endpoint_power_product) = S ((S (S pa_i_euta_eu_endpoint_power_product)) * pa_v_euta_eu_endpoint_power_product)) /\ exists pa_q_euta_eu_endpoint_power_product_successor. pa_u_euta_eu_endpoint_power_product = pa_q_euta_eu_endpoint_power_product_successor * S ((S (S pa_i_euta_eu_endpoint_power_product)) * pa_v_euta_eu_endpoint_power_product) + (pa_s_euta_eu_endpoint_power_product))) /\ pa_s_euta_eu_endpoint_power_product = pa_r_euta_eu_endpoint_power_product * pa_p_euta_eu_endpoint_power_product)))))))) -> (exists eu_mod_left_endpoint_result eu_mod_right_endpoint_result. (w) + (m) * eu_mod_left_endpoint_result = (1) + (m) * eu_mod_right_endpoint_result)

Constructive proof overview

Generated structural guide

For every positive modulus and any actual Phi and Pow values, construct all finite permutation/product witnesses and prove the Euler congruence by coprime cancellation.

The unchanged tactic script uses 9 declared prerequisites and contains 111 exact native proof lines.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

EU0014 euler_unit_product_prefix_exists beta_product_exists Stable theorem; checked-use authorized EU000D euler_multiplier_permutation_exists finite_beta_composition_exists Alpha theorem; checked-use authorized beta_product_permutation_invariant Alpha theorem; checked-use authorized EU001B euler_unit_product_reindex_scale EU001E euler_unit_count_product_balance EU0017 euler_unit_product_coprime EU001D euler_coprime_weighted_product_cancel

Direct dependents

EU0020 euler_coprime_totient_power

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

111 script commands · 21 reading checkpoints · 8 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.

Named ingredients (6)
euler unit product prefix existseuler multiplier permutation existseuler unit product reindex scaleeuler unit count product balanceeuler unit product coprimeeuler coprime weighted product cancel

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–8

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

  1. L1
    intro a
  2. L2
    intro m
  3. L3
    intro t
  4. L4
    intro w
  5. L5
    intro hm
  6. L6
    intro ha
  7. L7
    intro ht
  8. L8
    intro hw
02Separate the logical casesL9–9

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

  1. L9
    cases ht
03Establish hfL10–13

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

  1. L10
    have hf : ∃ b. ∃ c. UnitProductPrefix(m,b,c,m)Definitions: UnitProductPrefix
  2. L11
    specialize euler_unit_product_prefix_exists (m)
  3. L12
    specialize euler_unit_product_prefix_exists (m)
  4. L13
    apply euler_unit_product_prefix_exists
04Separate the logical casesL14–15

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

  1. L14
    cases hf
  2. L15
    cases hf_witness
05Establish hPL16–20

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

  1. L16
    have hP : ∃ P. Product(x,x1,m,P)Definitions: Product
  2. L17
    specialize beta_product_exists (x)
  3. L18
    specialize beta_product_exists (x1)
  4. L19
    specialize beta_product_exists (m)
  5. L20
    apply beta_product_exists
06Separate the logical casesL21–21

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

  1. L21
    cases hP
07Establish hmapL22–27

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

  1. L22
    have hmap : ∃ r. ∃ s. UnitMultiplierPrefix(a,m,r,s,m) ∧ PermutationPrefix(r,s,m)Definitions: PermutationPrefixUnitMultiplierPrefix
  2. L23
    specialize euler_multiplier_permutation_exists (a)
  3. L24
    specialize euler_multiplier_permutation_exists (m)
  4. L25
    apply euler_multiplier_permutation_exists
  5. L26
    exact hm
  6. L27
    exact ha
08Separate the logical casesL28–32

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

  1. L28
    cases hmap
  2. L29
    cases hmap_witness
  3. L30
    cases hmap_witness_witness
  4. L31
    cases hmap_witness_witness_right
  5. L32
    cases hmap_witness_witness_right_right
09Establish hcompL33–39

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

  1. L33
    have hcomp : ∃ z. ∃ d. ∀ y. ∀ n. ∀ k. Lt(y,m) → BetaAt(x3,x4,y,n) → BetaAt(x,x1,n,k) → BetaAt(z,d,y,k)Definitions: LtBetaAt
  2. L34
    specialize finite_beta_composition_exists (x3)
  3. L35
    specialize finite_beta_composition_exists (x4)
  4. L36
    specialize finite_beta_composition_exists (x)
  5. L37
    specialize finite_beta_composition_exists (x1)
  6. L38
    specialize finite_beta_composition_exists (m)
  7. L39
    apply finite_beta_composition_exists
10Separate the logical casesL40–41

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

  1. L40
    cases hcomp
  2. L41
    cases hcomp_witness
11Establish hQL42–46

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

  1. L42
    have hQ : ∃ Q. Product(x5,x6,m,Q)Definitions: Product
  2. L43
    specialize beta_product_exists (x5)
  3. L44
    specialize beta_product_exists (x6)
  4. L45
    specialize beta_product_exists (m)
  5. L46
    apply beta_product_exists
12Separate the logical casesL47–47

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

  1. L47
    cases hQ
13Establish heL48–57

Establish this local claim before using it. It is not an additional assumption.

  1. L48
    have he : x7=x2
  2. L49
    symm
  3. L50
    specialize beta_product_permutation_invariant (m)
  4. L51
    specialize beta_product_permutation_invariant (x3)
  5. L52
    specialize beta_product_permutation_invariant (x4)
  6. L53
    specialize beta_product_permutation_invariant (x)
  7. L54
    specialize beta_product_permutation_invariant (x1)
  8. L55
    specialize beta_product_permutation_invariant (x5)
  9. L56
    specialize beta_product_permutation_invariant (x6)
  10. L57
    specialize beta_product_permutation_invariant (x2)
14Use earlier factsL58–64

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

  1. L58
    specialize beta_product_permutation_invariant (x7)
  2. L59
    apply beta_product_permutation_invariant
  3. L60
    exact hmap_witness_witness_right_left
  4. L61
    exact hmap_witness_witness_right_right_left
  5. L62
    exact hcomp_witness_witness
  6. L63
    exact hP_witness
  7. L64
    exact hQ_witness
15Establish hsL65–74

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

  1. L65
    have hs : UnitScaledPrefix(a,m,x,x1,x5,x6,m)Definitions: UnitScaledPrefix
  2. L66
    specialize euler_unit_product_reindex_scale (a)
  3. L67
    specialize euler_unit_product_reindex_scale (m)
  4. L68
    specialize euler_unit_product_reindex_scale (x3)
  5. L69
    specialize euler_unit_product_reindex_scale (x4)
  6. L70
    specialize euler_unit_product_reindex_scale (x)
  7. L71
    specialize euler_unit_product_reindex_scale (x1)
  8. L72
    specialize euler_unit_product_reindex_scale (x5)
  9. L73
    specialize euler_unit_product_reindex_scale (x6)
  10. L74
    apply euler_unit_product_reindex_scale
16Use earlier factsL75–78

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

  1. L75
    exact ha
  2. L76
    exact hmap_witness_witness_left
  3. L77
    exact hf_witness_witness
  4. L78
    exact hcomp_witness_witness
17Establish hbalanceL79–88

Establish this local claim before using it. It is not an additional assumption.

  1. L79
    have hbalance : exists eu_mod_left_endpoint_balance eu_mod_right_endpoint_balance. (w*x2) + (m) * eu_mod_left_endpoint_balance = (x7) + (m) * eu_mod_right_endpoint_balance
  2. L80
    specialize euler_unit_count_product_balance (m)
  3. L81
    specialize euler_unit_count_product_balance (a)
  4. L82
    specialize euler_unit_count_product_balance (m)
  5. L83
    specialize euler_unit_count_product_balance (x)
  6. L84
    specialize euler_unit_count_product_balance (x1)
  7. L85
    specialize euler_unit_count_product_balance (x5)
  8. L86
    specialize euler_unit_count_product_balance (x6)
  9. L87
    specialize euler_unit_count_product_balance (t)
  10. L88
    specialize euler_unit_count_product_balance (x2)
18Use earlier factsL89–96

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

  1. L89
    specialize euler_unit_count_product_balance (x7)
  2. L90
    specialize euler_unit_count_product_balance (w)
  3. L91
    apply euler_unit_count_product_balance
  4. L92
    exact ht_right
  5. L93
    exact hs
  6. L94
    exact hP_witness
  7. L95
    exact hQ_witness
  8. L96
    exact hw
19Calculate and transport equalitiesL97–97

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

  1. L97
    rewrite he at hbalance
20Use earlier factsL98–107

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

  1. L98
    specialize euler_coprime_weighted_product_cancel (m)
  2. L99
    specialize euler_coprime_weighted_product_cancel (x2)
  3. L100
    specialize euler_coprime_weighted_product_cancel (w)
  4. L101
    apply euler_coprime_weighted_product_cancel
  5. L102
    exact hm
  6. L103
    specialize euler_unit_product_coprime (m)
  7. L104
    specialize euler_unit_product_coprime (m)
  8. L105
    specialize euler_unit_product_coprime (x)
  9. L106
    specialize euler_unit_product_coprime (x1)
  10. L107
    specialize euler_unit_product_coprime (x2)
21Use earlier factsL108–111

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

  1. L108
    apply euler_unit_product_coprime
  2. L109
    exact hf_witness_witness
  3. L110
    exact hP_witness
  4. L111
    exact hbalance

Library-wide reading audit

Original exact command ledger · 111 lines
  1. 0001intro a
  2. 0002intro m
  3. 0003intro t
  4. 0004intro w
  5. 0005intro hm
  6. 0006intro ha
  7. 0007intro ht
  8. 0008intro hw
  9. 0009cases ht
  10. 0010have hf : exists b c. (forall eu_factor_index_endpoint_factors. (exists eut_gap_eu_endpoint_factors_index. eut_gap_eu_endpoint_factors_index + S (eu_factor_index_endpoint_factors) = (m)) -> exists eu_factor_value_endpoint_factors. (((exists fs_h_eu_endpoint_factors_at. fs_h_eu_endpoint_factors_at + S (eu_factor_value_endpoint_factors) = S ((S (eu_factor_index_endpoint_factors)) * c)) /\ exists fs_q_eu_endpoint_factors_at. b = fs_q_eu_endpoint_factors_at * S ((S (eu_factor_index_endpoint_factors)) * c) + (eu_factor_value_endpoint_factors))) /\ ((((forall eut_divisor_eu_endpoint_factors_choice_coprime. (exists eut_left_eu_endpoint_factors_choice_coprime. (eu_factor_index_endpoint_factors) = eut_divisor_eu_endpoint_factors_choice_coprime * eut_left_eu_endpoint_factors_choice_coprime) -> (exists eut_right_eu_endpoint_factors_choice_coprime. (m) = eut_divisor_eu_endpoint_factors_choice_coprime * eut_right_eu_endpoint_factors_choice_coprime) -> eut_divisor_eu_endpoint_factors_choice_coprime = 1) /\ (eu_factor_value_endpoint_factors)=(eu_factor_index_endpoint_factors)) \/ (~(forall eut_divisor_eu_endpoint_factors_choice_coprime. (exists eut_left_eu_endpoint_factors_choice_coprime. (eu_factor_index_endpoint_factors) = eut_divisor_eu_endpoint_factors_choice_coprime * eut_left_eu_endpoint_factors_choice_coprime) -> (exists eut_right_eu_endpoint_factors_choice_coprime. (m) = eut_divisor_eu_endpoint_factors_choice_coprime * eut_right_eu_endpoint_factors_choice_coprime) -> eut_divisor_eu_endpoint_factors_choice_coprime = 1) /\ (eu_factor_value_endpoint_factors)=1))))
  11. 0011specialize euler_unit_product_prefix_exists (m)
  12. 0012specialize euler_unit_product_prefix_exists (m)
  13. 0013apply euler_unit_product_prefix_exists
  14. 0014cases hf
  15. 0015cases hf_witness
  16. 0016have hP : exists P. (exists ff_u_fsat_eu_endpoint_product ff_v_fsat_eu_endpoint_product. ((((exists ff_h_fsat_eu_endpoint_product_start. ff_h_fsat_eu_endpoint_product_start + S (1) = S ((S (0)) * ff_v_fsat_eu_endpoint_product)) /\ exists ff_q_fsat_eu_endpoint_product_start. ff_u_fsat_eu_endpoint_product = ff_q_fsat_eu_endpoint_product_start * S ((S (0)) * ff_v_fsat_eu_endpoint_product) + (1))) /\ ((((exists ff_h_fsat_eu_endpoint_product_terminal. ff_h_fsat_eu_endpoint_product_terminal + S (P) = S ((S (m)) * ff_v_fsat_eu_endpoint_product)) /\ exists ff_q_fsat_eu_endpoint_product_terminal. ff_u_fsat_eu_endpoint_product = ff_q_fsat_eu_endpoint_product_terminal * S ((S (m)) * ff_v_fsat_eu_endpoint_product) + (P))) /\ forall ff_i_fsat_eu_endpoint_product. (exists ff_lt_fsat_eu_endpoint_product_bound. ff_lt_fsat_eu_endpoint_product_bound + S ff_i_fsat_eu_endpoint_product = m) -> exists ff_p_fsat_eu_endpoint_product ff_r_fsat_eu_endpoint_product ff_s_fsat_eu_endpoint_product. ((((exists ff_h_fsat_eu_endpoint_product_factor. ff_h_fsat_eu_endpoint_product_factor + S (ff_p_fsat_eu_endpoint_product) = S ((S (ff_i_fsat_eu_endpoint_product)) * x1)) /\ exists ff_q_fsat_eu_endpoint_product_factor. x = ff_q_fsat_eu_endpoint_product_factor * S ((S (ff_i_fsat_eu_endpoint_product)) * x1) + (ff_p_fsat_eu_endpoint_product))) /\ ((((exists ff_h_fsat_eu_endpoint_product_partial. ff_h_fsat_eu_endpoint_product_partial + S (ff_r_fsat_eu_endpoint_product) = S ((S (ff_i_fsat_eu_endpoint_product)) * ff_v_fsat_eu_endpoint_product)) /\ exists ff_q_fsat_eu_endpoint_product_partial. ff_u_fsat_eu_endpoint_product = ff_q_fsat_eu_endpoint_product_partial * S ((S (ff_i_fsat_eu_endpoint_product)) * ff_v_fsat_eu_endpoint_product) + (ff_r_fsat_eu_endpoint_product))) /\ ((((exists ff_h_fsat_eu_endpoint_product_successor. ff_h_fsat_eu_endpoint_product_successor + S (ff_s_fsat_eu_endpoint_product) = S ((S (S ff_i_fsat_eu_endpoint_product)) * ff_v_fsat_eu_endpoint_product)) /\ exists ff_q_fsat_eu_endpoint_product_successor. ff_u_fsat_eu_endpoint_product = ff_q_fsat_eu_endpoint_product_successor * S ((S (S ff_i_fsat_eu_endpoint_product)) * ff_v_fsat_eu_endpoint_product) + (ff_s_fsat_eu_endpoint_product))) /\ ff_s_fsat_eu_endpoint_product = ff_r_fsat_eu_endpoint_product * ff_p_fsat_eu_endpoint_product))))))
  17. 0017specialize beta_product_exists (x)
  18. 0018specialize beta_product_exists (x1)
  19. 0019specialize beta_product_exists (m)
  20. 0020apply beta_product_exists
  21. 0021cases hP
  22. 0022have hmap : exists r s. (forall eu_index_endpoint_map. (exists eut_gap_eu_endpoint_map_index. eut_gap_eu_endpoint_map_index + S (eu_index_endpoint_map) = (m)) -> exists eu_residue_endpoint_map. (((exists fs_h_eu_endpoint_map_at. fs_h_eu_endpoint_map_at + S (eu_residue_endpoint_map) = S ((S (eu_index_endpoint_map)) * s)) /\ exists fs_q_eu_endpoint_map_at. r = fs_q_eu_endpoint_map_at * S ((S (eu_index_endpoint_map)) * s) + (eu_residue_endpoint_map))) /\ ((exists eut_gap_eu_endpoint_map_bound. eut_gap_eu_endpoint_map_bound + S (eu_residue_endpoint_map) = (m)) /\ (exists eu_mod_left_endpoint_map_mod eu_mod_right_endpoint_map_mod. ((a)*eu_index_endpoint_map) + (m) * eu_mod_left_endpoint_map_mod = (eu_residue_endpoint_map) + (m) * eu_mod_right_endpoint_map_mod))) /\ (((forall fp_i_eu_endpoint_permutation_bounded. (exists fp_gap_eu_endpoint_permutation_bounded_index. fp_gap_eu_endpoint_permutation_bounded_index + S fp_i_eu_endpoint_permutation_bounded = m) -> exists fp_value_eu_endpoint_permutation_bounded. ((((exists ff_h_eu_endpoint_permutation_bounded_entry. ff_h_eu_endpoint_permutation_bounded_entry + S (fp_value_eu_endpoint_permutation_bounded) = S ((S (fp_i_eu_endpoint_permutation_bounded)) * s)) /\ exists ff_q_eu_endpoint_permutation_bounded_entry. r = ff_q_eu_endpoint_permutation_bounded_entry * S ((S (fp_i_eu_endpoint_permutation_bounded)) * s) + (fp_value_eu_endpoint_permutation_bounded))) /\ (exists fp_gap_eu_endpoint_permutation_bounded_value. fp_gap_eu_endpoint_permutation_bounded_value + S fp_value_eu_endpoint_permutation_bounded = m))) /\ ((forall fp_i_eu_endpoint_permutation_injective fp_j_eu_endpoint_permutation_injective fp_value_eu_endpoint_permutation_injective. (exists fp_gap_eu_endpoint_permutation_injective_i. fp_gap_eu_endpoint_permutation_injective_i + S fp_i_eu_endpoint_permutation_injective = m) -> (exists fp_gap_eu_endpoint_permutation_injective_j. fp_gap_eu_endpoint_permutation_injective_j + S fp_j_eu_endpoint_permutation_injective = m) -> (((exists ff_h_eu_endpoint_permutation_injective_left. ff_h_eu_endpoint_permutation_injective_left + S (fp_value_eu_endpoint_permutation_injective) = S ((S (fp_i_eu_endpoint_permutation_injective)) * s)) /\ exists ff_q_eu_endpoint_permutation_injective_left. r = ff_q_eu_endpoint_permutation_injective_left * S ((S (fp_i_eu_endpoint_permutation_injective)) * s) + (fp_value_eu_endpoint_permutation_injective))) -> (((exists ff_h_eu_endpoint_permutation_injective_right. ff_h_eu_endpoint_permutation_injective_right + S (fp_value_eu_endpoint_permutation_injective) = S ((S (fp_j_eu_endpoint_permutation_injective)) * s)) /\ exists ff_q_eu_endpoint_permutation_injective_right. r = ff_q_eu_endpoint_permutation_injective_right * S ((S (fp_j_eu_endpoint_permutation_injective)) * s) + (fp_value_eu_endpoint_permutation_injective))) -> fp_i_eu_endpoint_permutation_injective = fp_j_eu_endpoint_permutation_injective) /\ (forall fp_value_eu_endpoint_permutation_surjective. (exists fp_gap_eu_endpoint_permutation_surjective_value. fp_gap_eu_endpoint_permutation_surjective_value + S fp_value_eu_endpoint_permutation_surjective = m) -> exists fp_i_eu_endpoint_permutation_surjective. ((exists fp_gap_eu_endpoint_permutation_surjective_index. fp_gap_eu_endpoint_permutation_surjective_index + S fp_i_eu_endpoint_permutation_surjective = m) /\ (((exists ff_h_eu_endpoint_permutation_surjective_entry. ff_h_eu_endpoint_permutation_surjective_entry + S (fp_value_eu_endpoint_permutation_surjective) = S ((S (fp_i_eu_endpoint_permutation_surjective)) * s)) /\ exists ff_q_eu_endpoint_permutation_surjective_entry. r = ff_q_eu_endpoint_permutation_surjective_entry * S ((S (fp_i_eu_endpoint_permutation_surjective)) * s) + (fp_value_eu_endpoint_permutation_surjective))))))))
  23. 0023specialize euler_multiplier_permutation_exists (a)
  24. 0024specialize euler_multiplier_permutation_exists (m)
  25. 0025apply euler_multiplier_permutation_exists
  26. 0026exact hm
  27. 0027exact ha
  28. 0028cases hmap
  29. 0029cases hmap_witness
  30. 0030cases hmap_witness_witness
  31. 0031cases hmap_witness_witness_right
  32. 0032cases hmap_witness_witness_right_right
  33. 0033have hcomp : exists z d. (forall fms_i_eu_endpoint_composition fms_j_eu_endpoint_composition fms_v_eu_endpoint_composition. (exists fms_gap_eu_endpoint_composition. fms_gap_eu_endpoint_composition + S (fms_i_eu_endpoint_composition) = (m)) -> (((exists fs_h_fms_eu_endpoint_composition_index. fs_h_fms_eu_endpoint_composition_index + S (fms_j_eu_endpoint_composition) = S ((S (fms_i_eu_endpoint_composition)) * x4)) /\ exists fs_q_fms_eu_endpoint_composition_index. x3 = fs_q_fms_eu_endpoint_composition_index * S ((S (fms_i_eu_endpoint_composition)) * x4) + (fms_j_eu_endpoint_composition))) -> (((exists fs_h_fms_eu_endpoint_composition_source. fs_h_fms_eu_endpoint_composition_source + S (fms_v_eu_endpoint_composition) = S ((S (fms_j_eu_endpoint_composition)) * x1)) /\ exists fs_q_fms_eu_endpoint_composition_source. x = fs_q_fms_eu_endpoint_composition_source * S ((S (fms_j_eu_endpoint_composition)) * x1) + (fms_v_eu_endpoint_composition))) -> (((exists fs_h_fms_eu_endpoint_composition_target. fs_h_fms_eu_endpoint_composition_target + S (fms_v_eu_endpoint_composition) = S ((S (fms_i_eu_endpoint_composition)) * d)) /\ exists fs_q_fms_eu_endpoint_composition_target. z = fs_q_fms_eu_endpoint_composition_target * S ((S (fms_i_eu_endpoint_composition)) * d) + (fms_v_eu_endpoint_composition))))
  34. 0034specialize finite_beta_composition_exists (x3)
  35. 0035specialize finite_beta_composition_exists (x4)
  36. 0036specialize finite_beta_composition_exists (x)
  37. 0037specialize finite_beta_composition_exists (x1)
  38. 0038specialize finite_beta_composition_exists (m)
  39. 0039apply finite_beta_composition_exists
  40. 0040cases hcomp
  41. 0041cases hcomp_witness
  42. 0042have hQ : exists Q. (exists ff_u_fsat_eu_endpoint_target_product ff_v_fsat_eu_endpoint_target_product. ((((exists ff_h_fsat_eu_endpoint_target_product_start. ff_h_fsat_eu_endpoint_target_product_start + S (1) = S ((S (0)) * ff_v_fsat_eu_endpoint_target_product)) /\ exists ff_q_fsat_eu_endpoint_target_product_start. ff_u_fsat_eu_endpoint_target_product = ff_q_fsat_eu_endpoint_target_product_start * S ((S (0)) * ff_v_fsat_eu_endpoint_target_product) + (1))) /\ ((((exists ff_h_fsat_eu_endpoint_target_product_terminal. ff_h_fsat_eu_endpoint_target_product_terminal + S (Q) = S ((S (m)) * ff_v_fsat_eu_endpoint_target_product)) /\ exists ff_q_fsat_eu_endpoint_target_product_terminal. ff_u_fsat_eu_endpoint_target_product = ff_q_fsat_eu_endpoint_target_product_terminal * S ((S (m)) * ff_v_fsat_eu_endpoint_target_product) + (Q))) /\ forall ff_i_fsat_eu_endpoint_target_product. (exists ff_lt_fsat_eu_endpoint_target_product_bound. ff_lt_fsat_eu_endpoint_target_product_bound + S ff_i_fsat_eu_endpoint_target_product = m) -> exists ff_p_fsat_eu_endpoint_target_product ff_r_fsat_eu_endpoint_target_product ff_s_fsat_eu_endpoint_target_product. ((((exists ff_h_fsat_eu_endpoint_target_product_factor. ff_h_fsat_eu_endpoint_target_product_factor + S (ff_p_fsat_eu_endpoint_target_product) = S ((S (ff_i_fsat_eu_endpoint_target_product)) * x6)) /\ exists ff_q_fsat_eu_endpoint_target_product_factor. x5 = ff_q_fsat_eu_endpoint_target_product_factor * S ((S (ff_i_fsat_eu_endpoint_target_product)) * x6) + (ff_p_fsat_eu_endpoint_target_product))) /\ ((((exists ff_h_fsat_eu_endpoint_target_product_partial. ff_h_fsat_eu_endpoint_target_product_partial + S (ff_r_fsat_eu_endpoint_target_product) = S ((S (ff_i_fsat_eu_endpoint_target_product)) * ff_v_fsat_eu_endpoint_target_product)) /\ exists ff_q_fsat_eu_endpoint_target_product_partial. ff_u_fsat_eu_endpoint_target_product = ff_q_fsat_eu_endpoint_target_product_partial * S ((S (ff_i_fsat_eu_endpoint_target_product)) * ff_v_fsat_eu_endpoint_target_product) + (ff_r_fsat_eu_endpoint_target_product))) /\ ((((exists ff_h_fsat_eu_endpoint_target_product_successor. ff_h_fsat_eu_endpoint_target_product_successor + S (ff_s_fsat_eu_endpoint_target_product) = S ((S (S ff_i_fsat_eu_endpoint_target_product)) * ff_v_fsat_eu_endpoint_target_product)) /\ exists ff_q_fsat_eu_endpoint_target_product_successor. ff_u_fsat_eu_endpoint_target_product = ff_q_fsat_eu_endpoint_target_product_successor * S ((S (S ff_i_fsat_eu_endpoint_target_product)) * ff_v_fsat_eu_endpoint_target_product) + (ff_s_fsat_eu_endpoint_target_product))) /\ ff_s_fsat_eu_endpoint_target_product = ff_r_fsat_eu_endpoint_target_product * ff_p_fsat_eu_endpoint_target_product))))))
  43. 0043specialize beta_product_exists (x5)
  44. 0044specialize beta_product_exists (x6)
  45. 0045specialize beta_product_exists (m)
  46. 0046apply beta_product_exists
  47. 0047cases hQ
  48. 0048have he : x7=x2
  49. 0049symm
  50. 0050specialize beta_product_permutation_invariant (m)
  51. 0051specialize beta_product_permutation_invariant (x3)
  52. 0052specialize beta_product_permutation_invariant (x4)
  53. 0053specialize beta_product_permutation_invariant (x)
  54. 0054specialize beta_product_permutation_invariant (x1)
  55. 0055specialize beta_product_permutation_invariant (x5)
  56. 0056specialize beta_product_permutation_invariant (x6)
  57. 0057specialize beta_product_permutation_invariant (x2)
  58. 0058specialize beta_product_permutation_invariant (x7)
  59. 0059apply beta_product_permutation_invariant
  60. 0060exact hmap_witness_witness_right_left
  61. 0061exact hmap_witness_witness_right_right_left
  62. 0062exact hcomp_witness_witness
  63. 0063exact hP_witness
  64. 0064exact hQ_witness
  65. 0065have hs : forall eu_scale_index_endpoint_scaled eu_scale_source_endpoint_scaled eu_scale_target_endpoint_scaled. (exists eut_gap_eu_endpoint_scaled_index. eut_gap_eu_endpoint_scaled_index + S (eu_scale_index_endpoint_scaled) = (m)) -> (((exists fs_h_eu_endpoint_scaled_source. fs_h_eu_endpoint_scaled_source + S (eu_scale_source_endpoint_scaled) = S ((S (eu_scale_index_endpoint_scaled)) * x1)) /\ exists fs_q_eu_endpoint_scaled_source. x = fs_q_eu_endpoint_scaled_source * S ((S (eu_scale_index_endpoint_scaled)) * x1) + (eu_scale_source_endpoint_scaled))) -> (((exists fs_h_eu_endpoint_scaled_target. fs_h_eu_endpoint_scaled_target + S (eu_scale_target_endpoint_scaled) = S ((S (eu_scale_index_endpoint_scaled)) * x6)) /\ exists fs_q_eu_endpoint_scaled_target. x5 = fs_q_eu_endpoint_scaled_target * S ((S (eu_scale_index_endpoint_scaled)) * x6) + (eu_scale_target_endpoint_scaled))) -> (((forall eut_divisor_eu_endpoint_scaled_unit. (exists eut_left_eu_endpoint_scaled_unit. (eu_scale_index_endpoint_scaled) = eut_divisor_eu_endpoint_scaled_unit * eut_left_eu_endpoint_scaled_unit) -> (exists eut_right_eu_endpoint_scaled_unit. (m) = eut_divisor_eu_endpoint_scaled_unit * eut_right_eu_endpoint_scaled_unit) -> eut_divisor_eu_endpoint_scaled_unit = 1) -> (exists eu_mod_left_endpoint_scaled_scaled eu_mod_right_endpoint_scaled_scaled. ((a)*eu_scale_source_endpoint_scaled) + (m) * eu_mod_left_endpoint_scaled_scaled = (eu_scale_target_endpoint_scaled) + (m) * eu_mod_right_endpoint_scaled_scaled)) /\ (~(forall eut_divisor_eu_endpoint_scaled_unit. (exists eut_left_eu_endpoint_scaled_unit. (eu_scale_index_endpoint_scaled) = eut_divisor_eu_endpoint_scaled_unit * eut_left_eu_endpoint_scaled_unit) -> (exists eut_right_eu_endpoint_scaled_unit. (m) = eut_divisor_eu_endpoint_scaled_unit * eut_right_eu_endpoint_scaled_unit) -> eut_divisor_eu_endpoint_scaled_unit = 1) -> (exists eu_mod_left_endpoint_scaled_unchanged eu_mod_right_endpoint_scaled_unchanged. (eu_scale_source_endpoint_scaled) + (m) * eu_mod_left_endpoint_scaled_unchanged = (eu_scale_target_endpoint_scaled) + (m) * eu_mod_right_endpoint_scaled_unchanged)))
  66. 0066specialize euler_unit_product_reindex_scale (a)
  67. 0067specialize euler_unit_product_reindex_scale (m)
  68. 0068specialize euler_unit_product_reindex_scale (x3)
  69. 0069specialize euler_unit_product_reindex_scale (x4)
  70. 0070specialize euler_unit_product_reindex_scale (x)
  71. 0071specialize euler_unit_product_reindex_scale (x1)
  72. 0072specialize euler_unit_product_reindex_scale (x5)
  73. 0073specialize euler_unit_product_reindex_scale (x6)
  74. 0074apply euler_unit_product_reindex_scale
  75. 0075exact ha
  76. 0076exact hmap_witness_witness_left
  77. 0077exact hf_witness_witness
  78. 0078exact hcomp_witness_witness
  79. 0079have hbalance : exists eu_mod_left_endpoint_balance eu_mod_right_endpoint_balance. (w*x2) + (m) * eu_mod_left_endpoint_balance = (x7) + (m) * eu_mod_right_endpoint_balance
  80. 0080specialize euler_unit_count_product_balance (m)
  81. 0081specialize euler_unit_count_product_balance (a)
  82. 0082specialize euler_unit_count_product_balance (m)
  83. 0083specialize euler_unit_count_product_balance (x)
  84. 0084specialize euler_unit_count_product_balance (x1)
  85. 0085specialize euler_unit_count_product_balance (x5)
  86. 0086specialize euler_unit_count_product_balance (x6)
  87. 0087specialize euler_unit_count_product_balance (t)
  88. 0088specialize euler_unit_count_product_balance (x2)
  89. 0089specialize euler_unit_count_product_balance (x7)
  90. 0090specialize euler_unit_count_product_balance (w)
  91. 0091apply euler_unit_count_product_balance
  92. 0092exact ht_right
  93. 0093exact hs
  94. 0094exact hP_witness
  95. 0095exact hQ_witness
  96. 0096exact hw
  97. 0097rewrite he at hbalance
  98. 0098specialize euler_coprime_weighted_product_cancel (m)
  99. 0099specialize euler_coprime_weighted_product_cancel (x2)
  100. 0100specialize euler_coprime_weighted_product_cancel (w)
  101. 0101apply euler_coprime_weighted_product_cancel
  102. 0102exact hm
  103. 0103specialize euler_unit_product_coprime (m)
  104. 0104specialize euler_unit_product_coprime (m)
  105. 0105specialize euler_unit_product_coprime (x)
  106. 0106specialize euler_unit_product_coprime (x1)
  107. 0107specialize euler_unit_product_coprime (x2)
  108. 0108apply euler_unit_product_coprime
  109. 0109exact hf_witness_witness
  110. 0110exact hP_witness
  111. 0111exact hbalance