JT003A

jordan_tuple_congruence_coprime_product

The actual universal-property lcm merges both coordinate congruences.

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

95 new Alpha admissions come from 96 source lemmas: tuple equality reflexivity reuses an already-admitted theorem and is not counted twice. All counts use actual finite beta-coded enumerations. G008 multiplicativity is proved; the general prime-power count and distinct-prime product formula are further goals. General prime-power fields (G091) remain open. Stable is unchanged.

Exact theorem in conservative defined notation

∀ m. ∀ n. ∀ b. ∀ c. ∀ d. ∀ e. ∀ k. Coprime(m,n) → JordanTupleCongruence(m,b,c,d,e,k) → JordanTupleCongruence(n,b,c,d,e,k) → JordanTupleCongruence(m · n,b,c,d,e,k)

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

Definition DAG

JordanTupleCongruence(n,b,c,d,e,k) · 3Coprime(a,b) · 1

Actual proof prerequisites

mod_eq_lcm_merge · checked external prerequisitecoprime_product_is_lcm · checked external prerequisite
Original expanded first-order statement 
forall m n b c d e k. (forall jt_divisor_combinecop. (exists jt_factor_combinecopa. (m)=(jt_divisor_combinecop)*jt_factor_combinecopa) -> (exists jt_factor_combinecopb. (n)=(jt_divisor_combinecop)*jt_factor_combinecopb) -> jt_divisor_combinecop=1) -> (forall jt_index_combinem jt_left_combinem jt_right_combinem. (exists jt_gap_combinemindex. jt_gap_combinemindex+S (jt_index_combinem)=(k)) -> (((exists fs_h_jt_combinemleft. fs_h_jt_combinemleft + S (jt_left_combinem) = S ((S (jt_index_combinem)) * c)) /\ exists fs_q_jt_combinemleft. b = fs_q_jt_combinemleft * S ((S (jt_index_combinem)) * c) + (jt_left_combinem))) -> (((exists fs_h_jt_combinemright. fs_h_jt_combinemright + S (jt_right_combinem) = S ((S (jt_index_combinem)) * e)) /\ exists fs_q_jt_combinemright. d = fs_q_jt_combinemright * S ((S (jt_index_combinem)) * e) + (jt_right_combinem))) -> (exists jt_left_combinemmod jt_right_combinemmod. (jt_left_combinem)+(m)*jt_left_combinemmod=(jt_right_combinem)+(m)*jt_right_combinemmod)) -> (forall jt_index_combinen jt_left_combinen jt_right_combinen. (exists jt_gap_combinenindex. jt_gap_combinenindex+S (jt_index_combinen)=(k)) -> (((exists fs_h_jt_combinenleft. fs_h_jt_combinenleft + S (jt_left_combinen) = S ((S (jt_index_combinen)) * c)) /\ exists fs_q_jt_combinenleft. b = fs_q_jt_combinenleft * S ((S (jt_index_combinen)) * c) + (jt_left_combinen))) -> (((exists fs_h_jt_combinenright. fs_h_jt_combinenright + S (jt_right_combinen) = S ((S (jt_index_combinen)) * e)) /\ exists fs_q_jt_combinenright. d = fs_q_jt_combinenright * S ((S (jt_index_combinen)) * e) + (jt_right_combinen))) -> (exists jt_left_combinenmod jt_right_combinenmod. (jt_left_combinen)+(n)*jt_left_combinenmod=(jt_right_combinen)+(n)*jt_right_combinenmod)) -> (forall jt_index_combineproduct jt_left_combineproduct jt_right_combineproduct. (exists jt_gap_combineproductindex. jt_gap_combineproductindex+S (jt_index_combineproduct)=(k)) -> (((exists fs_h_jt_combineproductleft. fs_h_jt_combineproductleft + S (jt_left_combineproduct) = S ((S (jt_index_combineproduct)) * c)) /\ exists fs_q_jt_combineproductleft. b = fs_q_jt_combineproductleft * S ((S (jt_index_combineproduct)) * c) + (jt_left_combineproduct))) -> (((exists fs_h_jt_combineproductright. fs_h_jt_combineproductright + S (jt_right_combineproduct) = S ((S (jt_index_combineproduct)) * e)) /\ exists fs_q_jt_combineproductright. d = fs_q_jt_combineproductright * S ((S (jt_index_combineproduct)) * e) + (jt_right_combineproduct))) -> (exists jt_left_combineproductmod jt_right_combineproductmod. (jt_left_combineproduct)+(m*n)*jt_left_combineproductmod=(jt_right_combineproduct)+(m*n)*jt_right_combineproductmod))

