JT002B

jordan_crt_tuple_extend

Append one genuine scalar CRT solution using an actual beta prefix extension.

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. ∀ f. ∀ g. ∀ k. ∀ a. ∀ z. ∀ w. JordanTupleCRT(m,n,b,c,d,e,f,g,k) → BetaAt(b,c,k,a) → BetaAt(d,e,k,z) → ModEq(m,w,a) → ModEq(n,w,z) → ∃ x. ∃ y. JordanTupleCRT(m,n,b,c,d,e,x,y,S k)

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

Definition DAG

BetaPrefixEqual(b,c,d,e,l) · 1JordanTupleCRT(m,n,b,c,d,e,f,g,k) · 2Lt(a,b) · 1ModEq(m,a,b) · 4BetaAt(b,c,i,x) · 6

Actual proof prerequisites

beta_prefix_extend · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisite
Original expanded first-order statement 
forall m n b c d e f g k a z w. (forall jt_index_crtprefix. (exists jt_gap_crtprefixindex. jt_gap_crtprefixindex+S (jt_index_crtprefix)=(k)) -> exists jt_left_crtprefix jt_right_crtprefix jt_output_crtprefix. ((((exists fs_h_jt_crtprefixleft. fs_h_jt_crtprefixleft + S (jt_left_crtprefix) = S ((S (jt_index_crtprefix)) * c)) /\ exists fs_q_jt_crtprefixleft. b = fs_q_jt_crtprefixleft * S ((S (jt_index_crtprefix)) * c) + (jt_left_crtprefix))) /\ (((((exists fs_h_jt_crtprefixright. fs_h_jt_crtprefixright + S (jt_right_crtprefix) = S ((S (jt_index_crtprefix)) * e)) /\ exists fs_q_jt_crtprefixright. d = fs_q_jt_crtprefixright * S ((S (jt_index_crtprefix)) * e) + (jt_right_crtprefix))) /\ (((((exists fs_h_jt_crtprefixoutput. fs_h_jt_crtprefixoutput + S (jt_output_crtprefix) = S ((S (jt_index_crtprefix)) * g)) /\ exists fs_q_jt_crtprefixoutput. f = fs_q_jt_crtprefixoutput * S ((S (jt_index_crtprefix)) * g) + (jt_output_crtprefix))) /\ (((exists jt_left_crtprefixmodleft jt_right_crtprefixmodleft. (jt_output_crtprefix)+(m)*jt_left_crtprefixmodleft=(jt_left_crtprefix)+(m)*jt_right_crtprefixmodleft) /\ (exists jt_left_crtprefixmodright jt_right_crtprefixmodright. (jt_output_crtprefix)+(n)*jt_left_crtprefixmodright=(jt_right_crtprefix)+(n)*jt_right_crtprefixmodright))))))))) -> (((exists fs_h_jt_crtlastleft. fs_h_jt_crtlastleft + S (a) = S ((S (k)) * c)) /\ exists fs_q_jt_crtlastleft. b = fs_q_jt_crtlastleft * S ((S (k)) * c) + (a))) -> (((exists fs_h_jt_crtlastright. fs_h_jt_crtlastright + S (z) = S ((S (k)) * e)) /\ exists fs_q_jt_crtlastright. d = fs_q_jt_crtlastright * S ((S (k)) * e) + (z))) -> (exists jt_left_crtlastmodleft jt_right_crtlastmodleft. (w)+(m)*jt_left_crtlastmodleft=(a)+(m)*jt_right_crtlastmodleft) -> (exists jt_left_crtlastmodright jt_right_crtlastmodright. (w)+(n)*jt_left_crtlastmodright=(z)+(n)*jt_right_crtlastmodright) -> exists u v. forall jt_index_crtextended. (exists jt_gap_crtextendedindex. jt_gap_crtextendedindex+S (jt_index_crtextended)=(S k)) -> exists jt_left_crtextended jt_right_crtextended jt_output_crtextended. ((((exists fs_h_jt_crtextendedleft. fs_h_jt_crtextendedleft + S (jt_left_crtextended) = S ((S (jt_index_crtextended)) * c)) /\ exists fs_q_jt_crtextendedleft. b = fs_q_jt_crtextendedleft * S ((S (jt_index_crtextended)) * c) + (jt_left_crtextended))) /\ (((((exists fs_h_jt_crtextendedright. fs_h_jt_crtextendedright + S (jt_right_crtextended) = S ((S (jt_index_crtextended)) * e)) /\ exists fs_q_jt_crtextendedright. d = fs_q_jt_crtextendedright * S ((S (jt_index_crtextended)) * e) + (jt_right_crtextended))) /\ (((((exists fs_h_jt_crtextendedoutput. fs_h_jt_crtextendedoutput + S (jt_output_crtextended) = S ((S (jt_index_crtextended)) * v)) /\ exists fs_q_jt_crtextendedoutput. u = fs_q_jt_crtextendedoutput * S ((S (jt_index_crtextended)) * v) + (jt_output_crtextended))) /\ (((exists jt_left_crtextendedmodleft jt_right_crtextendedmodleft. (jt_output_crtextended)+(m)*jt_left_crtextendedmodleft=(jt_left_crtextended)+(m)*jt_right_crtextendedmodleft) /\ (exists jt_left_crtextendedmodright jt_right_crtextendedmodright. (jt_output_crtextended)+(n)*jt_left_crtextendedmodright=(jt_right_crtextended)+(n)*jt_right_crtextendedmodright))))))))

