JT002E

jordan_crt_tuple_right

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

Every actual output coordinate has the required right congruence.

Exact expanded first-order arithmetic statement

forall m n b c d e f g k. (forall jt_index_crtright. (exists jt_gap_crtrightindex. jt_gap_crtrightindex+S (jt_index_crtright)=(k)) -> exists jt_left_crtright jt_right_crtright jt_output_crtright. ((((exists fs_h_jt_crtrightleft. fs_h_jt_crtrightleft + S (jt_left_crtright) = S ((S (jt_index_crtright)) * c)) /\ exists fs_q_jt_crtrightleft. b = fs_q_jt_crtrightleft * S ((S (jt_index_crtright)) * c) + (jt_left_crtright))) /\ (((((exists fs_h_jt_crtrightright. fs_h_jt_crtrightright + S (jt_right_crtright) = S ((S (jt_index_crtright)) * e)) /\ exists fs_q_jt_crtrightright. d = fs_q_jt_crtrightright * S ((S (jt_index_crtright)) * e) + (jt_right_crtright))) /\ (((((exists fs_h_jt_crtrightoutput. fs_h_jt_crtrightoutput + S (jt_output_crtright) = S ((S (jt_index_crtright)) * g)) /\ exists fs_q_jt_crtrightoutput. f = fs_q_jt_crtrightoutput * S ((S (jt_index_crtright)) * g) + (jt_output_crtright))) /\ (((exists jt_left_crtrightmodleft jt_right_crtrightmodleft. (jt_output_crtright)+(m)*jt_left_crtrightmodleft=(jt_left_crtright)+(m)*jt_right_crtrightmodleft) /\ (exists jt_left_crtrightmodright jt_right_crtrightmodright. (jt_output_crtright)+(n)*jt_left_crtrightmodright=(jt_right_crtright)+(n)*jt_right_crtrightmodright))))))))) -> (forall jt_index_crtprojectionright jt_left_crtprojectionright jt_right_crtprojectionright. (exists jt_gap_crtprojectionrightindex. jt_gap_crtprojectionrightindex+S (jt_index_crtprojectionright)=(k)) -> (((exists fs_h_jt_crtprojectionrightleft. fs_h_jt_crtprojectionrightleft + S (jt_left_crtprojectionright) = S ((S (jt_index_crtprojectionright)) * g)) /\ exists fs_q_jt_crtprojectionrightleft. f = fs_q_jt_crtprojectionrightleft * S ((S (jt_index_crtprojectionright)) * g) + (jt_left_crtprojectionright))) -> (((exists fs_h_jt_crtprojectionrightright. fs_h_jt_crtprojectionrightright + S (jt_right_crtprojectionright) = S ((S (jt_index_crtprojectionright)) * e)) /\ exists fs_q_jt_crtprojectionrightright. d = fs_q_jt_crtprojectionrightright * S ((S (jt_index_crtprojectionright)) * e) + (jt_right_crtprojectionright))) -> (exists jt_left_crtprojectionrightmod jt_right_crtprojectionrightmod. (jt_left_crtprojectionright)+(n)*jt_left_crtprojectionrightmod=(jt_right_crtprojectionright)+(n)*jt_right_crtprojectionrightmod))

Constructive proof overview

Generated structural guide

Every actual output coordinate has the required right congruence.

The unchanged tactic script uses 1 declared prerequisite and contains 48 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_at_unique Alpha theorem; checked-use authorized

Direct dependents

JT0032 jordan_canonical_crt_tuple_exists

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

48 script commands · 8 reading checkpoints · 3 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.

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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 f
  8. L8
    intro g
  9. L9
    intro k
  10. L10
    intro h
02Fix variables and assumptionsL11–16

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

  1. L11
    intro i
  2. L12
    intro w
  3. L13
    intro a
  4. L14
    intro hi
  5. L15
    intro hw
  6. L16
    intro ha
03Establish htL17–20

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

  1. L17
    have ht : ∃ u. ∃ v. ∃ q. BetaAt(b,c,i,u) ∧ (BetaAt(d,e,i,v) ∧ (BetaAt(f,g,i,q) ∧ (ModEq(m,q,u) ∧ ModEq(n,q,v))))Definitions: ModEqBetaAt
  2. L18
    specialize h (i)
  3. L19
    apply h
  4. L20
    exact hi
04Separate the logical casesL21–27

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

  1. L21
    cases ht
  2. L22
    cases ht_witness
  3. L23
    cases ht_witness_witness
  4. L24
    cases ht_witness_witness_witness
  5. L25
    cases ht_witness_witness_witness_right
  6. L26
    cases ht_witness_witness_witness_right_right
  7. L27
    cases ht_witness_witness_witness_right_right_right
