EU0013

euler_unit_product_prefix_extend

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

Actually append the independently chosen next factor while preserving every earlier factor.

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 b c l v. (forall eu_factor_index_factors_extend_old. (exists eut_gap_eu_factors_extend_old_index. eut_gap_eu_factors_extend_old_index + S (eu_factor_index_factors_extend_old) = (l)) -> exists eu_factor_value_factors_extend_old. (((exists fs_h_eu_factors_extend_old_at. fs_h_eu_factors_extend_old_at + S (eu_factor_value_factors_extend_old) = S ((S (eu_factor_index_factors_extend_old)) * c)) /\ exists fs_q_eu_factors_extend_old_at. b = fs_q_eu_factors_extend_old_at * S ((S (eu_factor_index_factors_extend_old)) * c) + (eu_factor_value_factors_extend_old))) /\ ((((forall eut_divisor_eu_factors_extend_old_choice_coprime. (exists eut_left_eu_factors_extend_old_choice_coprime. (eu_factor_index_factors_extend_old) = eut_divisor_eu_factors_extend_old_choice_coprime * eut_left_eu_factors_extend_old_choice_coprime) -> (exists eut_right_eu_factors_extend_old_choice_coprime. (m) = eut_divisor_eu_factors_extend_old_choice_coprime * eut_right_eu_factors_extend_old_choice_coprime) -> eut_divisor_eu_factors_extend_old_choice_coprime = 1) /\ (eu_factor_value_factors_extend_old)=(eu_factor_index_factors_extend_old)) \/ (~(forall eut_divisor_eu_factors_extend_old_choice_coprime. (exists eut_left_eu_factors_extend_old_choice_coprime. (eu_factor_index_factors_extend_old) = eut_divisor_eu_factors_extend_old_choice_coprime * eut_left_eu_factors_extend_old_choice_coprime) -> (exists eut_right_eu_factors_extend_old_choice_coprime. (m) = eut_divisor_eu_factors_extend_old_choice_coprime * eut_right_eu_factors_extend_old_choice_coprime) -> eut_divisor_eu_factors_extend_old_choice_coprime = 1) /\ (eu_factor_value_factors_extend_old)=1)))) -> ((((forall eut_divisor_eu_factor_extend_last_coprime. (exists eut_left_eu_factor_extend_last_coprime. (l) = eut_divisor_eu_factor_extend_last_coprime * eut_left_eu_factor_extend_last_coprime) -> (exists eut_right_eu_factor_extend_last_coprime. (m) = eut_divisor_eu_factor_extend_last_coprime * eut_right_eu_factor_extend_last_coprime) -> eut_divisor_eu_factor_extend_last_coprime = 1) /\ (v)=(l)) \/ (~(forall eut_divisor_eu_factor_extend_last_coprime. (exists eut_left_eu_factor_extend_last_coprime. (l) = eut_divisor_eu_factor_extend_last_coprime * eut_left_eu_factor_extend_last_coprime) -> (exists eut_right_eu_factor_extend_last_coprime. (m) = eut_divisor_eu_factor_extend_last_coprime * eut_right_eu_factor_extend_last_coprime) -> eut_divisor_eu_factor_extend_last_coprime = 1) /\ (v)=1))) -> exists d e. (forall eu_factor_index_factors_extend_new. (exists eut_gap_eu_factors_extend_new_index. eut_gap_eu_factors_extend_new_index + S (eu_factor_index_factors_extend_new) = (S l)) -> exists eu_factor_value_factors_extend_new. (((exists fs_h_eu_factors_extend_new_at. fs_h_eu_factors_extend_new_at + S (eu_factor_value_factors_extend_new) = S ((S (eu_factor_index_factors_extend_new)) * e)) /\ exists fs_q_eu_factors_extend_new_at. d = fs_q_eu_factors_extend_new_at * S ((S (eu_factor_index_factors_extend_new)) * e) + (eu_factor_value_factors_extend_new))) /\ ((((forall eut_divisor_eu_factors_extend_new_choice_coprime. (exists eut_left_eu_factors_extend_new_choice_coprime. (eu_factor_index_factors_extend_new) = eut_divisor_eu_factors_extend_new_choice_coprime * eut_left_eu_factors_extend_new_choice_coprime) -> (exists eut_right_eu_factors_extend_new_choice_coprime. (m) = eut_divisor_eu_factors_extend_new_choice_coprime * eut_right_eu_factors_extend_new_choice_coprime) -> eut_divisor_eu_factors_extend_new_choice_coprime = 1) /\ (eu_factor_value_factors_extend_new)=(eu_factor_index_factors_extend_new)) \/ (~(forall eut_divisor_eu_factors_extend_new_choice_coprime. (exists eut_left_eu_factors_extend_new_choice_coprime. (eu_factor_index_factors_extend_new) = eut_divisor_eu_factors_extend_new_choice_coprime * eut_left_eu_factors_extend_new_choice_coprime) -> (exists eut_right_eu_factors_extend_new_choice_coprime. (m) = eut_divisor_eu_factors_extend_new_choice_coprime * eut_right_eu_factors_extend_new_choice_coprime) -> eut_divisor_eu_factors_extend_new_choice_coprime = 1) /\ (eu_factor_value_factors_extend_new)=1))))

