EU0014

euler_unit_product_prefix_exists

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.

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

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. ∀ l. ∃ b. ∃ c. UnitProductPrefix(m,b,c,l)

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

Definition DAG

UnitProductFactor(m,i,v) · 1UnitProductPrefix(m,b,c,l) · 1

Actual proof prerequisites

euler_unit_product_prefix_emptyeuler_unit_product_factor_existseuler_unit_product_prefix_extend
Original expanded first-order 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))))

Complete tactic proof in conservative notation

All 23 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

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.

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

Named ingredients (3)
euler unit product prefix emptyeuler unit product factor existseuler unit product prefix extend
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(m,l,v)Original native command in the exact edition
  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 defined 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 : ∃ v. UnitProductFactor(m,l,v)
  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