EU001E

euler_unit_count_product_balance

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

Induction on the actual independently counted zero-based unit prefix proves the exact power/product congruence; no Euler conclusion or unit-count oracle is a premise.

Exact expanded first-order arithmetic statement

forall l a m b c d e t P Q w. (exists eut_code_eu_balance_count eut_scale_eu_balance_count. (forall eut_index_eu_balance_count_mask. (exists eut_gap_eu_balance_count_mask_bound. eut_gap_eu_balance_count_mask_bound + S (eut_index_eu_balance_count_mask) = (l)) -> exists eut_bit_eu_balance_count_mask. (((exists fs_h_eut_eu_balance_count_mask_entry. fs_h_eut_eu_balance_count_mask_entry + S (eut_bit_eu_balance_count_mask) = S ((S (eut_index_eu_balance_count_mask)) * eut_scale_eu_balance_count)) /\ exists fs_q_eut_eu_balance_count_mask_entry. eut_code_eu_balance_count = fs_q_eut_eu_balance_count_mask_entry * S ((S (eut_index_eu_balance_count_mask)) * eut_scale_eu_balance_count) + (eut_bit_eu_balance_count_mask))) /\ ((((forall eut_divisor_eu_balance_count_mask_choice_coprime. (exists eut_left_eu_balance_count_mask_choice_coprime. (eut_index_eu_balance_count_mask) = eut_divisor_eu_balance_count_mask_choice_coprime * eut_left_eu_balance_count_mask_choice_coprime) -> (exists eut_right_eu_balance_count_mask_choice_coprime. (m) = eut_divisor_eu_balance_count_mask_choice_coprime * eut_right_eu_balance_count_mask_choice_coprime) -> eut_divisor_eu_balance_count_mask_choice_coprime = 1) /\ (eut_bit_eu_balance_count_mask) = 1) \/ (~(forall eut_divisor_eu_balance_count_mask_choice_coprime. (exists eut_left_eu_balance_count_mask_choice_coprime. (eut_index_eu_balance_count_mask) = eut_divisor_eu_balance_count_mask_choice_coprime * eut_left_eu_balance_count_mask_choice_coprime) -> (exists eut_right_eu_balance_count_mask_choice_coprime. (m) = eut_divisor_eu_balance_count_mask_choice_coprime * eut_right_eu_balance_count_mask_choice_coprime) -> eut_divisor_eu_balance_count_mask_choice_coprime = 1) /\ (eut_bit_eu_balance_count_mask) = 0)))) /\ (exists fs_u_eut_eu_balance_count_sum fs_v_eut_eu_balance_count_sum. ((((exists fs_h_eut_eu_balance_count_sum_body_start. fs_h_eut_eu_balance_count_sum_body_start + S (0) = S ((S (0)) * fs_v_eut_eu_balance_count_sum)) /\ exists fs_q_eut_eu_balance_count_sum_body_start. fs_u_eut_eu_balance_count_sum = fs_q_eut_eu_balance_count_sum_body_start * S ((S (0)) * fs_v_eut_eu_balance_count_sum) + (0))) /\ ((((exists fs_h_eut_eu_balance_count_sum_body_terminal. fs_h_eut_eu_balance_count_sum_body_terminal + S (t) = S ((S (l)) * fs_v_eut_eu_balance_count_sum)) /\ exists fs_q_eut_eu_balance_count_sum_body_terminal. fs_u_eut_eu_balance_count_sum = fs_q_eut_eu_balance_count_sum_body_terminal * S ((S (l)) * fs_v_eut_eu_balance_count_sum) + (t))) /\ forall fs_i_eut_eu_balance_count_sum_body_steps. (exists fs_lt_eut_eu_balance_count_sum_body_steps_bound. fs_lt_eut_eu_balance_count_sum_body_steps_bound + S fs_i_eut_eu_balance_count_sum_body_steps = l) -> exists fs_a_eut_eu_balance_count_sum_body_steps fs_r_eut_eu_balance_count_sum_body_steps fs_s_eut_eu_balance_count_sum_body_steps. ((((exists fs_h_eut_eu_balance_count_sum_body_steps_summand. fs_h_eut_eu_balance_count_sum_body_steps_summand + S (fs_a_eut_eu_balance_count_sum_body_steps) = S ((S (fs_i_eut_eu_balance_count_sum_body_steps)) * eut_scale_eu_balance_count)) /\ exists fs_q_eut_eu_balance_count_sum_body_steps_summand. eut_code_eu_balance_count = fs_q_eut_eu_balance_count_sum_body_steps_summand * S ((S (fs_i_eut_eu_balance_count_sum_body_steps)) * eut_scale_eu_balance_count) + (fs_a_eut_eu_balance_count_sum_body_steps))) /\ ((((exists fs_h_eut_eu_balance_count_sum_body_steps_partial. fs_h_eut_eu_balance_count_sum_body_steps_partial + S (fs_r_eut_eu_balance_count_sum_body_steps) = S ((S (fs_i_eut_eu_balance_count_sum_body_steps)) * fs_v_eut_eu_balance_count_sum)) /\ exists fs_q_eut_eu_balance_count_sum_body_steps_partial. fs_u_eut_eu_balance_count_sum = fs_q_eut_eu_balance_count_sum_body_steps_partial * S ((S (fs_i_eut_eu_balance_count_sum_body_steps)) * fs_v_eut_eu_balance_count_sum) + (fs_r_eut_eu_balance_count_sum_body_steps))) /\ ((((exists fs_h_eut_eu_balance_count_sum_body_steps_successor. fs_h_eut_eu_balance_count_sum_body_steps_successor + S (fs_s_eut_eu_balance_count_sum_body_steps) = S ((S (S fs_i_eut_eu_balance_count_sum_body_steps)) * fs_v_eut_eu_balance_count_sum)) /\ exists fs_q_eut_eu_balance_count_sum_body_steps_successor. fs_u_eut_eu_balance_count_sum = fs_q_eut_eu_balance_count_sum_body_steps_successor * S ((S (S fs_i_eut_eu_balance_count_sum_body_steps)) * fs_v_eut_eu_balance_count_sum) + (fs_s_eut_eu_balance_count_sum_body_steps))) /\ fs_s_eut_eu_balance_count_sum_body_steps = fs_r_eut_eu_balance_count_sum_body_steps + fs_a_eut_eu_balance_count_sum_body_steps))))))) -> (forall eu_scale_index_balance_scale eu_scale_source_balance_scale eu_scale_target_balance_scale. (exists eut_gap_eu_balance_scale_index. eut_gap_eu_balance_scale_index + S (eu_scale_index_balance_scale) = (l)) -> (((exists fs_h_eu_balance_scale_source. fs_h_eu_balance_scale_source + S (eu_scale_source_balance_scale) = S ((S (eu_scale_index_balance_scale)) * c)) /\ exists fs_q_eu_balance_scale_source. b = fs_q_eu_balance_scale_source * S ((S (eu_scale_index_balance_scale)) * c) + (eu_scale_source_balance_scale))) -> (((exists fs_h_eu_balance_scale_target. fs_h_eu_balance_scale_target + S (eu_scale_target_balance_scale) = S ((S (eu_scale_index_balance_scale)) * e)) /\ exists fs_q_eu_balance_scale_target. d = fs_q_eu_balance_scale_target * S ((S (eu_scale_index_balance_scale)) * e) + (eu_scale_target_balance_scale))) -> (((forall eut_divisor_eu_balance_scale_unit. (exists eut_left_eu_balance_scale_unit. (eu_scale_index_balance_scale) = eut_divisor_eu_balance_scale_unit * eut_left_eu_balance_scale_unit) -> (exists eut_right_eu_balance_scale_unit. (m) = eut_divisor_eu_balance_scale_unit * eut_right_eu_balance_scale_unit) -> eut_divisor_eu_balance_scale_unit = 1) -> (exists eu_mod_left_balance_scale_scaled eu_mod_right_balance_scale_scaled. ((a)*eu_scale_source_balance_scale) + (m) * eu_mod_left_balance_scale_scaled = (eu_scale_target_balance_scale) + (m) * eu_mod_right_balance_scale_scaled)) /\ (~(forall eut_divisor_eu_balance_scale_unit. (exists eut_left_eu_balance_scale_unit. (eu_scale_index_balance_scale) = eut_divisor_eu_balance_scale_unit * eut_left_eu_balance_scale_unit) -> (exists eut_right_eu_balance_scale_unit. (m) = eut_divisor_eu_balance_scale_unit * eut_right_eu_balance_scale_unit) -> eut_divisor_eu_balance_scale_unit = 1) -> (exists eu_mod_left_balance_scale_unchanged eu_mod_right_balance_scale_unchanged. (eu_scale_source_balance_scale) + (m) * eu_mod_left_balance_scale_unchanged = (eu_scale_target_balance_scale) + (m) * eu_mod_right_balance_scale_unchanged)))) -> (exists ff_u_fsat_eu_balance_source ff_v_fsat_eu_balance_source. ((((exists ff_h_fsat_eu_balance_source_start. ff_h_fsat_eu_balance_source_start + S (1) = S ((S (0)) * ff_v_fsat_eu_balance_source)) /\ exists ff_q_fsat_eu_balance_source_start. ff_u_fsat_eu_balance_source = ff_q_fsat_eu_balance_source_start * S ((S (0)) * ff_v_fsat_eu_balance_source) + (1))) /\ ((((exists ff_h_fsat_eu_balance_source_terminal. ff_h_fsat_eu_balance_source_terminal + S (P) = S ((S (l)) * ff_v_fsat_eu_balance_source)) /\ exists ff_q_fsat_eu_balance_source_terminal. ff_u_fsat_eu_balance_source = ff_q_fsat_eu_balance_source_terminal * S ((S (l)) * ff_v_fsat_eu_balance_source) + (P))) /\ forall ff_i_fsat_eu_balance_source. (exists ff_lt_fsat_eu_balance_source_bound. ff_lt_fsat_eu_balance_source_bound + S ff_i_fsat_eu_balance_source = l) -> exists ff_p_fsat_eu_balance_source ff_r_fsat_eu_balance_source ff_s_fsat_eu_balance_source. ((((exists ff_h_fsat_eu_balance_source_factor. ff_h_fsat_eu_balance_source_factor + S (ff_p_fsat_eu_balance_source) = S ((S (ff_i_fsat_eu_balance_source)) * c)) /\ exists ff_q_fsat_eu_balance_source_factor. b = ff_q_fsat_eu_balance_source_factor * S ((S (ff_i_fsat_eu_balance_source)) * c) + (ff_p_fsat_eu_balance_source))) /\ ((((exists ff_h_fsat_eu_balance_source_partial. ff_h_fsat_eu_balance_source_partial + S (ff_r_fsat_eu_balance_source) = S ((S (ff_i_fsat_eu_balance_source)) * ff_v_fsat_eu_balance_source)) /\ exists ff_q_fsat_eu_balance_source_partial. ff_u_fsat_eu_balance_source = ff_q_fsat_eu_balance_source_partial * S ((S (ff_i_fsat_eu_balance_source)) * ff_v_fsat_eu_balance_source) + (ff_r_fsat_eu_balance_source))) /\ ((((exists ff_h_fsat_eu_balance_source_successor. ff_h_fsat_eu_balance_source_successor + S (ff_s_fsat_eu_balance_source) = S ((S (S ff_i_fsat_eu_balance_source)) * ff_v_fsat_eu_balance_source)) /\ exists ff_q_fsat_eu_balance_source_successor. ff_u_fsat_eu_balance_source = ff_q_fsat_eu_balance_source_successor * S ((S (S ff_i_fsat_eu_balance_source)) * ff_v_fsat_eu_balance_source) + (ff_s_fsat_eu_balance_source))) /\ ff_s_fsat_eu_balance_source = ff_r_fsat_eu_balance_source * ff_p_fsat_eu_balance_source)))))) -> (exists ff_u_fsat_eu_balance_target ff_v_fsat_eu_balance_target. ((((exists ff_h_fsat_eu_balance_target_start. ff_h_fsat_eu_balance_target_start + S (1) = S ((S (0)) * ff_v_fsat_eu_balance_target)) /\ exists ff_q_fsat_eu_balance_target_start. ff_u_fsat_eu_balance_target = ff_q_fsat_eu_balance_target_start * S ((S (0)) * ff_v_fsat_eu_balance_target) + (1))) /\ ((((exists ff_h_fsat_eu_balance_target_terminal. ff_h_fsat_eu_balance_target_terminal + S (Q) = S ((S (l)) * ff_v_fsat_eu_balance_target)) /\ exists ff_q_fsat_eu_balance_target_terminal. ff_u_fsat_eu_balance_target = ff_q_fsat_eu_balance_target_terminal * S ((S (l)) * ff_v_fsat_eu_balance_target) + (Q))) /\ forall ff_i_fsat_eu_balance_target. (exists ff_lt_fsat_eu_balance_target_bound. ff_lt_fsat_eu_balance_target_bound + S ff_i_fsat_eu_balance_target = l) -> exists ff_p_fsat_eu_balance_target ff_r_fsat_eu_balance_target ff_s_fsat_eu_balance_target. ((((exists ff_h_fsat_eu_balance_target_factor. ff_h_fsat_eu_balance_target_factor + S (ff_p_fsat_eu_balance_target) = S ((S (ff_i_fsat_eu_balance_target)) * e)) /\ exists ff_q_fsat_eu_balance_target_factor. d = ff_q_fsat_eu_balance_target_factor * S ((S (ff_i_fsat_eu_balance_target)) * e) + (ff_p_fsat_eu_balance_target))) /\ ((((exists ff_h_fsat_eu_balance_target_partial. ff_h_fsat_eu_balance_target_partial + S (ff_r_fsat_eu_balance_target) = S ((S (ff_i_fsat_eu_balance_target)) * ff_v_fsat_eu_balance_target)) /\ exists ff_q_fsat_eu_balance_target_partial. ff_u_fsat_eu_balance_target = ff_q_fsat_eu_balance_target_partial * S ((S (ff_i_fsat_eu_balance_target)) * ff_v_fsat_eu_balance_target) + (ff_r_fsat_eu_balance_target))) /\ ((((exists ff_h_fsat_eu_balance_target_successor. ff_h_fsat_eu_balance_target_successor + S (ff_s_fsat_eu_balance_target) = S ((S (S ff_i_fsat_eu_balance_target)) * ff_v_fsat_eu_balance_target)) /\ exists ff_q_fsat_eu_balance_target_successor. ff_u_fsat_eu_balance_target = ff_q_fsat_eu_balance_target_successor * S ((S (S ff_i_fsat_eu_balance_target)) * ff_v_fsat_eu_balance_target) + (ff_s_fsat_eu_balance_target))) /\ ff_s_fsat_eu_balance_target = ff_r_fsat_eu_balance_target * ff_p_fsat_eu_balance_target)))))) -> (exists pa_b_euta_eu_balance_power pa_c_euta_eu_balance_power. ((forall pa_i_euta_eu_balance_power_repeat. (exists pa_lt_euta_eu_balance_power_repeat_bound. pa_lt_euta_eu_balance_power_repeat_bound + S pa_i_euta_eu_balance_power_repeat = t) -> (((exists pa_h_euta_eu_balance_power_repeat_decoded. pa_h_euta_eu_balance_power_repeat_decoded + S (a) = S ((S (pa_i_euta_eu_balance_power_repeat)) * pa_c_euta_eu_balance_power)) /\ exists pa_q_euta_eu_balance_power_repeat_decoded. pa_b_euta_eu_balance_power = pa_q_euta_eu_balance_power_repeat_decoded * S ((S (pa_i_euta_eu_balance_power_repeat)) * pa_c_euta_eu_balance_power) + (a)))) /\ (exists pa_u_euta_eu_balance_power_product pa_v_euta_eu_balance_power_product. ((((exists pa_h_euta_eu_balance_power_product_start. pa_h_euta_eu_balance_power_product_start + S (1) = S ((S (0)) * pa_v_euta_eu_balance_power_product)) /\ exists pa_q_euta_eu_balance_power_product_start. pa_u_euta_eu_balance_power_product = pa_q_euta_eu_balance_power_product_start * S ((S (0)) * pa_v_euta_eu_balance_power_product) + (1))) /\ ((((exists pa_h_euta_eu_balance_power_product_terminal. pa_h_euta_eu_balance_power_product_terminal + S (w) = S ((S (t)) * pa_v_euta_eu_balance_power_product)) /\ exists pa_q_euta_eu_balance_power_product_terminal. pa_u_euta_eu_balance_power_product = pa_q_euta_eu_balance_power_product_terminal * S ((S (t)) * pa_v_euta_eu_balance_power_product) + (w))) /\ forall pa_i_euta_eu_balance_power_product. (exists pa_lt_euta_eu_balance_power_product_bound. pa_lt_euta_eu_balance_power_product_bound + S pa_i_euta_eu_balance_power_product = t) -> exists pa_p_euta_eu_balance_power_product pa_r_euta_eu_balance_power_product pa_s_euta_eu_balance_power_product. ((((exists pa_h_euta_eu_balance_power_product_factor. pa_h_euta_eu_balance_power_product_factor + S (pa_p_euta_eu_balance_power_product) = S ((S (pa_i_euta_eu_balance_power_product)) * pa_c_euta_eu_balance_power)) /\ exists pa_q_euta_eu_balance_power_product_factor. pa_b_euta_eu_balance_power = pa_q_euta_eu_balance_power_product_factor * S ((S (pa_i_euta_eu_balance_power_product)) * pa_c_euta_eu_balance_power) + (pa_p_euta_eu_balance_power_product))) /\ ((((exists pa_h_euta_eu_balance_power_product_partial. pa_h_euta_eu_balance_power_product_partial + S (pa_r_euta_eu_balance_power_product) = S ((S (pa_i_euta_eu_balance_power_product)) * pa_v_euta_eu_balance_power_product)) /\ exists pa_q_euta_eu_balance_power_product_partial. pa_u_euta_eu_balance_power_product = pa_q_euta_eu_balance_power_product_partial * S ((S (pa_i_euta_eu_balance_power_product)) * pa_v_euta_eu_balance_power_product) + (pa_r_euta_eu_balance_power_product))) /\ ((((exists pa_h_euta_eu_balance_power_product_successor. pa_h_euta_eu_balance_power_product_successor + S (pa_s_euta_eu_balance_power_product) = S ((S (S pa_i_euta_eu_balance_power_product)) * pa_v_euta_eu_balance_power_product)) /\ exists pa_q_euta_eu_balance_power_product_successor. pa_u_euta_eu_balance_power_product = pa_q_euta_eu_balance_power_product_successor * S ((S (S pa_i_euta_eu_balance_power_product)) * pa_v_euta_eu_balance_power_product) + (pa_s_euta_eu_balance_power_product))) /\ pa_s_euta_eu_balance_power_product = pa_r_euta_eu_balance_power_product * pa_p_euta_eu_balance_power_product)))))))) -> (exists eu_mod_left_balance_result eu_mod_right_balance_result. (w*P) + (m) * eu_mod_left_balance_result = (Q) + (m) * eu_mod_right_balance_result)