Constructive proof overview

Generated structural guide

Actually append the independently chosen next factor while preserving every earlier factor.

The unchanged tactic script uses 2 declared prerequisites and contains 47 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_prefix_extend Stable theorem; checked-use authorized finite_lt_succ_eq_or_lt Stable theorem; checked-use authorized

Direct dependents

EU0014 euler_unit_product_prefix_exists

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

47 script commands · 18 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.

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

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

  1. L1
    intro m
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro l
  5. L5
    intro v
  6. L6
    intro h
  7. L7
    intro hv
02Use earlier factsL8–11

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

  1. L8
    specialize beta_prefix_extend l
  2. L9
    specialize beta_prefix_extend b
  3. L10
    specialize beta_prefix_extend c
  4. L11
    specialize beta_prefix_extend v
03Separate the logical casesL12–14

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

  1. L12
    cases beta_prefix_extend
  2. L13
    cases beta_prefix_extend_witness
  3. L14
    cases beta_prefix_extend_witness_witness
04Construct an explicit witnessL15–16

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

  1. L15
    exists x
  2. L16
    exists x1
05Fix variables and assumptionsL17–18

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

  1. L17
    intro i
  2. L18
    intro hi
06Establish hsL19–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L19
    have hs : i=l \/ (exists eut_gap_eu_factor_extend_index. eut_gap_eu_factor_extend_index + S (i) = (l))
  2. L20
    specialize finite_lt_succ_eq_or_lt (l)
  3. L21
    specialize finite_lt_succ_eq_or_lt (i)
  4. L22
    apply finite_lt_succ_eq_or_lt
  5. L23
    exact hi
07Separate the logical casesL24–24

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

  1. L24
    cases hs
08Construct an explicit witnessL25–25

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

  1. L25
    exists v
09Separate the logical casesL26–26

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

  1. L26
    split
10Calculate and transport equalitiesL27–28

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

  1. L27
    rewrite hs_left
  2. L28
    rewrite hs_left
11Use earlier factsL29–29

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

  1. L29
    exact beta_prefix_extend_witness_witness_left
12Calculate and transport equalitiesL30–32

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

  1. L30
    rewrite hs_left
  2. L31
    rewrite hs_left
  3. L32
    rewrite hs_left
13Use earlier factsL33–33

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

  1. L33
    exact hv
14Establish hpL34–37

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

  1. L34
    have hp : ∃ w. BetaAt(b,c,i,w) ∧ UnitProductFactor(m,i,w)Definitions: UnitProductFactorBetaAt
  2. L35
    specialize h (i)
  3. L36
    apply h
  4. L37
    exact hs_right
