EU0017

euler_unit_product_coprime

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

The entire actual unit-weighted product is coprime to m; this is the proved cancellation premise.

Exact expanded first-order arithmetic statement

forall l m b c P. (forall eu_factor_index_product_coprime_factors. (exists eut_gap_eu_product_coprime_factors_index. eut_gap_eu_product_coprime_factors_index + S (eu_factor_index_product_coprime_factors) = (l)) -> exists eu_factor_value_product_coprime_factors. (((exists fs_h_eu_product_coprime_factors_at. fs_h_eu_product_coprime_factors_at + S (eu_factor_value_product_coprime_factors) = S ((S (eu_factor_index_product_coprime_factors)) * c)) /\ exists fs_q_eu_product_coprime_factors_at. b = fs_q_eu_product_coprime_factors_at * S ((S (eu_factor_index_product_coprime_factors)) * c) + (eu_factor_value_product_coprime_factors))) /\ ((((forall eut_divisor_eu_product_coprime_factors_choice_coprime. (exists eut_left_eu_product_coprime_factors_choice_coprime. (eu_factor_index_product_coprime_factors) = eut_divisor_eu_product_coprime_factors_choice_coprime * eut_left_eu_product_coprime_factors_choice_coprime) -> (exists eut_right_eu_product_coprime_factors_choice_coprime. (m) = eut_divisor_eu_product_coprime_factors_choice_coprime * eut_right_eu_product_coprime_factors_choice_coprime) -> eut_divisor_eu_product_coprime_factors_choice_coprime = 1) /\ (eu_factor_value_product_coprime_factors)=(eu_factor_index_product_coprime_factors)) \/ (~(forall eut_divisor_eu_product_coprime_factors_choice_coprime. (exists eut_left_eu_product_coprime_factors_choice_coprime. (eu_factor_index_product_coprime_factors) = eut_divisor_eu_product_coprime_factors_choice_coprime * eut_left_eu_product_coprime_factors_choice_coprime) -> (exists eut_right_eu_product_coprime_factors_choice_coprime. (m) = eut_divisor_eu_product_coprime_factors_choice_coprime * eut_right_eu_product_coprime_factors_choice_coprime) -> eut_divisor_eu_product_coprime_factors_choice_coprime = 1) /\ (eu_factor_value_product_coprime_factors)=1)))) -> (exists ff_u_fsat_eu_product_coprime ff_v_fsat_eu_product_coprime. ((((exists ff_h_fsat_eu_product_coprime_start. ff_h_fsat_eu_product_coprime_start + S (1) = S ((S (0)) * ff_v_fsat_eu_product_coprime)) /\ exists ff_q_fsat_eu_product_coprime_start. ff_u_fsat_eu_product_coprime = ff_q_fsat_eu_product_coprime_start * S ((S (0)) * ff_v_fsat_eu_product_coprime) + (1))) /\ ((((exists ff_h_fsat_eu_product_coprime_terminal. ff_h_fsat_eu_product_coprime_terminal + S (P) = S ((S (l)) * ff_v_fsat_eu_product_coprime)) /\ exists ff_q_fsat_eu_product_coprime_terminal. ff_u_fsat_eu_product_coprime = ff_q_fsat_eu_product_coprime_terminal * S ((S (l)) * ff_v_fsat_eu_product_coprime) + (P))) /\ forall ff_i_fsat_eu_product_coprime. (exists ff_lt_fsat_eu_product_coprime_bound. ff_lt_fsat_eu_product_coprime_bound + S ff_i_fsat_eu_product_coprime = l) -> exists ff_p_fsat_eu_product_coprime ff_r_fsat_eu_product_coprime ff_s_fsat_eu_product_coprime. ((((exists ff_h_fsat_eu_product_coprime_factor. ff_h_fsat_eu_product_coprime_factor + S (ff_p_fsat_eu_product_coprime) = S ((S (ff_i_fsat_eu_product_coprime)) * c)) /\ exists ff_q_fsat_eu_product_coprime_factor. b = ff_q_fsat_eu_product_coprime_factor * S ((S (ff_i_fsat_eu_product_coprime)) * c) + (ff_p_fsat_eu_product_coprime))) /\ ((((exists ff_h_fsat_eu_product_coprime_partial. ff_h_fsat_eu_product_coprime_partial + S (ff_r_fsat_eu_product_coprime) = S ((S (ff_i_fsat_eu_product_coprime)) * ff_v_fsat_eu_product_coprime)) /\ exists ff_q_fsat_eu_product_coprime_partial. ff_u_fsat_eu_product_coprime = ff_q_fsat_eu_product_coprime_partial * S ((S (ff_i_fsat_eu_product_coprime)) * ff_v_fsat_eu_product_coprime) + (ff_r_fsat_eu_product_coprime))) /\ ((((exists ff_h_fsat_eu_product_coprime_successor. ff_h_fsat_eu_product_coprime_successor + S (ff_s_fsat_eu_product_coprime) = S ((S (S ff_i_fsat_eu_product_coprime)) * ff_v_fsat_eu_product_coprime)) /\ exists ff_q_fsat_eu_product_coprime_successor. ff_u_fsat_eu_product_coprime = ff_q_fsat_eu_product_coprime_successor * S ((S (S ff_i_fsat_eu_product_coprime)) * ff_v_fsat_eu_product_coprime) + (ff_s_fsat_eu_product_coprime))) /\ ff_s_fsat_eu_product_coprime = ff_r_fsat_eu_product_coprime * ff_p_fsat_eu_product_coprime)))))) -> (forall eut_divisor_eu_product_coprime. (exists eut_left_eu_product_coprime. (P) = eut_divisor_eu_product_coprime * eut_left_eu_product_coprime) -> (exists eut_right_eu_product_coprime. (m) = eut_divisor_eu_product_coprime * eut_right_eu_product_coprime) -> eut_divisor_eu_product_coprime = 1)