Constructive proof overview

Generated structural guide

Induction on the actual independently counted zero-based unit prefix proves the exact power/product congruence; no Euler conclusion or unit-count oracle is a premise.

The unchanged tactic script uses 15 declared prerequisites and contains 208 exact native proof lines.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

Proof neighborhood

Direct dependencies

totient_unit_count_zero_length Alpha theorem; checked-use authorized pow_zero Alpha theorem; checked-use authorized beta_product_zero Alpha theorem; checked-use authorized one_mul Alpha theorem; checked-use authorized mod_eq_refl Alpha theorem; checked-use authorized totient_unit_count_succ_decompose Alpha theorem; checked-use authorized beta_product_succ_decompose Alpha theorem; checked-use authorized pow_exists Alpha theorem; checked-use authorized EU001A euler_unit_scaled_prefix_drop_last le_refl Alpha theorem; checked-use authorized pow_successor_pair_mul Alpha theorem; checked-use authorized mul_shuffle_four Alpha theorem; checked-use authorized mod_eq_mul Alpha theorem; checked-use authorized pow_functional Alpha theorem; checked-use authorized mul_assoc Alpha theorem; checked-use authorized

Direct dependents

EU001F euler_coprime_totient_power_value

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. The literal dependency-closed bundle is checked by original HA and the independently compiled Lean verifier. Public delivery grants no Alpha checked-use authority or Stable membership.