15Separate the logical casesL38–39

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

  1. L38
    cases hp
  2. L39
    cases hp_witness
16Construct an explicit witnessL40–40

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

  1. L40
    exists x2
17Separate the logical casesL41–41

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

  1. L41
    split
18Use earlier factsL42–47

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

  1. L42
    specialize beta_prefix_extend_witness_witness_right (i)
  2. L43
    specialize beta_prefix_extend_witness_witness_right (x2)
  3. L44
    apply beta_prefix_extend_witness_witness_right
  4. L45
    exact hs_right
  5. L46
    exact hp_witness_left
  6. L47
    exact hp_witness_right

Library-wide reading audit

Original exact command ledger · 47 lines
  1. 0001intro m
  2. 0002intro b
  3. 0003intro c
  4. 0004intro l
  5. 0005intro v
  6. 0006intro h
  7. 0007intro hv
  8. 0008specialize beta_prefix_extend l
  9. 0009specialize beta_prefix_extend b
  10. 0010specialize beta_prefix_extend c
  11. 0011specialize beta_prefix_extend v
  12. 0012cases beta_prefix_extend
  13. 0013cases beta_prefix_extend_witness
  14. 0014cases beta_prefix_extend_witness_witness
  15. 0015exists x
  16. 0016exists x1
  17. 0017intro i
  18. 0018intro hi
  19. 0019have hs : i=l \/ (exists eut_gap_eu_factor_extend_index. eut_gap_eu_factor_extend_index + S (i) = (l))
  20. 0020specialize finite_lt_succ_eq_or_lt (l)
  21. 0021specialize finite_lt_succ_eq_or_lt (i)
  22. 0022apply finite_lt_succ_eq_or_lt
  23. 0023exact hi
  24. 0024cases hs
  25. 0025exists v
  26. 0026split
  27. 0027rewrite hs_left
  28. 0028rewrite hs_left
  29. 0029exact beta_prefix_extend_witness_witness_left
  30. 0030rewrite hs_left
  31. 0031rewrite hs_left
  32. 0032rewrite hs_left
  33. 0033exact hv
  34. 0034have hp : exists w. (((exists fs_h_eu_factor_extend_old. fs_h_eu_factor_extend_old + S (w) = S ((S (i)) * c)) /\ exists fs_q_eu_factor_extend_old. b = fs_q_eu_factor_extend_old * S ((S (i)) * c) + (w))) /\ ((((forall eut_divisor_eu_factor_extend_old_coprime. (exists eut_left_eu_factor_extend_old_coprime. (i) = eut_divisor_eu_factor_extend_old_coprime * eut_left_eu_factor_extend_old_coprime) -> (exists eut_right_eu_factor_extend_old_coprime. (m) = eut_divisor_eu_factor_extend_old_coprime * eut_right_eu_factor_extend_old_coprime) -> eut_divisor_eu_factor_extend_old_coprime = 1) /\ (w)=(i)) \/ (~(forall eut_divisor_eu_factor_extend_old_coprime. (exists eut_left_eu_factor_extend_old_coprime. (i) = eut_divisor_eu_factor_extend_old_coprime * eut_left_eu_factor_extend_old_coprime) -> (exists eut_right_eu_factor_extend_old_coprime. (m) = eut_divisor_eu_factor_extend_old_coprime * eut_right_eu_factor_extend_old_coprime) -> eut_divisor_eu_factor_extend_old_coprime = 1) /\ (w)=1)))
  35. 0035specialize h (i)
  36. 0036apply h
  37. 0037exact hs_right
  38. 0038cases hp
  39. 0039cases hp_witness
  40. 0040exists x2
  41. 0041split
  42. 0042specialize beta_prefix_extend_witness_witness_right (i)
  43. 0043specialize beta_prefix_extend_witness_witness_right (x2)
  44. 0044apply beta_prefix_extend_witness_witness_right
  45. 0045exact hs_right
  46. 0046exact hp_witness_left
  47. 0047exact hp_witness_right