Constructive proof overview

Generated structural guide

The entire actual unit-weighted product is coprime to m; this is the proved cancellation premise.

The unchanged tactic script uses 8 declared prerequisites and contains 65 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

beta_product_zero Alpha theorem; checked-use authorized coprime_one_left Alpha theorem; checked-use authorized beta_product_succ_decompose Alpha theorem; checked-use authorized EU0015 euler_unit_product_prefix_drop_last EU0016 euler_unit_product_prefix_entry EU0011 euler_unit_product_factor_coprime coprime_mul_left Alpha theorem; checked-use authorized le_refl 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

65 script commands · 10 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (3)
euler unit product prefix drop lasteuler unit product prefix entryeuler unit product factor coprime

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–7

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 m
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro P
  6. L6
    intro hf
  7. L7
    intro hP
02Establish heL8–17

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

  1. L8
    have he : P=1
  2. L9
    specialize beta_product_zero (b)
  3. L10
    specialize beta_product_zero (c)
  4. L11
    specialize beta_product_zero (P)
  5. L12
    apply beta_product_zero
  6. L13
    exact hP
  7. L14
    rewrite he
  8. L15
    specialize coprime_one_left (m)
  9. L16
    apply coprime_one_left
  10. L17
    intro m
03Fix variables and assumptionsL18–22

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

  1. L18
    intro b
  2. L19
    intro c
  3. L20
    intro P
  4. L21
    intro hf
  5. L22
    intro hP
04Establish hdL23–29

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

  1. L23
    have hd : ∃ v. ∃ Q. BetaAt(b,c,l,v) ∧ (Product(b,c,l,Q) ∧ P = Q · v)Definitions: BetaAtProduct
  2. L24
    specialize beta_product_succ_decompose (b)
  3. L25
    specialize beta_product_succ_decompose (c)
  4. L26
    specialize beta_product_succ_decompose (l)
  5. L27
    specialize beta_product_succ_decompose (P)
  6. L28
    apply beta_product_succ_decompose
  7. L29
    exact hP
05Separate the logical casesL30–33

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

  1. L30
    cases hd
  2. L31
    cases hd_witness
  3. L32
    cases hd_witness_witness
  4. L33
    cases hd_witness_witness_right
06Calculate and transport equalitiesL34–34

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

  1. L34
    rewrite hd_witness_witness_right_right