Complete tactic proof in conservative notation

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

40 script commands · 5 reading checkpoints · 0 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–10

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

  1. L1
    intro m
  2. L2
    intro n
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro d
  6. L6
    intro e
  7. L7
    intro k
  8. L8
    intro hcop
  9. L9
    intro hm
  10. L10
    intro hn
02Fix variables and assumptionsL11–16

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

  1. L11
    intro i
  2. L12
    intro a
  3. L13
    intro z
  4. L14
    intro hi
  5. L15
    intro ha
  6. L16
    intro hz
03Use earlier factsL17–26

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

  1. L17
    specialize mod_eq_lcm_merge (m*n)
  2. L18
    specialize mod_eq_lcm_merge (m)
  3. L19
    specialize mod_eq_lcm_merge (n)
  4. L20
    specialize mod_eq_lcm_merge (a)
  5. L21
    specialize mod_eq_lcm_merge (z)
  6. L22
    apply mod_eq_lcm_merge
  7. L23
    specialize coprime_product_is_lcm (m)
  8. L24
    specialize coprime_product_is_lcm (n)
  9. L25
    apply coprime_product_is_lcm
  10. L26
    exact hcop
04Use earlier factsL27–36

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

  1. L27
    specialize hm (i)
  2. L28
    specialize hm (a)
  3. L29
    specialize hm (z)
  4. L30
    apply hm
  5. L31
    exact hi
  6. L32
    exact ha
  7. L33
    exact hz
  8. L34
    specialize hn (i)
  9. L35
    specialize hn (a)
  10. L36
    specialize hn (z)
05Use earlier factsL37–40

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

  1. L37
    apply hn
  2. L38
    exact hi
  3. L39
    exact ha
  4. L40
    exact hz

Library-wide reading audit

Original defined command ledger · 40 lines
  1. 0001intro m
  2. 0002intro n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro e
  7. 0007intro k
  8. 0008intro hcop
  9. 0009intro hm
  10. 0010intro hn
  11. 0011intro i
  12. 0012intro a
  13. 0013intro z
  14. 0014intro hi
  15. 0015intro ha
  16. 0016intro hz
  17. 0017specialize mod_eq_lcm_merge (m*n)
  18. 0018specialize mod_eq_lcm_merge (m)
  19. 0019specialize mod_eq_lcm_merge (n)
  20. 0020specialize mod_eq_lcm_merge (a)
  21. 0021specialize mod_eq_lcm_merge (z)
  22. 0022apply mod_eq_lcm_merge
  23. 0023specialize coprime_product_is_lcm (m)
  24. 0024specialize coprime_product_is_lcm (n)
  25. 0025apply coprime_product_is_lcm
  26. 0026exact hcop
  27. 0027specialize hm (i)
  28. 0028specialize hm (a)
  29. 0029specialize hm (z)
  30. 0030apply hm
  31. 0031exact hi
  32. 0032exact ha
  33. 0033exact hz
  34. 0034specialize hn (i)
  35. 0035specialize hn (a)
  36. 0036specialize hn (z)
  37. 0037apply hn
  38. 0038exact hi
  39. 0039exact ha
  40. 0040exact hz