JT002C

jordan_crt_tuple_exists

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

Construct simultaneous residue representatives coordinate by coordinate, without any tuple totality premise.

Exact expanded first-order arithmetic statement

forall m n b c d e. ~(m=0) -> ~(n=0) -> (forall jt_divisor_crtcoprime. (exists jt_factor_crtcoprimea. (m)=(jt_divisor_crtcoprime)*jt_factor_crtcoprimea) -> (exists jt_factor_crtcoprimeb. (n)=(jt_divisor_crtcoprime)*jt_factor_crtcoprimeb) -> jt_divisor_crtcoprime=1) -> forall k. exists f g. forall jt_index_crtexists. (exists jt_gap_crtexistsindex. jt_gap_crtexistsindex+S (jt_index_crtexists)=(k)) -> exists jt_left_crtexists jt_right_crtexists jt_output_crtexists. ((((exists fs_h_jt_crtexistsleft. fs_h_jt_crtexistsleft + S (jt_left_crtexists) = S ((S (jt_index_crtexists)) * c)) /\ exists fs_q_jt_crtexistsleft. b = fs_q_jt_crtexistsleft * S ((S (jt_index_crtexists)) * c) + (jt_left_crtexists))) /\ (((((exists fs_h_jt_crtexistsright. fs_h_jt_crtexistsright + S (jt_right_crtexists) = S ((S (jt_index_crtexists)) * e)) /\ exists fs_q_jt_crtexistsright. d = fs_q_jt_crtexistsright * S ((S (jt_index_crtexists)) * e) + (jt_right_crtexists))) /\ (((((exists fs_h_jt_crtexistsoutput. fs_h_jt_crtexistsoutput + S (jt_output_crtexists) = S ((S (jt_index_crtexists)) * g)) /\ exists fs_q_jt_crtexistsoutput. f = fs_q_jt_crtexistsoutput * S ((S (jt_index_crtexists)) * g) + (jt_output_crtexists))) /\ (((exists jt_left_crtexistsmodleft jt_right_crtexistsmodleft. (jt_output_crtexists)+(m)*jt_left_crtexistsmodleft=(jt_left_crtexists)+(m)*jt_right_crtexistsmodleft) /\ (exists jt_left_crtexistsmodright jt_right_crtexistsmodright. (jt_output_crtexists)+(n)*jt_left_crtexistsmodright=(jt_right_crtexists)+(n)*jt_right_crtexistsmodright))))))))

Constructive proof overview

Generated structural guide

Construct simultaneous residue representatives coordinate by coordinate, without any tuple totality premise.

The unchanged tactic script uses 4 declared prerequisites and contains 64 exact native proof lines.

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

Proof neighborhood

Direct dependencies

JT002A jordan_crt_tuple_empty beta_at_exists Alpha theorem; checked-use authorized binary_crt Alpha theorem; checked-use authorized JT002B jordan_crt_tuple_extend

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

64 script commands · 13 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.

Named ingredients (2)
jordan crt tuple emptyjordan crt tuple extend
01Fix variables and assumptionsL1–9

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 hm
  8. L8
    intro hn
  9. L9
    intro hcop
02Induction on kL10–10

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L10
    induction k
03Construct an explicit witnessL11–12

Supply the displayed value, then prove that it has the required property.

  1. L11
    exists 0
  2. L12
    exists 0
04Use earlier factsL13–21

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

  1. L13
    specialize jordan_crt_tuple_empty (m)
  2. L14
    specialize jordan_crt_tuple_empty (n)
  3. L15
    specialize jordan_crt_tuple_empty (b)
  4. L16
    specialize jordan_crt_tuple_empty (c)
  5. L17
    specialize jordan_crt_tuple_empty (d)
  6. L18
    specialize jordan_crt_tuple_empty (e)
  7. L19
    specialize jordan_crt_tuple_empty (0)
  8. L20
    specialize jordan_crt_tuple_empty (0)
  9. L21
    apply jordan_crt_tuple_empty
05Separate the logical casesL22–23

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

  1. L22
    cases IH
  2. L23
    cases IH_witness
06Establish haL24–28

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

  1. L24
    have ha : exists a. ((exists fs_h_jt_crttotalleft. fs_h_jt_crttotalleft + S (a) = S ((S (k)) * c)) /\ exists fs_q_jt_crttotalleft. b = fs_q_jt_crttotalleft * S ((S (k)) * c) + (a))
  2. L25
    specialize beta_at_exists (b)
  3. L26
    specialize beta_at_exists (c)
  4. L27
    specialize beta_at_exists (k)
  5. L28
    apply beta_at_exists
07Separate the logical casesL29–29

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

  1. L29
    cases ha
08Establish hzL30–34

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

  1. L30
    have hz : exists z. ((exists fs_h_jt_crttotalright. fs_h_jt_crttotalright + S (z) = S ((S (k)) * e)) /\ exists fs_q_jt_crttotalright. d = fs_q_jt_crttotalright * S ((S (k)) * e) + (z))
  2. L31
    specialize beta_at_exists (d)
  3. L32
    specialize beta_at_exists (e)
  4. L33
    specialize beta_at_exists (k)
  5. L34
    apply beta_at_exists
09Separate the logical casesL35–35

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

  1. L35
    cases hz