Read the argument

Proof checkpoints

208 script commands · 31 reading checkpoints · 17 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 (1)
euler unit scaled prefix drop last

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.

01Induction on lL1–10

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

  1. L1
    induction l
  2. L2
    intro a
  3. L3
    intro m
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro d
  7. L7
    intro e
  8. L8
    intro t
  9. L9
    intro P
  10. L10
    intro Q
02Fix variables and assumptionsL11–16

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

  1. L11
    intro w
  2. L12
    intro ht
  3. L13
    intro hs
  4. L14
    intro hP
  5. L15
    intro hQ
  6. L16
    intro hw
03Establish ht0L17–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply totient unit count zero length.

  1. L17
    have ht0 : t=0
  2. L18
    specialize totient_unit_count_zero_length (m)
  3. L19
    specialize totient_unit_count_zero_length (t)
  4. L20
    apply totient_unit_count_zero_length
  5. L21
    exact ht
04Establish hw1L22–28

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

  1. L22
    have hw1 : w=1
  2. L23
    specialize pow_zero (a)
  3. L24
    specialize pow_zero (t)
  4. L25
    specialize pow_zero (w)
  5. L26
    apply pow_zero
  6. L27
    exact ht0
  7. L28
    exact hw
05Establish hP1L29–34

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

  1. L29
    have hP1 : P=1
  2. L30
    specialize beta_product_zero (b)
  3. L31
    specialize beta_product_zero (c)
  4. L32
    specialize beta_product_zero (P)
  5. L33
    apply beta_product_zero
  6. L34
    exact hP
06Establish hQ1L35–41

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

  1. L35
    have hQ1 : Q=1
  2. L36
    specialize beta_product_zero (d)
  3. L37
    specialize beta_product_zero (e)
  4. L38
    specialize beta_product_zero (Q)
  5. L39
    apply beta_product_zero
  6. L40
    exact hQ
  7. L41
    rewrite hw1
07Establish heL42–51

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

  1. L42
    have he : 1*P=P
  2. L43
    specialize one_mul (P)
  3. L44
    apply one_mul
  4. L45
    rewrite he
  5. L46
    rewrite hP1
  6. L47
    rewrite hQ1
  7. L48
    specialize mod_eq_refl (m)
  8. L49
    specialize mod_eq_refl (1)
  9. L50
    apply mod_eq_refl
  10. L51
    intro a
08Fix variables and assumptionsL52–61

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

  1. L52
    intro m
  2. L53
    intro b
  3. L54
    intro c
  4. L55
    intro d
  5. L56
    intro e
  6. L57
    intro t
  7. L58
    intro P
  8. L59
    intro Q
  9. L60
    intro w
  10. L61
    intro ht
09Fix variables and assumptionsL62–65

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

  1. L62
    intro hs
  2. L63
    intro hP
  3. L64
    intro hQ
  4. L65
    intro hw