Complete tactic proof in conservative notation

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

81 script commands · 31 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.

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 a
02Fix variables and assumptionsL11–17

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

  1. L11
    intro z
  2. L12
    intro w
  3. L13
    intro hprefix
  4. L14
    intro ha
  5. L15
    intro hz
  6. L16
    intro hm
  7. L17
    intro hn
03Establish hextL18–23

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

  1. L18
    have hext : ∃ u. ∃ v. BetaAt(u,v,k,w) ∧ BetaPrefixEqual(f,g,u,v,k)Definitions: BetaAt(u,v,k,w)BetaPrefixEqual(f,g,u,v,k)Original native command in the exact edition
  2. L19
    specialize beta_prefix_extend (k)
  3. L20
    specialize beta_prefix_extend (f)
  4. L21
    specialize beta_prefix_extend (g)
  5. L22
    specialize beta_prefix_extend (w)
  6. L23
    apply beta_prefix_extend
04Separate the logical casesL24–26

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

  1. L24
    cases hext
  2. L25
    cases hext_witness
  3. L26
    cases hext_witness_witness
05Construct an explicit witnessL27–28

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

  1. L27
    exists x
  2. L28
    exists x1
06Fix variables and assumptionsL29–30

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

  1. L29
    intro i
  2. L30
    intro hi
07Establish hcL31–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L31
    have hc : i = k ∨ Lt(i,k)Definitions: Lt(i,k)Original native command in the exact edition
  2. L32
    specialize finite_lt_succ_eq_or_lt (k)
  3. L33
    specialize finite_lt_succ_eq_or_lt (i)
  4. L34
    apply finite_lt_succ_eq_or_lt
  5. L35
    exact hi
08Separate the logical casesL36–36

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

  1. L36
    cases hc
09Construct an explicit witnessL37–39

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

  1. L37
    exists a
  2. L38
    exists z
  3. L39
    exists w
10Separate the logical casesL40–40

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

  1. L40
    split
11Calculate and transport equalitiesL41–42

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

  1. L41
    rewrite hc_left
  2. L42
    rewrite hc_left
12Use earlier factsL43–43

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

  1. L43
    exact ha
13Separate the logical casesL44–44

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

  1. L44
    split
14Calculate and transport equalitiesL45–46

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

  1. L45
    rewrite hc_left
  2. L46
    rewrite hc_left
15Use earlier factsL47–47

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

  1. L47
    exact hz
16Separate the logical casesL48–48

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

  1. L48
    split
17Calculate and transport equalitiesL49–50

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

  1. L49
    rewrite hc_left
  2. L50
    rewrite hc_left
18Use earlier factsL51–51

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

  1. L51
    exact hext_witness_witness_left
19Separate the logical casesL52–52

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

  1. L52
    split
20Use earlier factsL53–54

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

  1. L53
    exact hm
  2. L54
    exact hn
21Establish hvalueL55–58

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

  1. L55
    have hvalue : ∃ a. ∃ z. ∃ w. BetaAt(b,c,i,a) ∧ (BetaAt(d,e,i,z) ∧ (BetaAt(f,g,i,w) ∧ (ModEq(m,w,a) ∧ ModEq(n,w,z))))Definitions: BetaAt(b,c,i,a)BetaAt(d,e,i,z)BetaAt(f,g,i,w)ModEq(m,w,a)ModEq(n,w,z)Original native command in the exact edition
  2. L56
    specialize hprefix (i)
  3. L57
    apply hprefix
  4. L58
    exact hc_right