10Establish hwL36–44

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

  1. L36
    have hw : exists w. ((exists jt_left_crttotalmodleft jt_right_crttotalmodleft. (w)+(m)*jt_left_crttotalmodleft=(x2)+(m)*jt_right_crttotalmodleft) /\ (exists jt_left_crttotalmodright jt_right_crttotalmodright. (w)+(n)*jt_left_crttotalmodright=(x3)+(n)*jt_right_crttotalmodright))
  2. L37
    specialize binary_crt (m)
  3. L38
    specialize binary_crt (n)
  4. L39
    specialize binary_crt (x2)
  5. L40
    specialize binary_crt (x3)
  6. L41
    apply binary_crt
  7. L42
    exact hm
  8. L43
    exact hn
  9. L44
    exact hcop
11Separate the logical casesL45–46

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

  1. L45
    cases hw
  2. L46
    cases hw_witness
12Use earlier factsL47–56

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

  1. L47
    specialize jordan_crt_tuple_extend (m)
  2. L48
    specialize jordan_crt_tuple_extend (n)
  3. L49
    specialize jordan_crt_tuple_extend (b)
  4. L50
    specialize jordan_crt_tuple_extend (c)
  5. L51
    specialize jordan_crt_tuple_extend (d)
  6. L52
    specialize jordan_crt_tuple_extend (e)
  7. L53
    specialize jordan_crt_tuple_extend (x)
  8. L54
    specialize jordan_crt_tuple_extend (x1)
  9. L55
    specialize jordan_crt_tuple_extend (k)
  10. L56
    specialize jordan_crt_tuple_extend (x2)
13Use earlier factsL57–64

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

  1. L57
    specialize jordan_crt_tuple_extend (x3)
  2. L58
    specialize jordan_crt_tuple_extend (x4)
  3. L59
    apply jordan_crt_tuple_extend
  4. L60
    exact IH_witness_witness
  5. L61
    exact ha_witness
  6. L62
    exact hz_witness
  7. L63
    exact hw_witness_left
  8. L64
    exact hw_witness_right

Library-wide reading audit

Original exact command ledger · 64 lines
  1. 0001intro m
  2. 0002intro n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro e
  7. 0007intro hm
  8. 0008intro hn
  9. 0009intro hcop
  10. 0010induction k
  11. 0011exists 0
  12. 0012exists 0
  13. 0013specialize jordan_crt_tuple_empty (m)
  14. 0014specialize jordan_crt_tuple_empty (n)
  15. 0015specialize jordan_crt_tuple_empty (b)
  16. 0016specialize jordan_crt_tuple_empty (c)
  17. 0017specialize jordan_crt_tuple_empty (d)
  18. 0018specialize jordan_crt_tuple_empty (e)
  19. 0019specialize jordan_crt_tuple_empty (0)
  20. 0020specialize jordan_crt_tuple_empty (0)
  21. 0021apply jordan_crt_tuple_empty
  22. 0022cases IH
  23. 0023cases IH_witness
  24. 0024have ha : exists a. ((exists fs_h_jt_crttotalleft. fs_h_jt_crttotalleft + S (a) = S ((S (k)) * c)) /\ exists fs_q_jt_crttotalleft. b = fs_q_jt_crttotalleft * S ((S (k)) * c) + (a))
  25. 0025specialize beta_at_exists (b)
  26. 0026specialize beta_at_exists (c)
  27. 0027specialize beta_at_exists (k)
  28. 0028apply beta_at_exists
  29. 0029cases ha
  30. 0030have hz : exists z. ((exists fs_h_jt_crttotalright. fs_h_jt_crttotalright + S (z) = S ((S (k)) * e)) /\ exists fs_q_jt_crttotalright. d = fs_q_jt_crttotalright * S ((S (k)) * e) + (z))
  31. 0031specialize beta_at_exists (d)
  32. 0032specialize beta_at_exists (e)
  33. 0033specialize beta_at_exists (k)
  34. 0034apply beta_at_exists
  35. 0035cases hz
  36. 0036have hw : exists w. ((exists jt_left_crttotalmodleft jt_right_crttotalmodleft. (w)+(m)*jt_left_crttotalmodleft=(x2)+(m)*jt_right_crttotalmodleft) /\ (exists jt_left_crttotalmodright jt_right_crttotalmodright. (w)+(n)*jt_left_crttotalmodright=(x3)+(n)*jt_right_crttotalmodright))
  37. 0037specialize binary_crt (m)
  38. 0038specialize binary_crt (n)
  39. 0039specialize binary_crt (x2)
  40. 0040specialize binary_crt (x3)
  41. 0041apply binary_crt
  42. 0042exact hm
  43. 0043exact hn
  44. 0044exact hcop
  45. 0045cases hw
  46. 0046cases hw_witness
  47. 0047specialize jordan_crt_tuple_extend (m)
  48. 0048specialize jordan_crt_tuple_extend (n)
  49. 0049specialize jordan_crt_tuple_extend (b)
  50. 0050specialize jordan_crt_tuple_extend (c)
  51. 0051specialize jordan_crt_tuple_extend (d)
  52. 0052specialize jordan_crt_tuple_extend (e)
  53. 0053specialize jordan_crt_tuple_extend (x)
  54. 0054specialize jordan_crt_tuple_extend (x1)
  55. 0055specialize jordan_crt_tuple_extend (k)
  56. 0056specialize jordan_crt_tuple_extend (x2)
  57. 0057specialize jordan_crt_tuple_extend (x3)
  58. 0058specialize jordan_crt_tuple_extend (x4)
  59. 0059apply jordan_crt_tuple_extend
  60. 0060exact IH_witness_witness
  61. 0061exact ha_witness
  62. 0062exact hz_witness
  63. 0063exact hw_witness_left
  64. 0064exact hw_witness_right