10Establish hcL66–71

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply totient unit count succ decompose.

  1. L66
    have hc : ∃ r. ∃ f. UnitCount(m,l,r) ∧ ((Coprime(l,m) ∧ f = 1 ∨ ¬Coprime(l,m) ∧ f = 0) ∧ t = r + f)Definitions: UnitCountCoprime
  2. L67
    specialize totient_unit_count_succ_decompose (m)
  3. L68
    specialize totient_unit_count_succ_decompose (l)
  4. L69
    specialize totient_unit_count_succ_decompose (t)
  5. L70
    apply totient_unit_count_succ_decompose
  6. L71
    exact ht
11Separate the logical casesL72–75

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

  1. L72
    cases hc
  2. L73
    cases hc_witness
  3. L74
    cases hc_witness_witness
  4. L75
    cases hc_witness_witness_right
12Establish hpL76–82

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

  1. L76
    have hp : ∃ v. ∃ R. BetaAt(b,c,l,v) ∧ (Product(b,c,l,R) ∧ P = R · v)Definitions: BetaAtProduct
  2. L77
    specialize beta_product_succ_decompose (b)
  3. L78
    specialize beta_product_succ_decompose (c)
  4. L79
    specialize beta_product_succ_decompose (l)
  5. L80
    specialize beta_product_succ_decompose (P)
  6. L81
    apply beta_product_succ_decompose
  7. L82
    exact hP
13Separate the logical casesL83–86

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

  1. L83
    cases hp
  2. L84
    cases hp_witness
  3. L85
    cases hp_witness_witness
  4. L86
    cases hp_witness_witness_right
14Establish hqL87–93

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

  1. L87
    have hq : ∃ v. ∃ R. BetaAt(d,e,l,v) ∧ (Product(d,e,l,R) ∧ Q = R · v)Definitions: BetaAtProduct
  2. L88
    specialize beta_product_succ_decompose (d)
  3. L89
    specialize beta_product_succ_decompose (e)
  4. L90
    specialize beta_product_succ_decompose (l)
  5. L91
    specialize beta_product_succ_decompose (Q)
  6. L92
    apply beta_product_succ_decompose
  7. L93
    exact hQ
15Separate the logical casesL94–97

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

  1. L94
    cases hq
  2. L95
    cases hq_witness
  3. L96
    cases hq_witness_witness
  4. L97
    cases hq_witness_witness_right
16Establish hzL98–101

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

  1. L98
    have hz : ∃ z. Pow(a,x,z)Definitions: Pow
  2. L99
    specialize pow_exists (a)
  3. L100
    specialize pow_exists (x)
  4. L101
    apply pow_exists
17Separate the logical casesL102–102

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

  1. L102
    cases hz
18Establish hpreviousL103–112

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

  1. L103
    have hprevious : exists eu_mod_left_balance_previous eu_mod_right_balance_previous. (x6*x3) + (m) * eu_mod_left_balance_previous = (x5) + (m) * eu_mod_right_balance_previous
  2. L104
    specialize IH (a)
  3. L105
    specialize IH (m)
  4. L106
    specialize IH (b)
  5. L107
    specialize IH (c)
  6. L108
    specialize IH (d)
  7. L109
    specialize IH (e)
  8. L110
    specialize IH (x)
  9. L111
    specialize IH (x3)
  10. L112
    specialize IH (x5)
19Use earlier factsL113–122

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

  1. L113
    specialize IH (x6)
  2. L114
    apply IH
  3. L115
    exact hc_witness_witness_left
  4. L116
    specialize euler_unit_scaled_prefix_drop_last (a)
  5. L117
    specialize euler_unit_scaled_prefix_drop_last (m)
  6. L118
    specialize euler_unit_scaled_prefix_drop_last (b)
  7. L119
    specialize euler_unit_scaled_prefix_drop_last (c)
  8. L120
    specialize euler_unit_scaled_prefix_drop_last (d)
  9. L121
    specialize euler_unit_scaled_prefix_drop_last (e)
  10. L122
    specialize euler_unit_scaled_prefix_drop_last (l)
20Use earlier factsL123–127

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

  1. L123
    apply euler_unit_scaled_prefix_drop_last
  2. L124
    exact hs
  3. L125
    exact hp_witness_witness_right_left
  4. L126
    exact hq_witness_witness_right_left
  5. L127
    exact hz_witness
21Establish hstepL128–136

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

  1. L128
    have hstep : (Coprime(l,m) → ModEq(m,a · x2,x4)) ∧ (¬Coprime(l,m) → ModEq(m,x2,x4))Definitions: CoprimeModEq
  2. L129
    specialize hs (l)
  3. L130
    specialize hs (x2)
  4. L131
    specialize hs (x4)
  5. L132
    apply hs
  6. L133
    specialize le_refl (S l)
  7. L134
    apply le_refl
  8. L135
    exact hp_witness_witness_left
  9. L136
    exact hq_witness_witness_left
22Separate the logical casesL137–139

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

  1. L137
    cases hstep
  2. L138
    cases hc_witness_witness_right_left
  3. L139
    cases hc_witness_witness_right_left_left
23Establish htexpL140–143

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

  1. L140
    have htexp : t=S x
  2. L141
    rewrite hc_witness_witness_right_right
  3. L142
    rewrite hc_witness_witness_right_left_left_right
  4. L143
    simp
24Establish hwpL144–153

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor pair mul.

  1. L144
    have hwp : w=x6*a
  2. L145
    specialize pow_successor_pair_mul (a)
  3. L146
    specialize pow_successor_pair_mul (x)
  4. L147
    specialize pow_successor_pair_mul (t)
  5. L148
    specialize pow_successor_pair_mul (x6)
  6. L149
    specialize pow_successor_pair_mul (w)
  7. L150
    apply pow_successor_pair_mul
  8. L151
    exact htexp
  9. L152
    exact hz_witness
  10. L153
    exact hw
25Establish hproductL154–163

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

  1. L154
    have hproduct : w*P=(x6*x3)*(a*x2)
  2. L155
    rewrite hwp
  3. L156
    rewrite hp_witness_witness_right_right
  4. L157
    specialize mul_shuffle_four (x6)
  5. L158
    specialize mul_shuffle_four (a)
  6. L159
    specialize mul_shuffle_four (x3)
  7. L160
    specialize mul_shuffle_four (x2)
  8. L161
    apply mul_shuffle_four
  9. L162
    rewrite hproduct
  10. L163
    rewrite hq_witness_witness_right_right
26Use earlier factsL164–172

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

  1. L164
    specialize mod_eq_mul (m)
  2. L165
    specialize mod_eq_mul (x6*x3)
  3. L166
    specialize mod_eq_mul (x5)
  4. L167
    specialize mod_eq_mul (a*x2)
  5. L168
    specialize mod_eq_mul (x4)
  6. L169
    apply mod_eq_mul
  7. L170
    exact hprevious
  8. L171
    apply hstep_left
  9. L172
    exact hc_witness_witness_right_left_left_left
27Separate the logical casesL173–173

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

  1. L173
    cases hc_witness_witness_right_left_right
28Establish htexpL174–181

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

  1. L174
    have htexp : t=x
  2. L175
    rewrite hc_witness_witness_right_right
  3. L176
    rewrite hc_witness_witness_right_left_right_right
  4. L177
    simp
  5. L178
    rewrite htexp at hw
  6. L179
    rewrite htexp at hw
  7. L180
    rewrite htexp at hw
  8. L181
    rewrite htexp at hw
29Establish hwpL182–189

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

  1. L182
    have hwp : w=x6
  2. L183
    specialize pow_functional (a)
  3. L184
    specialize pow_functional (x)
  4. L185
    specialize pow_functional (w)
  5. L186
    specialize pow_functional (x6)
  6. L187
    apply pow_functional
  7. L188
    exact hw
  8. L189
    exact hz_witness