22Separate the logical casesL59–65

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

  1. L59
    cases hvalue
  2. L60
    cases hvalue_witness
  3. L61
    cases hvalue_witness_witness
  4. L62
    cases hvalue_witness_witness_witness
  5. L63
    cases hvalue_witness_witness_witness_right
  6. L64
    cases hvalue_witness_witness_witness_right_right
  7. L65
    cases hvalue_witness_witness_witness_right_right_right
23Construct an explicit witnessL66–68

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

  1. L66
    exists x2
  2. L67
    exists x3
  3. L68
    exists x4
24Separate the logical casesL69–69

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

  1. L69
    split
25Use earlier factsL70–70

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

  1. L70
    exact hvalue_witness_witness_witness_left
26Separate the logical casesL71–71

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

  1. L71
    split
27Use earlier factsL72–72

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

  1. L72
    exact hvalue_witness_witness_witness_right_left
28Separate the logical casesL73–73

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

  1. L73
    split
29Use earlier factsL74–78

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

  1. L74
    specialize hext_witness_witness_right (i)
  2. L75
    specialize hext_witness_witness_right (x4)
  3. L76
    apply hext_witness_witness_right
  4. L77
    exact hc_right
  5. L78
    exact hvalue_witness_witness_witness_right_right_left
30Separate the logical casesL79–79

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

  1. L79
    split
31Use earlier factsL80–81

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

  1. L80
    exact hvalue_witness_witness_witness_right_right_right_left
  2. L81
    exact hvalue_witness_witness_witness_right_right_right_right

Library-wide reading audit

Original defined command ledger · 81 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 a
  11. 0011intro z
  12. 0012intro w
  13. 0013intro hprefix
  14. 0014intro ha
  15. 0015intro hz
  16. 0016intro hm
  17. 0017intro hn
  18. 0018have hext : ∃ u. ∃ v. BetaAt(u,v,k,w) ∧ BetaPrefixEqual(f,g,u,v,k)
  19. 0019specialize beta_prefix_extend (k)
  20. 0020specialize beta_prefix_extend (f)
  21. 0021specialize beta_prefix_extend (g)
  22. 0022specialize beta_prefix_extend (w)
  23. 0023apply beta_prefix_extend
  24. 0024cases hext
  25. 0025cases hext_witness
  26. 0026cases hext_witness_witness
  27. 0027exists x
  28. 0028exists x1
  29. 0029intro i
  30. 0030intro hi
  31. 0031have hc : i = k ∨ Lt(i,k)
  32. 0032specialize finite_lt_succ_eq_or_lt (k)
  33. 0033specialize finite_lt_succ_eq_or_lt (i)
  34. 0034apply finite_lt_succ_eq_or_lt
  35. 0035exact hi
  36. 0036cases hc
  37. 0037exists a
  38. 0038exists z
  39. 0039exists w
  40. 0040split
  41. 0041rewrite hc_left
  42. 0042rewrite hc_left
  43. 0043exact ha
  44. 0044split
  45. 0045rewrite hc_left
  46. 0046rewrite hc_left
  47. 0047exact hz
  48. 0048split
  49. 0049rewrite hc_left
  50. 0050rewrite hc_left
  51. 0051exact hext_witness_witness_left
  52. 0052split
  53. 0053exact hm
  54. 0054exact hn
  55. 0055have hvalue : ∃ a. ∃ z. ∃ w. BetaAt(b,c,i,a) ∧ (BetaAt(d,e,i,z) ∧ (BetaAt(f,g,i,w) ∧ (ModEq(m,w,a) ∧ ModEq(n,w,z))))
  56. 0056specialize hprefix (i)
  57. 0057apply hprefix
  58. 0058exact hc_right
  59. 0059cases hvalue
  60. 0060cases hvalue_witness
  61. 0061cases hvalue_witness_witness
  62. 0062cases hvalue_witness_witness_witness
  63. 0063cases hvalue_witness_witness_witness_right
  64. 0064cases hvalue_witness_witness_witness_right_right
  65. 0065cases hvalue_witness_witness_witness_right_right_right
  66. 0066exists x2
  67. 0067exists x3
  68. 0068exists x4
  69. 0069split
  70. 0070exact hvalue_witness_witness_witness_left
  71. 0071split
  72. 0072exact hvalue_witness_witness_witness_right_left
  73. 0073split
  74. 0074specialize hext_witness_witness_right (i)
  75. 0075specialize hext_witness_witness_right (x4)
  76. 0076apply hext_witness_witness_right
  77. 0077exact hc_right
  78. 0078exact hvalue_witness_witness_witness_right_right_left
  79. 0079split
  80. 0080exact hvalue_witness_witness_witness_right_right_right_left
  81. 0081exact hvalue_witness_witness_witness_right_right_right_right