JT0030

jordan_tuple_congruence_trans

Alpha v35 independently verified · alpha_closed; checked-use authorized; not Stable

Actual decoded middle entries witness transitivity of coordinate congruence.

Exact expanded first-order arithmetic 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))

Constructive proof overview

Generated structural guide

Actual decoded middle entries witness transitivity of coordinate congruence.

The unchanged tactic script uses 2 declared prerequisites and contains 41 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_at_exists Alpha theorem; checked-use authorized mod_eq_trans Alpha theorem; checked-use authorized

Direct dependents

JT0032 jordan_canonical_crt_tuple_exists JT003B jordan_crt_component_recovery JT003C jordan_canonical_crt_tuple_unique JT0045 jordan_enumeration_reduce_primitive

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 : exists x. ((exists fs_h_jt_modtransmiddle. fs_h_jt_modtransmiddle + S (x) = S ((S (i)) * e)) /\ exists fs_q_jt_modtransmiddle. d = fs_q_jt_modtransmiddle * S ((S (i)) * e) + (x))
  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 exact 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 : exists x. ((exists fs_h_jt_modtransmiddle. fs_h_jt_modtransmiddle + S (x) = S ((S (i)) * e)) /\ exists fs_q_jt_modtransmiddle. d = fs_q_jt_modtransmiddle * S ((S (i)) * e) + (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