07Use earlier factsL35–44

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

  1. L35
    specialize coprime_mul_left (x1)
  2. L36
    specialize coprime_mul_left (x)
  3. L37
    specialize coprime_mul_left (m)
  4. L38
    apply coprime_mul_left
  5. L39
    specialize IH (m)
  6. L40
    specialize IH (b)
  7. L41
    specialize IH (c)
  8. L42
    specialize IH (x1)
  9. L43
    apply IH
  10. L44
    specialize euler_unit_product_prefix_drop_last (m)
08Use earlier factsL45–54

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

  1. L45
    specialize euler_unit_product_prefix_drop_last (b)
  2. L46
    specialize euler_unit_product_prefix_drop_last (c)
  3. L47
    specialize euler_unit_product_prefix_drop_last (l)
  4. L48
    apply euler_unit_product_prefix_drop_last
  5. L49
    exact hf
  6. L50
    exact hd_witness_witness_right_left
  7. L51
    specialize euler_unit_product_factor_coprime (m)
  8. L52
    specialize euler_unit_product_factor_coprime (l)
  9. L53
    specialize euler_unit_product_factor_coprime (x)
  10. L54
    apply euler_unit_product_factor_coprime
09Use earlier factsL55–64

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

  1. L55
    specialize euler_unit_product_prefix_entry (m)
  2. L56
    specialize euler_unit_product_prefix_entry (b)
  3. L57
    specialize euler_unit_product_prefix_entry (c)
  4. L58
    specialize euler_unit_product_prefix_entry (S l)
  5. L59
    specialize euler_unit_product_prefix_entry (l)
  6. L60
    specialize euler_unit_product_prefix_entry (x)
  7. L61
    apply euler_unit_product_prefix_entry
  8. L62
    exact hf
  9. L63
    specialize le_refl (S l)
  10. L64
    apply le_refl
10Use earlier factsL65–65

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

  1. L65
    exact hd_witness_witness_left

Library-wide reading audit

