EU0013

euler_unit_product_prefix_extend

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.

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

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

The exact G014 theorem is proved in this research checkpoint for m>1 and genuinely invertible a. Phi counts coprime residues independently of the conclusion. The broader coprime theorem also handles m=1 by congruence, not by asserting that one is a canonical remainder. No multiplicative-order or RSA theorem is claimed. The published atlas and Alpha membership are unchanged.

Exact theorem in conservative defined notation

∀ m. ∀ b. ∀ c. ∀ l. ∀ v. UnitProductPrefix(m,b,c,l) → UnitProductFactor(m,l,v) → ∃ x. ∃ y. UnitProductPrefix(m,x,y,S l)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

UnitProductFactor(m,i,v) · 2UnitProductPrefix(m,b,c,l) · 2Lt(a,b) · 1BetaAt(b,c,i,x) · 1

Actual proof prerequisites

beta_prefix_extend · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisite
Original expanded first-order 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))))

Complete tactic proof in conservative notation

All 47 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  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: BetaAt(b,c,i,w)UnitProductFactor(m,i,w)Original native command in the exact edition
  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 defined 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 ∨ Lt(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 : ∃ w. BetaAt(b,c,i,w) ∧ UnitProductFactor(m,i,w)
  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