05Establish houtL28–36

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

  1. L28
    have hout : x2=w
  2. L29
    specialize beta_at_unique (f)
  3. L30
    specialize beta_at_unique (g)
  4. L31
    specialize beta_at_unique (i)
  5. L32
    specialize beta_at_unique (x2)
  6. L33
    specialize beta_at_unique (w)
  7. L34
    apply beta_at_unique
  8. L35
    exact ht_witness_witness_witness_right_right_left
  9. L36
    exact hw
06Establish hinL37–46

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

  1. L37
    have hin : x1=a
  2. L38
    specialize beta_at_unique (d)
  3. L39
    specialize beta_at_unique (e)
  4. L40
    specialize beta_at_unique (i)
  5. L41
    specialize beta_at_unique (x1)
  6. L42
    specialize beta_at_unique (a)
  7. L43
    apply beta_at_unique
  8. L44
    exact ht_witness_witness_witness_right_left
  9. L45
    exact ha
  10. L46
    rewrite hout at ht_witness_witness_witness_right_right_right_right
07Calculate and transport equalitiesL47–47

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L47
    rewrite hin at ht_witness_witness_witness_right_right_right_right
08Use earlier factsL48–48

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

  1. L48
    exact ht_witness_witness_witness_right_right_right_right

Library-wide reading audit

Original exact command ledger · 48 lines
  1. 0001intro m
  2. 0002intro n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro e
  7. 0007intro f
  8. 0008intro g
  9. 0009intro k
  10. 0010intro h
  11. 0011intro i
  12. 0012intro w
  13. 0013intro a
  14. 0014intro hi
  15. 0015intro hw
  16. 0016intro ha
  17. 0017have ht : exists u v q. ((((exists fs_h_jt_crtpointleft. fs_h_jt_crtpointleft + S (u) = S ((S (i)) * c)) /\ exists fs_q_jt_crtpointleft. b = fs_q_jt_crtpointleft * S ((S (i)) * c) + (u))) /\ (((((exists fs_h_jt_crtpointright. fs_h_jt_crtpointright + S (v) = S ((S (i)) * e)) /\ exists fs_q_jt_crtpointright. d = fs_q_jt_crtpointright * S ((S (i)) * e) + (v))) /\ (((((exists fs_h_jt_crtpointoutput. fs_h_jt_crtpointoutput + S (q) = S ((S (i)) * g)) /\ exists fs_q_jt_crtpointoutput. f = fs_q_jt_crtpointoutput * S ((S (i)) * g) + (q))) /\ (((exists jt_left_crtpointmodleft jt_right_crtpointmodleft. (q)+(m)*jt_left_crtpointmodleft=(u)+(m)*jt_right_crtpointmodleft) /\ (exists jt_left_crtpointmodright jt_right_crtpointmodright. (q)+(n)*jt_left_crtpointmodright=(v)+(n)*jt_right_crtpointmodright))))))))
  18. 0018specialize h (i)
  19. 0019apply h
  20. 0020exact hi
  21. 0021cases ht
  22. 0022cases ht_witness
  23. 0023cases ht_witness_witness
  24. 0024cases ht_witness_witness_witness
  25. 0025cases ht_witness_witness_witness_right
  26. 0026cases ht_witness_witness_witness_right_right
  27. 0027cases ht_witness_witness_witness_right_right_right
  28. 0028have hout : x2=w
  29. 0029specialize beta_at_unique (f)
  30. 0030specialize beta_at_unique (g)
  31. 0031specialize beta_at_unique (i)
  32. 0032specialize beta_at_unique (x2)
  33. 0033specialize beta_at_unique (w)
  34. 0034apply beta_at_unique
  35. 0035exact ht_witness_witness_witness_right_right_left
  36. 0036exact hw
  37. 0037have hin : x1=a
  38. 0038specialize beta_at_unique (d)
  39. 0039specialize beta_at_unique (e)
  40. 0040specialize beta_at_unique (i)
  41. 0041specialize beta_at_unique (x1)
  42. 0042specialize beta_at_unique (a)
  43. 0043apply beta_at_unique
  44. 0044exact ht_witness_witness_witness_right_left
  45. 0045exact ha
  46. 0046rewrite hout at ht_witness_witness_witness_right_right_right_right
  47. 0047rewrite hin at ht_witness_witness_witness_right_right_right_right
  48. 0048exact ht_witness_witness_witness_right_right_right_right