JT002C

jordan_crt_tuple_exists

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

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. ¬m = 0 → ¬n = 0 → Coprime(m,n) → ∀ x. ∃ y. ∃ z. JordanTupleCRT(m,n,b,c,d,e,y,z,x)

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

Definition DAG

JordanTupleCRT(m,n,b,c,d,e,f,g,k) · 1Coprime(a,b) · 1ModEq(m,a,b) · 2BetaAt(b,c,i,x) · 2

Actual proof prerequisites

jordan_crt_tuple_emptybeta_at_exists · checked external prerequisitebinary_crt · checked external prerequisitejordan_crt_tuple_extend
Original expanded first-order 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))))))))

Complete tactic proof in conservative notation

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

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 : ∃ a. BetaAt(b,c,k,a)Definitions: BetaAt(b,c,k,a)Original native command in the exact edition
  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 : ∃ z. BetaAt(d,e,k,z)Definitions: BetaAt(d,e,k,z)Original native command in the exact edition
  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 : ∃ w. ModEq(m,w,x2) ∧ ModEq(n,w,x3)Definitions: ModEq(m,w,x2)ModEq(n,w,x3)Original native command in the exact edition
  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 defined 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 : ∃ a. BetaAt(b,c,k,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 : ∃ z. BetaAt(d,e,k,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 : ∃ w. ModEq(m,w,x2) ∧ ModEq(n,w,x3)
  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