EU0014

euler_unit_product_prefix_exists

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

HA induction constructs all coprime-weighted factors; their list is never an endpoint assumption.

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 m l. exists b c. (forall eu_factor_index_factors_exists. (exists eut_gap_eu_factors_exists_index. eut_gap_eu_factors_exists_index + S (eu_factor_index_factors_exists) = (l)) -> exists eu_factor_value_factors_exists. (((exists fs_h_eu_factors_exists_at. fs_h_eu_factors_exists_at + S (eu_factor_value_factors_exists) = S ((S (eu_factor_index_factors_exists)) * c)) /\ exists fs_q_eu_factors_exists_at. b = fs_q_eu_factors_exists_at * S ((S (eu_factor_index_factors_exists)) * c) + (eu_factor_value_factors_exists))) /\ ((((forall eut_divisor_eu_factors_exists_choice_coprime. (exists eut_left_eu_factors_exists_choice_coprime. (eu_factor_index_factors_exists) = eut_divisor_eu_factors_exists_choice_coprime * eut_left_eu_factors_exists_choice_coprime) -> (exists eut_right_eu_factors_exists_choice_coprime. (m) = eut_divisor_eu_factors_exists_choice_coprime * eut_right_eu_factors_exists_choice_coprime) -> eut_divisor_eu_factors_exists_choice_coprime = 1) /\ (eu_factor_value_factors_exists)=(eu_factor_index_factors_exists)) \/ (~(forall eut_divisor_eu_factors_exists_choice_coprime. (exists eut_left_eu_factors_exists_choice_coprime. (eu_factor_index_factors_exists) = eut_divisor_eu_factors_exists_choice_coprime * eut_left_eu_factors_exists_choice_coprime) -> (exists eut_right_eu_factors_exists_choice_coprime. (m) = eut_divisor_eu_factors_exists_choice_coprime * eut_right_eu_factors_exists_choice_coprime) -> eut_divisor_eu_factors_exists_choice_coprime = 1) /\ (eu_factor_value_factors_exists)=1))))

Constructive proof overview

Generated structural guide

HA induction constructs all coprime-weighted factors; their list is never an endpoint assumption.

The unchanged tactic script uses 3 declared prerequisites and contains 23 exact native proof lines.

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

Proof neighborhood

Direct dependencies

EU0012 euler_unit_product_prefix_empty EU000E euler_unit_product_factor_exists EU0013 euler_unit_product_prefix_extend

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

23 script commands · 8 reading checkpoints · 1 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 emptyeuler unit product factor existseuler unit product prefix extend

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

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

  1. L1
    intro m
02Induction on lL2–2

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

  1. L2
    induction l
03Construct an explicit witnessL3–4

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

  1. L3
    exists 0
  2. L4
    exists 0
04Use earlier factsL5–8

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

  1. L5
    specialize euler_unit_product_prefix_empty (m)
  2. L6
    specialize euler_unit_product_prefix_empty (0)
  3. L7
    specialize euler_unit_product_prefix_empty (0)
  4. L8
    apply euler_unit_product_prefix_empty
05Separate the logical casesL9–10

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

  1. L9
    cases IH
  2. L10
    cases IH_witness
06Establish hvL11–14

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

  1. L11
    have hv : ∃ v. UnitProductFactor(m,l,v)Definitions: UnitProductFactor
  2. L12
    specialize euler_unit_product_factor_exists (m)
  3. L13
    specialize euler_unit_product_factor_exists (l)
  4. L14
    apply euler_unit_product_factor_exists
07Separate the logical casesL15–15

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

  1. L15
    cases hv
08Use earlier factsL16–23

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

  1. L16
    specialize euler_unit_product_prefix_extend (m)
  2. L17
    specialize euler_unit_product_prefix_extend (x)
  3. L18
    specialize euler_unit_product_prefix_extend (x1)
  4. L19
    specialize euler_unit_product_prefix_extend (l)
  5. L20
    specialize euler_unit_product_prefix_extend (x2)
  6. L21
    apply euler_unit_product_prefix_extend
  7. L22
    exact IH_witness_witness
  8. L23
    exact hv_witness

Library-wide reading audit

Original exact command ledger · 23 lines
  1. 0001intro m
  2. 0002induction l
  3. 0003exists 0
  4. 0004exists 0
  5. 0005specialize euler_unit_product_prefix_empty (m)
  6. 0006specialize euler_unit_product_prefix_empty (0)
  7. 0007specialize euler_unit_product_prefix_empty (0)
  8. 0008apply euler_unit_product_prefix_empty
  9. 0009cases IH
  10. 0010cases IH_witness
  11. 0011have hv : exists v. ((((forall eut_divisor_eu_factor_next_coprime. (exists eut_left_eu_factor_next_coprime. (l) = eut_divisor_eu_factor_next_coprime * eut_left_eu_factor_next_coprime) -> (exists eut_right_eu_factor_next_coprime. (m) = eut_divisor_eu_factor_next_coprime * eut_right_eu_factor_next_coprime) -> eut_divisor_eu_factor_next_coprime = 1) /\ (v)=(l)) \/ (~(forall eut_divisor_eu_factor_next_coprime. (exists eut_left_eu_factor_next_coprime. (l) = eut_divisor_eu_factor_next_coprime * eut_left_eu_factor_next_coprime) -> (exists eut_right_eu_factor_next_coprime. (m) = eut_divisor_eu_factor_next_coprime * eut_right_eu_factor_next_coprime) -> eut_divisor_eu_factor_next_coprime = 1) /\ (v)=1)))
  12. 0012specialize euler_unit_product_factor_exists (m)
  13. 0013specialize euler_unit_product_factor_exists (l)
  14. 0014apply euler_unit_product_factor_exists
  15. 0015cases hv
  16. 0016specialize euler_unit_product_prefix_extend (m)
  17. 0017specialize euler_unit_product_prefix_extend (x)
  18. 0018specialize euler_unit_product_prefix_extend (x1)
  19. 0019specialize euler_unit_product_prefix_extend (l)
  20. 0020specialize euler_unit_product_prefix_extend (x2)
  21. 0021apply euler_unit_product_prefix_extend
  22. 0022exact IH_witness_witness
  23. 0023exact hv_witness