JT002B

jordan_crt_tuple_extend

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

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

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

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

beta_prefix_extend Alpha theorem; checked-use authorized finite_lt_succ_eq_or_lt Alpha theorem; checked-use authorized

Direct dependents

JT002C jordan_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

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.

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 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: BetaPrefixEqualBetaAt
  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 \/ (exists jt_gap_crtextendcase. jt_gap_crtextendcase+S (i)=(k))
  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: ModEqBetaAt
  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 exact 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 : exists u v. ((((exists fs_h_jt_crtextendlast. fs_h_jt_crtextendlast + S (w) = S ((S (k)) * v)) /\ exists fs_q_jt_crtextendlast. u = fs_q_jt_crtextendlast * S ((S (k)) * v) + (w))) /\ (forall jt_index_crtextendprefix jt_value_crtextendprefix. (exists jt_gap_crtextendprefixindex. jt_gap_crtextendprefixindex+S (jt_index_crtextendprefix)=(k)) -> (((exists fs_h_jt_crtextendprefixold. fs_h_jt_crtextendprefixold + S (jt_value_crtextendprefix) = S ((S (jt_index_crtextendprefix)) * g)) /\ exists fs_q_jt_crtextendprefixold. f = fs_q_jt_crtextendprefixold * S ((S (jt_index_crtextendprefix)) * g) + (jt_value_crtextendprefix))) -> (((exists fs_h_jt_crtextendprefixnew. fs_h_jt_crtextendprefixnew + S (jt_value_crtextendprefix) = S ((S (jt_index_crtextendprefix)) * v)) /\ exists fs_q_jt_crtextendprefixnew. u = fs_q_jt_crtextendprefixnew * S ((S (jt_index_crtextendprefix)) * v) + (jt_value_crtextendprefix)))))
  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 \/ (exists jt_gap_crtextendcase. jt_gap_crtextendcase+S (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 : exists a z w. ((((exists fs_h_jt_crtoldleft. fs_h_jt_crtoldleft + S (a) = S ((S (i)) * c)) /\ exists fs_q_jt_crtoldleft. b = fs_q_jt_crtoldleft * S ((S (i)) * c) + (a))) /\ (((((exists fs_h_jt_crtoldright. fs_h_jt_crtoldright + S (z) = S ((S (i)) * e)) /\ exists fs_q_jt_crtoldright. d = fs_q_jt_crtoldright * S ((S (i)) * e) + (z))) /\ (((((exists fs_h_jt_crtoldoutput. fs_h_jt_crtoldoutput + S (w) = S ((S (i)) * g)) /\ exists fs_q_jt_crtoldoutput. f = fs_q_jt_crtoldoutput * S ((S (i)) * g) + (w))) /\ (((exists jt_left_crtoldmodleft jt_right_crtoldmodleft. (w)+(m)*jt_left_crtoldmodleft=(a)+(m)*jt_right_crtoldmodleft) /\ (exists jt_left_crtoldmodright jt_right_crtoldmodright. (w)+(n)*jt_left_crtoldmodright=(z)+(n)*jt_right_crtoldmodright))))))))
  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