Original exact command ledger · 65 lines
  1. 0001induction l
  2. 0002intro m
  3. 0003intro b
  4. 0004intro c
  5. 0005intro P
  6. 0006intro hf
  7. 0007intro hP
  8. 0008have he : P=1
  9. 0009specialize beta_product_zero (b)
  10. 0010specialize beta_product_zero (c)
  11. 0011specialize beta_product_zero (P)
  12. 0012apply beta_product_zero
  13. 0013exact hP
  14. 0014rewrite he
  15. 0015specialize coprime_one_left (m)
  16. 0016apply coprime_one_left
  17. 0017intro m
  18. 0018intro b
  19. 0019intro c
  20. 0020intro P
  21. 0021intro hf
  22. 0022intro hP
  23. 0023have hd : exists v Q. (((exists fs_h_eu_product_last. fs_h_eu_product_last + S (v) = S ((S (l)) * c)) /\ exists fs_q_eu_product_last. b = fs_q_eu_product_last * S ((S (l)) * c) + (v))) /\ ((exists ff_u_fsat_eu_product_previous ff_v_fsat_eu_product_previous. ((((exists ff_h_fsat_eu_product_previous_start. ff_h_fsat_eu_product_previous_start + S (1) = S ((S (0)) * ff_v_fsat_eu_product_previous)) /\ exists ff_q_fsat_eu_product_previous_start. ff_u_fsat_eu_product_previous = ff_q_fsat_eu_product_previous_start * S ((S (0)) * ff_v_fsat_eu_product_previous) + (1))) /\ ((((exists ff_h_fsat_eu_product_previous_terminal. ff_h_fsat_eu_product_previous_terminal + S (Q) = S ((S (l)) * ff_v_fsat_eu_product_previous)) /\ exists ff_q_fsat_eu_product_previous_terminal. ff_u_fsat_eu_product_previous = ff_q_fsat_eu_product_previous_terminal * S ((S (l)) * ff_v_fsat_eu_product_previous) + (Q))) /\ forall ff_i_fsat_eu_product_previous. (exists ff_lt_fsat_eu_product_previous_bound. ff_lt_fsat_eu_product_previous_bound + S ff_i_fsat_eu_product_previous = l) -> exists ff_p_fsat_eu_product_previous ff_r_fsat_eu_product_previous ff_s_fsat_eu_product_previous. ((((exists ff_h_fsat_eu_product_previous_factor. ff_h_fsat_eu_product_previous_factor + S (ff_p_fsat_eu_product_previous) = S ((S (ff_i_fsat_eu_product_previous)) * c)) /\ exists ff_q_fsat_eu_product_previous_factor. b = ff_q_fsat_eu_product_previous_factor * S ((S (ff_i_fsat_eu_product_previous)) * c) + (ff_p_fsat_eu_product_previous))) /\ ((((exists ff_h_fsat_eu_product_previous_partial. ff_h_fsat_eu_product_previous_partial + S (ff_r_fsat_eu_product_previous) = S ((S (ff_i_fsat_eu_product_previous)) * ff_v_fsat_eu_product_previous)) /\ exists ff_q_fsat_eu_product_previous_partial. ff_u_fsat_eu_product_previous = ff_q_fsat_eu_product_previous_partial * S ((S (ff_i_fsat_eu_product_previous)) * ff_v_fsat_eu_product_previous) + (ff_r_fsat_eu_product_previous))) /\ ((((exists ff_h_fsat_eu_product_previous_successor. ff_h_fsat_eu_product_previous_successor + S (ff_s_fsat_eu_product_previous) = S ((S (S ff_i_fsat_eu_product_previous)) * ff_v_fsat_eu_product_previous)) /\ exists ff_q_fsat_eu_product_previous_successor. ff_u_fsat_eu_product_previous = ff_q_fsat_eu_product_previous_successor * S ((S (S ff_i_fsat_eu_product_previous)) * ff_v_fsat_eu_product_previous) + (ff_s_fsat_eu_product_previous))) /\ ff_s_fsat_eu_product_previous = ff_r_fsat_eu_product_previous * ff_p_fsat_eu_product_previous)))))) /\ P=Q*v)
  24. 0024specialize beta_product_succ_decompose (b)
  25. 0025specialize beta_product_succ_decompose (c)
  26. 0026specialize beta_product_succ_decompose (l)
  27. 0027specialize beta_product_succ_decompose (P)
  28. 0028apply beta_product_succ_decompose
  29. 0029exact hP
  30. 0030cases hd
  31. 0031cases hd_witness
  32. 0032cases hd_witness_witness
  33. 0033cases hd_witness_witness_right
  34. 0034rewrite hd_witness_witness_right_right
  35. 0035specialize coprime_mul_left (x1)
  36. 0036specialize coprime_mul_left (x)
  37. 0037specialize coprime_mul_left (m)
  38. 0038apply coprime_mul_left
  39. 0039specialize IH (m)
  40. 0040specialize IH (b)
  41. 0041specialize IH (c)
  42. 0042specialize IH (x1)
  43. 0043apply IH
  44. 0044specialize euler_unit_product_prefix_drop_last (m)
  45. 0045specialize euler_unit_product_prefix_drop_last (b)
  46. 0046specialize euler_unit_product_prefix_drop_last (c)
  47. 0047specialize euler_unit_product_prefix_drop_last (l)
  48. 0048apply euler_unit_product_prefix_drop_last
  49. 0049exact hf
  50. 0050exact hd_witness_witness_right_left
  51. 0051specialize euler_unit_product_factor_coprime (m)
  52. 0052specialize euler_unit_product_factor_coprime (l)
  53. 0053specialize euler_unit_product_factor_coprime (x)
  54. 0054apply euler_unit_product_factor_coprime
  55. 0055specialize euler_unit_product_prefix_entry (m)
  56. 0056specialize euler_unit_product_prefix_entry (b)
  57. 0057specialize euler_unit_product_prefix_entry (c)
  58. 0058specialize euler_unit_product_prefix_entry (S l)
  59. 0059specialize euler_unit_product_prefix_entry (l)
  60. 0060specialize euler_unit_product_prefix_entry (x)
  61. 0061apply euler_unit_product_prefix_entry
  62. 0062exact hf
  63. 0063specialize le_refl (S l)
  64. 0064apply le_refl
  65. 0065exact hd_witness_witness_left