JT0030

jordan_tuple_congruence_trans

Actual decoded middle entries witness transitivity of coordinate congruence.

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

∀ n. ∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ k. JordanTupleCongruence(n,b,c,d,e,k) → JordanTupleCongruence(n,d,e,f,g,k) → JordanTupleCongruence(n,b,c,f,g,k)

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

Definition DAG

JordanTupleCongruence(n,b,c,d,e,k) · 3BetaAt(b,c,i,x) · 1

Actual proof prerequisites

beta_at_exists · checked external prerequisitemod_eq_trans · checked external prerequisite
Original expanded first-order statement 
forall n b c d e f g k. (forall jt_index_modtransfirst jt_left_modtransfirst jt_right_modtransfirst. (exists jt_gap_modtransfirstindex. jt_gap_modtransfirstindex+S (jt_index_modtransfirst)=(k)) -> (((exists fs_h_jt_modtransfirstleft. fs_h_jt_modtransfirstleft + S (jt_left_modtransfirst) = S ((S (jt_index_modtransfirst)) * c)) /\ exists fs_q_jt_modtransfirstleft. b = fs_q_jt_modtransfirstleft * S ((S (jt_index_modtransfirst)) * c) + (jt_left_modtransfirst))) -> (((exists fs_h_jt_modtransfirstright. fs_h_jt_modtransfirstright + S (jt_right_modtransfirst) = S ((S (jt_index_modtransfirst)) * e)) /\ exists fs_q_jt_modtransfirstright. d = fs_q_jt_modtransfirstright * S ((S (jt_index_modtransfirst)) * e) + (jt_right_modtransfirst))) -> (exists jt_left_modtransfirstmod jt_right_modtransfirstmod. (jt_left_modtransfirst)+(n)*jt_left_modtransfirstmod=(jt_right_modtransfirst)+(n)*jt_right_modtransfirstmod)) -> (forall jt_index_modtranssecond jt_left_modtranssecond jt_right_modtranssecond. (exists jt_gap_modtranssecondindex. jt_gap_modtranssecondindex+S (jt_index_modtranssecond)=(k)) -> (((exists fs_h_jt_modtranssecondleft. fs_h_jt_modtranssecondleft + S (jt_left_modtranssecond) = S ((S (jt_index_modtranssecond)) * e)) /\ exists fs_q_jt_modtranssecondleft. d = fs_q_jt_modtranssecondleft * S ((S (jt_index_modtranssecond)) * e) + (jt_left_modtranssecond))) -> (((exists fs_h_jt_modtranssecondright. fs_h_jt_modtranssecondright + S (jt_right_modtranssecond) = S ((S (jt_index_modtranssecond)) * g)) /\ exists fs_q_jt_modtranssecondright. f = fs_q_jt_modtranssecondright * S ((S (jt_index_modtranssecond)) * g) + (jt_right_modtranssecond))) -> (exists jt_left_modtranssecondmod jt_right_modtranssecondmod. (jt_left_modtranssecond)+(n)*jt_left_modtranssecondmod=(jt_right_modtranssecond)+(n)*jt_right_modtranssecondmod)) -> (forall jt_index_modtransresult jt_left_modtransresult jt_right_modtransresult. (exists jt_gap_modtransresultindex. jt_gap_modtransresultindex+S (jt_index_modtransresult)=(k)) -> (((exists fs_h_jt_modtransresultleft. fs_h_jt_modtransresultleft + S (jt_left_modtransresult) = S ((S (jt_index_modtransresult)) * c)) /\ exists fs_q_jt_modtransresultleft. b = fs_q_jt_modtransresultleft * S ((S (jt_index_modtransresult)) * c) + (jt_left_modtransresult))) -> (((exists fs_h_jt_modtransresultright. fs_h_jt_modtransresultright + S (jt_right_modtransresult) = S ((S (jt_index_modtransresult)) * g)) /\ exists fs_q_jt_modtransresultright. f = fs_q_jt_modtransresultright * S ((S (jt_index_modtransresult)) * g) + (jt_right_modtransresult))) -> (exists jt_left_modtransresultmod jt_right_modtransresultmod. (jt_left_modtransresult)+(n)*jt_left_modtransresultmod=(jt_right_modtransresult)+(n)*jt_right_modtransresultmod))

Complete tactic proof in conservative notation

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

41 script commands · 6 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.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro n
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro d
  5. L5
    intro e
  6. L6
    intro f
  7. L7
    intro g
  8. L8
    intro k
  9. L9
    intro hleft
  10. L10
    intro hright
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
03Establish hxL17–21

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

  1. L17
    have hx : ∃ x. BetaAt(d,e,i,x)Definitions: BetaAt(d,e,i,x)Original native command in the exact edition
  2. L18
    specialize beta_at_exists (d)
  3. L19
    specialize beta_at_exists (e)
  4. L20
    specialize beta_at_exists (i)
  5. L21
    apply beta_at_exists
04Separate the logical casesL22–22

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

  1. L22
    cases hx
05Use earlier factsL23–32

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

  1. L23
    specialize mod_eq_trans (n)
  2. L24
    specialize mod_eq_trans (a)
  3. L25
    specialize mod_eq_trans (x)
  4. L26
    specialize mod_eq_trans (z)
  5. L27
    apply mod_eq_trans
  6. L28
    specialize hleft (i)
  7. L29
    specialize hleft (a)
  8. L30
    specialize hleft (x)
  9. L31
    apply hleft
  10. L32
    exact hi
06Use earlier factsL33–41

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

  1. L33
    exact ha
  2. L34
    exact hx_witness
  3. L35
    specialize hright (i)
  4. L36
    specialize hright (x)
  5. L37
    specialize hright (z)
  6. L38
    apply hright
  7. L39
    exact hi
  8. L40
    exact hx_witness
  9. L41
    exact hz

Library-wide reading audit

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