JT0031

jordan_tuple_congruence_divisor

Coordinate congruence descends along actual divisibility of moduli.

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. Dvd(m,n) → JordanTupleCongruence(n,b,c,d,e,k) → JordanTupleCongruence(m,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) · 2Dvd(d,n) · 1

Actual proof prerequisites

mod_eq_of_mod_eq_multiple · checked external prerequisite
Original expanded first-order statement 
forall m n b c d e k. (exists jt_factor_moddivisor. (n)=(m)*jt_factor_moddivisor) -> (forall jt_index_modlarger jt_left_modlarger jt_right_modlarger. (exists jt_gap_modlargerindex. jt_gap_modlargerindex+S (jt_index_modlarger)=(k)) -> (((exists fs_h_jt_modlargerleft. fs_h_jt_modlargerleft + S (jt_left_modlarger) = S ((S (jt_index_modlarger)) * c)) /\ exists fs_q_jt_modlargerleft. b = fs_q_jt_modlargerleft * S ((S (jt_index_modlarger)) * c) + (jt_left_modlarger))) -> (((exists fs_h_jt_modlargerright. fs_h_jt_modlargerright + S (jt_right_modlarger) = S ((S (jt_index_modlarger)) * e)) /\ exists fs_q_jt_modlargerright. d = fs_q_jt_modlargerright * S ((S (jt_index_modlarger)) * e) + (jt_right_modlarger))) -> (exists jt_left_modlargermod jt_right_modlargermod. (jt_left_modlarger)+(n)*jt_left_modlargermod=(jt_right_modlarger)+(n)*jt_right_modlargermod)) -> (forall jt_index_modsmaller jt_left_modsmaller jt_right_modsmaller. (exists jt_gap_modsmallerindex. jt_gap_modsmallerindex+S (jt_index_modsmaller)=(k)) -> (((exists fs_h_jt_modsmallerleft. fs_h_jt_modsmallerleft + S (jt_left_modsmaller) = S ((S (jt_index_modsmaller)) * c)) /\ exists fs_q_jt_modsmallerleft. b = fs_q_jt_modsmallerleft * S ((S (jt_index_modsmaller)) * c) + (jt_left_modsmaller))) -> (((exists fs_h_jt_modsmallerright. fs_h_jt_modsmallerright + S (jt_right_modsmaller) = S ((S (jt_index_modsmaller)) * e)) /\ exists fs_q_jt_modsmallerright. d = fs_q_jt_modsmallerright * S ((S (jt_index_modsmaller)) * e) + (jt_right_modsmaller))) -> (exists jt_left_modsmallermod jt_right_modsmallermod. (jt_left_modsmaller)+(m)*jt_left_modsmallermod=(jt_right_modsmaller)+(m)*jt_right_modsmallermod))

Complete tactic proof in conservative notation

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

28 script commands · 4 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 hdiv
  9. L9
    intro hmod
  10. L10
    intro i
02Fix variables and assumptionsL11–15

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

  1. L11
    intro a
  2. L12
    intro z
  3. L13
    intro hi
  4. L14
    intro ha
  5. L15
    intro hz
03Use earlier factsL16–25

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

  1. L16
    specialize mod_eq_of_mod_eq_multiple (m)
  2. L17
    specialize mod_eq_of_mod_eq_multiple (n)
  3. L18
    specialize mod_eq_of_mod_eq_multiple (a)
  4. L19
    specialize mod_eq_of_mod_eq_multiple (z)
  5. L20
    apply mod_eq_of_mod_eq_multiple
  6. L21
    exact hdiv
  7. L22
    specialize hmod (i)
  8. L23
    specialize hmod (a)
  9. L24
    specialize hmod (z)
  10. L25
    apply hmod
04Use earlier factsL26–28

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

  1. L26
    exact hi
  2. L27
    exact ha
  3. L28
    exact hz

Library-wide reading audit

Original defined command ledger · 28 lines
  1. 0001intro m
  2. 0002intro n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro e
  7. 0007intro k
  8. 0008intro hdiv
  9. 0009intro hmod
  10. 0010intro i
  11. 0011intro a
  12. 0012intro z
  13. 0013intro hi
  14. 0014intro ha
  15. 0015intro hz
  16. 0016specialize mod_eq_of_mod_eq_multiple (m)
  17. 0017specialize mod_eq_of_mod_eq_multiple (n)
  18. 0018specialize mod_eq_of_mod_eq_multiple (a)
  19. 0019specialize mod_eq_of_mod_eq_multiple (z)
  20. 0020apply mod_eq_of_mod_eq_multiple
  21. 0021exact hdiv
  22. 0022specialize hmod (i)
  23. 0023specialize hmod (a)
  24. 0024specialize hmod (z)
  25. 0025apply hmod
  26. 0026exact hi
  27. 0027exact ha
  28. 0028exact hz