30Establish hproductL190–199

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

  1. L190
    have hproduct : w*P=(x6*x3)*x2
  2. L191
    rewrite hwp
  3. L192
    rewrite hp_witness_witness_right_right
  4. L193
    symm
  5. L194
    specialize mul_assoc (x6)
  6. L195
    specialize mul_assoc (x3)
  7. L196
    specialize mul_assoc (x2)
  8. L197
    apply mul_assoc
  9. L198
    rewrite hproduct
  10. L199
    rewrite hq_witness_witness_right_right
31Use earlier factsL200–208

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

  1. L200
    specialize mod_eq_mul (m)
  2. L201
    specialize mod_eq_mul (x6*x3)
  3. L202
    specialize mod_eq_mul (x5)
  4. L203
    specialize mod_eq_mul (x2)
  5. L204
    specialize mod_eq_mul (x4)
  6. L205
    apply mod_eq_mul
  7. L206
    exact hprevious
  8. L207
    apply hstep_right
  9. L208
    exact hc_witness_witness_right_left_right_left

Library-wide reading audit

Original exact command ledger · 208 lines
  1. 0001induction l
  2. 0002intro a
  3. 0003intro m
  4. 0004intro b
  5. 0005intro c
  6. 0006intro d
  7. 0007intro e
  8. 0008intro t
  9. 0009intro P
  10. 0010intro Q
  11. 0011intro w
  12. 0012intro ht
  13. 0013intro hs
  14. 0014intro hP
  15. 0015intro hQ
  16. 0016intro hw
  17. 0017have ht0 : t=0
  18. 0018specialize totient_unit_count_zero_length (m)
  19. 0019specialize totient_unit_count_zero_length (t)
  20. 0020apply totient_unit_count_zero_length
  21. 0021exact ht
  22. 0022have hw1 : w=1
  23. 0023specialize pow_zero (a)
  24. 0024specialize pow_zero (t)
  25. 0025specialize pow_zero (w)
  26. 0026apply pow_zero
  27. 0027exact ht0
  28. 0028exact hw
  29. 0029have hP1 : P=1
  30. 0030specialize beta_product_zero (b)
  31. 0031specialize beta_product_zero (c)
  32. 0032specialize beta_product_zero (P)
  33. 0033apply beta_product_zero
  34. 0034exact hP
  35. 0035have hQ1 : Q=1
  36. 0036specialize beta_product_zero (d)
  37. 0037specialize beta_product_zero (e)
  38. 0038specialize beta_product_zero (Q)
  39. 0039apply beta_product_zero
  40. 0040exact hQ
  41. 0041rewrite hw1
  42. 0042have he : 1*P=P
  43. 0043specialize one_mul (P)
  44. 0044apply one_mul
  45. 0045rewrite he
  46. 0046rewrite hP1
  47. 0047rewrite hQ1
  48. 0048specialize mod_eq_refl (m)
  49. 0049specialize mod_eq_refl (1)
  50. 0050apply mod_eq_refl
  51. 0051intro a
  52. 0052intro m
  53. 0053intro b
  54. 0054intro c
  55. 0055intro d
  56. 0056intro e
  57. 0057intro t
  58. 0058intro P
  59. 0059intro Q
  60. 0060intro w
  61. 0061intro ht
  62. 0062intro hs
  63. 0063intro hP
  64. 0064intro hQ
  65. 0065intro hw
  66. 0066have hc : exists r f. (exists eut_code_eu_balance_previous_count eut_scale_eu_balance_previous_count. (forall eut_index_eu_balance_previous_count_mask. (exists eut_gap_eu_balance_previous_count_mask_bound. eut_gap_eu_balance_previous_count_mask_bound + S (eut_index_eu_balance_previous_count_mask) = (l)) -> exists eut_bit_eu_balance_previous_count_mask. (((exists fs_h_eut_eu_balance_previous_count_mask_entry. fs_h_eut_eu_balance_previous_count_mask_entry + S (eut_bit_eu_balance_previous_count_mask) = S ((S (eut_index_eu_balance_previous_count_mask)) * eut_scale_eu_balance_previous_count)) /\ exists fs_q_eut_eu_balance_previous_count_mask_entry. eut_code_eu_balance_previous_count = fs_q_eut_eu_balance_previous_count_mask_entry * S ((S (eut_index_eu_balance_previous_count_mask)) * eut_scale_eu_balance_previous_count) + (eut_bit_eu_balance_previous_count_mask))) /\ ((((forall eut_divisor_eu_balance_previous_count_mask_choice_coprime. (exists eut_left_eu_balance_previous_count_mask_choice_coprime. (eut_index_eu_balance_previous_count_mask) = eut_divisor_eu_balance_previous_count_mask_choice_coprime * eut_left_eu_balance_previous_count_mask_choice_coprime) -> (exists eut_right_eu_balance_previous_count_mask_choice_coprime. (m) = eut_divisor_eu_balance_previous_count_mask_choice_coprime * eut_right_eu_balance_previous_count_mask_choice_coprime) -> eut_divisor_eu_balance_previous_count_mask_choice_coprime = 1) /\ (eut_bit_eu_balance_previous_count_mask) = 1) \/ (~(forall eut_divisor_eu_balance_previous_count_mask_choice_coprime. (exists eut_left_eu_balance_previous_count_mask_choice_coprime. (eut_index_eu_balance_previous_count_mask) = eut_divisor_eu_balance_previous_count_mask_choice_coprime * eut_left_eu_balance_previous_count_mask_choice_coprime) -> (exists eut_right_eu_balance_previous_count_mask_choice_coprime. (m) = eut_divisor_eu_balance_previous_count_mask_choice_coprime * eut_right_eu_balance_previous_count_mask_choice_coprime) -> eut_divisor_eu_balance_previous_count_mask_choice_coprime = 1) /\ (eut_bit_eu_balance_previous_count_mask) = 0)))) /\ (exists fs_u_eut_eu_balance_previous_count_sum fs_v_eut_eu_balance_previous_count_sum. ((((exists fs_h_eut_eu_balance_previous_count_sum_body_start. fs_h_eut_eu_balance_previous_count_sum_body_start + S (0) = S ((S (0)) * fs_v_eut_eu_balance_previous_count_sum)) /\ exists fs_q_eut_eu_balance_previous_count_sum_body_start. fs_u_eut_eu_balance_previous_count_sum = fs_q_eut_eu_balance_previous_count_sum_body_start * S ((S (0)) * fs_v_eut_eu_balance_previous_count_sum) + (0))) /\ ((((exists fs_h_eut_eu_balance_previous_count_sum_body_terminal. fs_h_eut_eu_balance_previous_count_sum_body_terminal + S (r) = S ((S (l)) * fs_v_eut_eu_balance_previous_count_sum)) /\ exists fs_q_eut_eu_balance_previous_count_sum_body_terminal. fs_u_eut_eu_balance_previous_count_sum = fs_q_eut_eu_balance_previous_count_sum_body_terminal * S ((S (l)) * fs_v_eut_eu_balance_previous_count_sum) + (r))) /\ forall fs_i_eut_eu_balance_previous_count_sum_body_steps. (exists fs_lt_eut_eu_balance_previous_count_sum_body_steps_bound. fs_lt_eut_eu_balance_previous_count_sum_body_steps_bound + S fs_i_eut_eu_balance_previous_count_sum_body_steps = l) -> exists fs_a_eut_eu_balance_previous_count_sum_body_steps fs_r_eut_eu_balance_previous_count_sum_body_steps fs_s_eut_eu_balance_previous_count_sum_body_steps. ((((exists fs_h_eut_eu_balance_previous_count_sum_body_steps_summand. fs_h_eut_eu_balance_previous_count_sum_body_steps_summand + S (fs_a_eut_eu_balance_previous_count_sum_body_steps) = S ((S (fs_i_eut_eu_balance_previous_count_sum_body_steps)) * eut_scale_eu_balance_previous_count)) /\ exists fs_q_eut_eu_balance_previous_count_sum_body_steps_summand. eut_code_eu_balance_previous_count = fs_q_eut_eu_balance_previous_count_sum_body_steps_summand * S ((S (fs_i_eut_eu_balance_previous_count_sum_body_steps)) * eut_scale_eu_balance_previous_count) + (fs_a_eut_eu_balance_previous_count_sum_body_steps))) /\ ((((exists fs_h_eut_eu_balance_previous_count_sum_body_steps_partial. fs_h_eut_eu_balance_previous_count_sum_body_steps_partial + S (fs_r_eut_eu_balance_previous_count_sum_body_steps) = S ((S (fs_i_eut_eu_balance_previous_count_sum_body_steps)) * fs_v_eut_eu_balance_previous_count_sum)) /\ exists fs_q_eut_eu_balance_previous_count_sum_body_steps_partial. fs_u_eut_eu_balance_previous_count_sum = fs_q_eut_eu_balance_previous_count_sum_body_steps_partial * S ((S (fs_i_eut_eu_balance_previous_count_sum_body_steps)) * fs_v_eut_eu_balance_previous_count_sum) + (fs_r_eut_eu_balance_previous_count_sum_body_steps))) /\ ((((exists fs_h_eut_eu_balance_previous_count_sum_body_steps_successor. fs_h_eut_eu_balance_previous_count_sum_body_steps_successor + S (fs_s_eut_eu_balance_previous_count_sum_body_steps) = S ((S (S fs_i_eut_eu_balance_previous_count_sum_body_steps)) * fs_v_eut_eu_balance_previous_count_sum)) /\ exists fs_q_eut_eu_balance_previous_count_sum_body_steps_successor. fs_u_eut_eu_balance_previous_count_sum = fs_q_eut_eu_balance_previous_count_sum_body_steps_successor * S ((S (S fs_i_eut_eu_balance_previous_count_sum_body_steps)) * fs_v_eut_eu_balance_previous_count_sum) + (fs_s_eut_eu_balance_previous_count_sum_body_steps))) /\ fs_s_eut_eu_balance_previous_count_sum_body_steps = fs_r_eut_eu_balance_previous_count_sum_body_steps + fs_a_eut_eu_balance_previous_count_sum_body_steps))))))) /\ (((((forall eut_divisor_eu_balance_last_bit_coprime. (exists eut_left_eu_balance_last_bit_coprime. (l) = eut_divisor_eu_balance_last_bit_coprime * eut_left_eu_balance_last_bit_coprime) -> (exists eut_right_eu_balance_last_bit_coprime. (m) = eut_divisor_eu_balance_last_bit_coprime * eut_right_eu_balance_last_bit_coprime) -> eut_divisor_eu_balance_last_bit_coprime = 1) /\ (f) = 1) \/ (~(forall eut_divisor_eu_balance_last_bit_coprime. (exists eut_left_eu_balance_last_bit_coprime. (l) = eut_divisor_eu_balance_last_bit_coprime * eut_left_eu_balance_last_bit_coprime) -> (exists eut_right_eu_balance_last_bit_coprime. (m) = eut_divisor_eu_balance_last_bit_coprime * eut_right_eu_balance_last_bit_coprime) -> eut_divisor_eu_balance_last_bit_coprime = 1) /\ (f) = 0))) /\ t=r+f)
  67. 0067specialize totient_unit_count_succ_decompose (m)
  68. 0068specialize totient_unit_count_succ_decompose (l)
  69. 0069specialize totient_unit_count_succ_decompose (t)
  70. 0070apply totient_unit_count_succ_decompose
  71. 0071exact ht
  72. 0072cases hc
  73. 0073cases hc_witness
  74. 0074cases hc_witness_witness
  75. 0075cases hc_witness_witness_right
  76. 0076have hp : exists v R. (((exists fs_h_eu_balance_source_last. fs_h_eu_balance_source_last + S (v) = S ((S (l)) * c)) /\ exists fs_q_eu_balance_source_last. b = fs_q_eu_balance_source_last * S ((S (l)) * c) + (v))) /\ ((exists ff_u_fsat_eu_balance_source_previous ff_v_fsat_eu_balance_source_previous. ((((exists ff_h_fsat_eu_balance_source_previous_start. ff_h_fsat_eu_balance_source_previous_start + S (1) = S ((S (0)) * ff_v_fsat_eu_balance_source_previous)) /\ exists ff_q_fsat_eu_balance_source_previous_start. ff_u_fsat_eu_balance_source_previous = ff_q_fsat_eu_balance_source_previous_start * S ((S (0)) * ff_v_fsat_eu_balance_source_previous) + (1))) /\ ((((exists ff_h_fsat_eu_balance_source_previous_terminal. ff_h_fsat_eu_balance_source_previous_terminal + S (R) = S ((S (l)) * ff_v_fsat_eu_balance_source_previous)) /\ exists ff_q_fsat_eu_balance_source_previous_terminal. ff_u_fsat_eu_balance_source_previous = ff_q_fsat_eu_balance_source_previous_terminal * S ((S (l)) * ff_v_fsat_eu_balance_source_previous) + (R))) /\ forall ff_i_fsat_eu_balance_source_previous. (exists ff_lt_fsat_eu_balance_source_previous_bound. ff_lt_fsat_eu_balance_source_previous_bound + S ff_i_fsat_eu_balance_source_previous = l) -> exists ff_p_fsat_eu_balance_source_previous ff_r_fsat_eu_balance_source_previous ff_s_fsat_eu_balance_source_previous. ((((exists ff_h_fsat_eu_balance_source_previous_factor. ff_h_fsat_eu_balance_source_previous_factor + S (ff_p_fsat_eu_balance_source_previous) = S ((S (ff_i_fsat_eu_balance_source_previous)) * c)) /\ exists ff_q_fsat_eu_balance_source_previous_factor. b = ff_q_fsat_eu_balance_source_previous_factor * S ((S (ff_i_fsat_eu_balance_source_previous)) * c) + (ff_p_fsat_eu_balance_source_previous))) /\ ((((exists ff_h_fsat_eu_balance_source_previous_partial. ff_h_fsat_eu_balance_source_previous_partial + S (ff_r_fsat_eu_balance_source_previous) = S ((S (ff_i_fsat_eu_balance_source_previous)) * ff_v_fsat_eu_balance_source_previous)) /\ exists ff_q_fsat_eu_balance_source_previous_partial. ff_u_fsat_eu_balance_source_previous = ff_q_fsat_eu_balance_source_previous_partial * S ((S (ff_i_fsat_eu_balance_source_previous)) * ff_v_fsat_eu_balance_source_previous) + (ff_r_fsat_eu_balance_source_previous))) /\ ((((exists ff_h_fsat_eu_balance_source_previous_successor. ff_h_fsat_eu_balance_source_previous_successor + S (ff_s_fsat_eu_balance_source_previous) = S ((S (S ff_i_fsat_eu_balance_source_previous)) * ff_v_fsat_eu_balance_source_previous)) /\ exists ff_q_fsat_eu_balance_source_previous_successor. ff_u_fsat_eu_balance_source_previous = ff_q_fsat_eu_balance_source_previous_successor * S ((S (S ff_i_fsat_eu_balance_source_previous)) * ff_v_fsat_eu_balance_source_previous) + (ff_s_fsat_eu_balance_source_previous))) /\ ff_s_fsat_eu_balance_source_previous = ff_r_fsat_eu_balance_source_previous * ff_p_fsat_eu_balance_source_previous)))))) /\ P=R*v)
  77. 0077specialize beta_product_succ_decompose (b)
  78. 0078specialize beta_product_succ_decompose (c)
  79. 0079specialize beta_product_succ_decompose (l)
  80. 0080specialize beta_product_succ_decompose (P)
  81. 0081apply beta_product_succ_decompose
  82. 0082exact hP
  83. 0083cases hp
  84. 0084cases hp_witness
  85. 0085cases hp_witness_witness
  86. 0086cases hp_witness_witness_right
  87. 0087have hq : exists v R. (((exists fs_h_eu_balance_target_last. fs_h_eu_balance_target_last + S (v) = S ((S (l)) * e)) /\ exists fs_q_eu_balance_target_last. d = fs_q_eu_balance_target_last * S ((S (l)) * e) + (v))) /\ ((exists ff_u_fsat_eu_balance_target_previous ff_v_fsat_eu_balance_target_previous. ((((exists ff_h_fsat_eu_balance_target_previous_start. ff_h_fsat_eu_balance_target_previous_start + S (1) = S ((S (0)) * ff_v_fsat_eu_balance_target_previous)) /\ exists ff_q_fsat_eu_balance_target_previous_start. ff_u_fsat_eu_balance_target_previous = ff_q_fsat_eu_balance_target_previous_start * S ((S (0)) * ff_v_fsat_eu_balance_target_previous) + (1))) /\ ((((exists ff_h_fsat_eu_balance_target_previous_terminal. ff_h_fsat_eu_balance_target_previous_terminal + S (R) = S ((S (l)) * ff_v_fsat_eu_balance_target_previous)) /\ exists ff_q_fsat_eu_balance_target_previous_terminal. ff_u_fsat_eu_balance_target_previous = ff_q_fsat_eu_balance_target_previous_terminal * S ((S (l)) * ff_v_fsat_eu_balance_target_previous) + (R))) /\ forall ff_i_fsat_eu_balance_target_previous. (exists ff_lt_fsat_eu_balance_target_previous_bound. ff_lt_fsat_eu_balance_target_previous_bound + S ff_i_fsat_eu_balance_target_previous = l) -> exists ff_p_fsat_eu_balance_target_previous ff_r_fsat_eu_balance_target_previous ff_s_fsat_eu_balance_target_previous. ((((exists ff_h_fsat_eu_balance_target_previous_factor. ff_h_fsat_eu_balance_target_previous_factor + S (ff_p_fsat_eu_balance_target_previous) = S ((S (ff_i_fsat_eu_balance_target_previous)) * e)) /\ exists ff_q_fsat_eu_balance_target_previous_factor. d = ff_q_fsat_eu_balance_target_previous_factor * S ((S (ff_i_fsat_eu_balance_target_previous)) * e) + (ff_p_fsat_eu_balance_target_previous))) /\ ((((exists ff_h_fsat_eu_balance_target_previous_partial. ff_h_fsat_eu_balance_target_previous_partial + S (ff_r_fsat_eu_balance_target_previous) = S ((S (ff_i_fsat_eu_balance_target_previous)) * ff_v_fsat_eu_balance_target_previous)) /\ exists ff_q_fsat_eu_balance_target_previous_partial. ff_u_fsat_eu_balance_target_previous = ff_q_fsat_eu_balance_target_previous_partial * S ((S (ff_i_fsat_eu_balance_target_previous)) * ff_v_fsat_eu_balance_target_previous) + (ff_r_fsat_eu_balance_target_previous))) /\ ((((exists ff_h_fsat_eu_balance_target_previous_successor. ff_h_fsat_eu_balance_target_previous_successor + S (ff_s_fsat_eu_balance_target_previous) = S ((S (S ff_i_fsat_eu_balance_target_previous)) * ff_v_fsat_eu_balance_target_previous)) /\ exists ff_q_fsat_eu_balance_target_previous_successor. ff_u_fsat_eu_balance_target_previous = ff_q_fsat_eu_balance_target_previous_successor * S ((S (S ff_i_fsat_eu_balance_target_previous)) * ff_v_fsat_eu_balance_target_previous) + (ff_s_fsat_eu_balance_target_previous))) /\ ff_s_fsat_eu_balance_target_previous = ff_r_fsat_eu_balance_target_previous * ff_p_fsat_eu_balance_target_previous)))))) /\ Q=R*v)
  88. 0088specialize beta_product_succ_decompose (d)
  89. 0089specialize beta_product_succ_decompose (e)
  90. 0090specialize beta_product_succ_decompose (l)
  91. 0091specialize beta_product_succ_decompose (Q)
  92. 0092apply beta_product_succ_decompose
  93. 0093exact hQ
  94. 0094cases hq
  95. 0095cases hq_witness
  96. 0096cases hq_witness_witness
  97. 0097cases hq_witness_witness_right
  98. 0098have hz : exists z. (exists pa_b_euta_eu_balance_previous_power pa_c_euta_eu_balance_previous_power. ((forall pa_i_euta_eu_balance_previous_power_repeat. (exists pa_lt_euta_eu_balance_previous_power_repeat_bound. pa_lt_euta_eu_balance_previous_power_repeat_bound + S pa_i_euta_eu_balance_previous_power_repeat = x) -> (((exists pa_h_euta_eu_balance_previous_power_repeat_decoded. pa_h_euta_eu_balance_previous_power_repeat_decoded + S (a) = S ((S (pa_i_euta_eu_balance_previous_power_repeat)) * pa_c_euta_eu_balance_previous_power)) /\ exists pa_q_euta_eu_balance_previous_power_repeat_decoded. pa_b_euta_eu_balance_previous_power = pa_q_euta_eu_balance_previous_power_repeat_decoded * S ((S (pa_i_euta_eu_balance_previous_power_repeat)) * pa_c_euta_eu_balance_previous_power) + (a)))) /\ (exists pa_u_euta_eu_balance_previous_power_product pa_v_euta_eu_balance_previous_power_product. ((((exists pa_h_euta_eu_balance_previous_power_product_start. pa_h_euta_eu_balance_previous_power_product_start + S (1) = S ((S (0)) * pa_v_euta_eu_balance_previous_power_product)) /\ exists pa_q_euta_eu_balance_previous_power_product_start. pa_u_euta_eu_balance_previous_power_product = pa_q_euta_eu_balance_previous_power_product_start * S ((S (0)) * pa_v_euta_eu_balance_previous_power_product) + (1))) /\ ((((exists pa_h_euta_eu_balance_previous_power_product_terminal. pa_h_euta_eu_balance_previous_power_product_terminal + S (z) = S ((S (x)) * pa_v_euta_eu_balance_previous_power_product)) /\ exists pa_q_euta_eu_balance_previous_power_product_terminal. pa_u_euta_eu_balance_previous_power_product = pa_q_euta_eu_balance_previous_power_product_terminal * S ((S (x)) * pa_v_euta_eu_balance_previous_power_product) + (z))) /\ forall pa_i_euta_eu_balance_previous_power_product. (exists pa_lt_euta_eu_balance_previous_power_product_bound. pa_lt_euta_eu_balance_previous_power_product_bound + S pa_i_euta_eu_balance_previous_power_product = x) -> exists pa_p_euta_eu_balance_previous_power_product pa_r_euta_eu_balance_previous_power_product pa_s_euta_eu_balance_previous_power_product. ((((exists pa_h_euta_eu_balance_previous_power_product_factor. pa_h_euta_eu_balance_previous_power_product_factor + S (pa_p_euta_eu_balance_previous_power_product) = S ((S (pa_i_euta_eu_balance_previous_power_product)) * pa_c_euta_eu_balance_previous_power)) /\ exists pa_q_euta_eu_balance_previous_power_product_factor. pa_b_euta_eu_balance_previous_power = pa_q_euta_eu_balance_previous_power_product_factor * S ((S (pa_i_euta_eu_balance_previous_power_product)) * pa_c_euta_eu_balance_previous_power) + (pa_p_euta_eu_balance_previous_power_product))) /\ ((((exists pa_h_euta_eu_balance_previous_power_product_partial. pa_h_euta_eu_balance_previous_power_product_partial + S (pa_r_euta_eu_balance_previous_power_product) = S ((S (pa_i_euta_eu_balance_previous_power_product)) * pa_v_euta_eu_balance_previous_power_product)) /\ exists pa_q_euta_eu_balance_previous_power_product_partial. pa_u_euta_eu_balance_previous_power_product = pa_q_euta_eu_balance_previous_power_product_partial * S ((S (pa_i_euta_eu_balance_previous_power_product)) * pa_v_euta_eu_balance_previous_power_product) + (pa_r_euta_eu_balance_previous_power_product))) /\ ((((exists pa_h_euta_eu_balance_previous_power_product_successor. pa_h_euta_eu_balance_previous_power_product_successor + S (pa_s_euta_eu_balance_previous_power_product) = S ((S (S pa_i_euta_eu_balance_previous_power_product)) * pa_v_euta_eu_balance_previous_power_product)) /\ exists pa_q_euta_eu_balance_previous_power_product_successor. pa_u_euta_eu_balance_previous_power_product = pa_q_euta_eu_balance_previous_power_product_successor * S ((S (S pa_i_euta_eu_balance_previous_power_product)) * pa_v_euta_eu_balance_previous_power_product) + (pa_s_euta_eu_balance_previous_power_product))) /\ pa_s_euta_eu_balance_previous_power_product = pa_r_euta_eu_balance_previous_power_product * pa_p_euta_eu_balance_previous_power_product))))))))
  99. 0099specialize pow_exists (a)
  100. 0100specialize pow_exists (x)
  101. 0101apply pow_exists
  102. 0102cases hz
  103. 0103have hprevious : exists eu_mod_left_balance_previous eu_mod_right_balance_previous. (x6*x3) + (m) * eu_mod_left_balance_previous = (x5) + (m) * eu_mod_right_balance_previous
  104. 0104specialize IH (a)
  105. 0105specialize IH (m)
  106. 0106specialize IH (b)
  107. 0107specialize IH (c)
  108. 0108specialize IH (d)
  109. 0109specialize IH (e)
  110. 0110specialize IH (x)
  111. 0111specialize IH (x3)
  112. 0112specialize IH (x5)
  113. 0113specialize IH (x6)
  114. 0114apply IH
  115. 0115exact hc_witness_witness_left
  116. 0116specialize euler_unit_scaled_prefix_drop_last (a)
  117. 0117specialize euler_unit_scaled_prefix_drop_last (m)
  118. 0118specialize euler_unit_scaled_prefix_drop_last (b)
  119. 0119specialize euler_unit_scaled_prefix_drop_last (c)
  120. 0120specialize euler_unit_scaled_prefix_drop_last (d)
  121. 0121specialize euler_unit_scaled_prefix_drop_last (e)
  122. 0122specialize euler_unit_scaled_prefix_drop_last (l)
  123. 0123apply euler_unit_scaled_prefix_drop_last
  124. 0124exact hs
  125. 0125exact hp_witness_witness_right_left
  126. 0126exact hq_witness_witness_right_left
  127. 0127exact hz_witness
  128. 0128have hstep : ((forall eut_divisor_eu_balance_last_unit. (exists eut_left_eu_balance_last_unit. (l) = eut_divisor_eu_balance_last_unit * eut_left_eu_balance_last_unit) -> (exists eut_right_eu_balance_last_unit. (m) = eut_divisor_eu_balance_last_unit * eut_right_eu_balance_last_unit) -> eut_divisor_eu_balance_last_unit = 1) -> (exists eu_mod_left_balance_last_scaled eu_mod_right_balance_last_scaled. (a*x2) + (m) * eu_mod_left_balance_last_scaled = (x4) + (m) * eu_mod_right_balance_last_scaled)) /\ (~(forall eut_divisor_eu_balance_last_nonunit. (exists eut_left_eu_balance_last_nonunit. (l) = eut_divisor_eu_balance_last_nonunit * eut_left_eu_balance_last_nonunit) -> (exists eut_right_eu_balance_last_nonunit. (m) = eut_divisor_eu_balance_last_nonunit * eut_right_eu_balance_last_nonunit) -> eut_divisor_eu_balance_last_nonunit = 1) -> (exists eu_mod_left_balance_last_unchanged eu_mod_right_balance_last_unchanged. (x2) + (m) * eu_mod_left_balance_last_unchanged = (x4) + (m) * eu_mod_right_balance_last_unchanged))
  129. 0129specialize hs (l)
  130. 0130specialize hs (x2)
  131. 0131specialize hs (x4)
  132. 0132apply hs
  133. 0133specialize le_refl (S l)
  134. 0134apply le_refl
  135. 0135exact hp_witness_witness_left
  136. 0136exact hq_witness_witness_left
  137. 0137cases hstep
  138. 0138cases hc_witness_witness_right_left
  139. 0139cases hc_witness_witness_right_left_left
  140. 0140have htexp : t=S x
  141. 0141rewrite hc_witness_witness_right_right
  142. 0142rewrite hc_witness_witness_right_left_left_right
  143. 0143simp
  144. 0144have hwp : w=x6*a
  145. 0145specialize pow_successor_pair_mul (a)
  146. 0146specialize pow_successor_pair_mul (x)
  147. 0147specialize pow_successor_pair_mul (t)
  148. 0148specialize pow_successor_pair_mul (x6)
  149. 0149specialize pow_successor_pair_mul (w)
  150. 0150apply pow_successor_pair_mul
  151. 0151exact htexp
  152. 0152exact hz_witness
  153. 0153exact hw
  154. 0154have hproduct : w*P=(x6*x3)*(a*x2)
  155. 0155rewrite hwp
  156. 0156rewrite hp_witness_witness_right_right
  157. 0157specialize mul_shuffle_four (x6)
  158. 0158specialize mul_shuffle_four (a)
  159. 0159specialize mul_shuffle_four (x3)
  160. 0160specialize mul_shuffle_four (x2)
  161. 0161apply mul_shuffle_four
  162. 0162rewrite hproduct
  163. 0163rewrite hq_witness_witness_right_right
  164. 0164specialize mod_eq_mul (m)
  165. 0165specialize mod_eq_mul (x6*x3)
  166. 0166specialize mod_eq_mul (x5)
  167. 0167specialize mod_eq_mul (a*x2)
  168. 0168specialize mod_eq_mul (x4)
  169. 0169apply mod_eq_mul
  170. 0170exact hprevious
  171. 0171apply hstep_left
  172. 0172exact hc_witness_witness_right_left_left_left
  173. 0173cases hc_witness_witness_right_left_right
  174. 0174have htexp : t=x
  175. 0175rewrite hc_witness_witness_right_right
  176. 0176rewrite hc_witness_witness_right_left_right_right
  177. 0177simp
  178. 0178rewrite htexp at hw
  179. 0179rewrite htexp at hw
  180. 0180rewrite htexp at hw
  181. 0181rewrite htexp at hw
  182. 0182have hwp : w=x6
  183. 0183specialize pow_functional (a)
  184. 0184specialize pow_functional (x)
  185. 0185specialize pow_functional (w)
  186. 0186specialize pow_functional (x6)
  187. 0187apply pow_functional
  188. 0188exact hw
  189. 0189exact hz_witness
  190. 0190have hproduct : w*P=(x6*x3)*x2
  191. 0191rewrite hwp
  192. 0192rewrite hp_witness_witness_right_right
  193. 0193symm
  194. 0194specialize mul_assoc (x6)
  195. 0195specialize mul_assoc (x3)
  196. 0196specialize mul_assoc (x2)
  197. 0197apply mul_assoc
  198. 0198rewrite hproduct
  199. 0199rewrite hq_witness_witness_right_right
  200. 0200specialize mod_eq_mul (m)
  201. 0201specialize mod_eq_mul (x6*x3)
  202. 0202specialize mod_eq_mul (x5)
  203. 0203specialize mod_eq_mul (x2)
  204. 0204specialize mod_eq_mul (x4)
  205. 0205apply mod_eq_mul
  206. 0206exact hprevious
  207. 0207apply hstep_right
  208. 0208exact hc_witness_witness_right_left_right_left