CR0008

crt_prefix_solution_successor_intro

A solved predecessor prefix extends exactly when the actual last decoded congruence holds.

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Historical partial components only: this chapter proves canonical solutions for finite positive pairwise-coprime systems and exact LCM solution classes. G011 is now closed in the separate Alpha-v27 generalized-crt branch for arbitrary pairwise-compatible systems, including noncoprime moduli. Full G011 proof · Alpha v27

Exact theorem in conservative defined notation

∀ r. ∀ s. ∀ b. ∀ c. ∀ l. ∀ x. ∀ a. ∀ m. CRTPrefixSolution(r,s,b,c,l,x) → Beta(r,s,l,a) → Beta(b,c,l,m) → ModEq(m,x,a) → CRTPrefixSolution(r,s,b,c,S l,x)

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

Definition DAG

Beta(b,c,i,x) · 2CRTPrefixSolution(r,s,b,c,l,x) · 2ModEq(m,a,b) · 1

Actual proof prerequisites

finite_lt_succ_eq_or_lt · checked external prerequisitebeta_at_unique · checked external prerequisite
Original expanded first-order statement 
forall r s b c l x a m. (forall gcrt_solution_index_intro_prefix gcrt_solution_residue_intro_prefix gcrt_solution_modulus_intro_prefix. (exists ff_lt_gcrt_intro_prefix_bound. ff_lt_gcrt_intro_prefix_bound + S gcrt_solution_index_intro_prefix = l) -> (((exists ff_h_gcrt_intro_prefix_residue. ff_h_gcrt_intro_prefix_residue + S (gcrt_solution_residue_intro_prefix) = S ((S (gcrt_solution_index_intro_prefix)) * s)) /\ exists ff_q_gcrt_intro_prefix_residue. r = ff_q_gcrt_intro_prefix_residue * S ((S (gcrt_solution_index_intro_prefix)) * s) + (gcrt_solution_residue_intro_prefix))) -> (((exists ff_h_gcrt_intro_prefix_modulus. ff_h_gcrt_intro_prefix_modulus + S (gcrt_solution_modulus_intro_prefix) = S ((S (gcrt_solution_index_intro_prefix)) * c)) /\ exists ff_q_gcrt_intro_prefix_modulus. b = ff_q_gcrt_intro_prefix_modulus * S ((S (gcrt_solution_index_intro_prefix)) * c) + (gcrt_solution_modulus_intro_prefix))) -> (exists hgcrt_mod_left_gcrt_intro_prefix_congruence hgcrt_mod_right_gcrt_intro_prefix_congruence. x + gcrt_solution_modulus_intro_prefix * hgcrt_mod_left_gcrt_intro_prefix_congruence = gcrt_solution_residue_intro_prefix + gcrt_solution_modulus_intro_prefix * hgcrt_mod_right_gcrt_intro_prefix_congruence)) -> (((exists ff_h_gcrt_intro_last_residue. ff_h_gcrt_intro_last_residue + S (a) = S ((S (l)) * s)) /\ exists ff_q_gcrt_intro_last_residue. r = ff_q_gcrt_intro_last_residue * S ((S (l)) * s) + (a))) -> (((exists ff_h_gcrt_intro_last_modulus. ff_h_gcrt_intro_last_modulus + S (m) = S ((S (l)) * c)) /\ exists ff_q_gcrt_intro_last_modulus. b = ff_q_gcrt_intro_last_modulus * S ((S (l)) * c) + (m))) -> (exists hgcrt_mod_left_gcrt_intro_last_congruence hgcrt_mod_right_gcrt_intro_last_congruence. x + m * hgcrt_mod_left_gcrt_intro_last_congruence = a + m * hgcrt_mod_right_gcrt_intro_last_congruence) -> (forall gcrt_solution_index_intro_result gcrt_solution_residue_intro_result gcrt_solution_modulus_intro_result. (exists ff_lt_gcrt_intro_result_bound. ff_lt_gcrt_intro_result_bound + S gcrt_solution_index_intro_result = S l) -> (((exists ff_h_gcrt_intro_result_residue. ff_h_gcrt_intro_result_residue + S (gcrt_solution_residue_intro_result) = S ((S (gcrt_solution_index_intro_result)) * s)) /\ exists ff_q_gcrt_intro_result_residue. r = ff_q_gcrt_intro_result_residue * S ((S (gcrt_solution_index_intro_result)) * s) + (gcrt_solution_residue_intro_result))) -> (((exists ff_h_gcrt_intro_result_modulus. ff_h_gcrt_intro_result_modulus + S (gcrt_solution_modulus_intro_result) = S ((S (gcrt_solution_index_intro_result)) * c)) /\ exists ff_q_gcrt_intro_result_modulus. b = ff_q_gcrt_intro_result_modulus * S ((S (gcrt_solution_index_intro_result)) * c) + (gcrt_solution_modulus_intro_result))) -> (exists hgcrt_mod_left_gcrt_intro_result_congruence hgcrt_mod_right_gcrt_intro_result_congruence. x + gcrt_solution_modulus_intro_result * hgcrt_mod_left_gcrt_intro_result_congruence = gcrt_solution_residue_intro_result + gcrt_solution_modulus_intro_result * hgcrt_mod_right_gcrt_intro_result_congruence))

Complete unchanged native tactic proof

All 57 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

57 script commands · 9 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 r
  2. L2
    intro s
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro l
  6. L6
    intro x
  7. L7
    intro a
  8. L8
    intro m
  9. L9
    intro hprefix
  10. L10
    intro ha
02Fix variables and assumptionsL11–18

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

  1. L11
    intro hm
  2. L12
    intro hnew
  3. L13
    intro i
  4. L14
    intro q
  5. L15
    intro n
  6. L16
    intro hi
  7. L17
    intro hq
  8. L18
    intro hn
03Establish hsplitL19–23

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. L19
    have hsplit : i = l \/ exists gap. gap + S i = l
  2. L20
    specialize finite_lt_succ_eq_or_lt l
  3. L21
    specialize finite_lt_succ_eq_or_lt i
  4. L22
    apply finite_lt_succ_eq_or_lt
  5. L23
    exact hi
04Separate the logical casesL24–24

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

  1. L24
    cases hsplit
05Calculate and transport equalitiesL25–28

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

  1. L25
    rewrite hsplit_left at hq
  2. L26
    rewrite hsplit_left at hq
  3. L27
    rewrite hsplit_left at hn
  4. L28
    rewrite hsplit_left at hn
06Establish hresidueL29–37

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

  1. L29
    have hresidue : q = a
  2. L30
    specialize beta_at_unique r
  3. L31
    specialize beta_at_unique s
  4. L32
    specialize beta_at_unique l
  5. L33
    specialize beta_at_unique q
  6. L34
    specialize beta_at_unique a
  7. L35
    apply beta_at_unique
  8. L36
    exact hq
  9. L37
    exact ha
07Establish hmodulusL38–47

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

  1. L38
    have hmodulus : n = m
  2. L39
    specialize beta_at_unique b
  3. L40
    specialize beta_at_unique c
  4. L41
    specialize beta_at_unique l
  5. L42
    specialize beta_at_unique n
  6. L43
    specialize beta_at_unique m
  7. L44
    apply beta_at_unique
  8. L45
    exact hn
  9. L46
    exact hm
  10. L47
    rewrite hmodulus
08Calculate and transport equalitiesL48–49

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

  1. L48
    rewrite hmodulus
  2. L49
    rewrite hresidue
09Use earlier factsL50–57

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

  1. L50
    exact hnew
  2. L51
    specialize hprefix i
  3. L52
    specialize hprefix q
  4. L53
    specialize hprefix n
  5. L54
    apply hprefix
  6. L55
    exact hsplit_right
  7. L56
    exact hq
  8. L57
    exact hn

Library-wide reading audit

Original defined command ledger · 57 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro x
  7. 0007intro a
  8. 0008intro m
  9. 0009intro hprefix
  10. 0010intro ha
  11. 0011intro hm
  12. 0012intro hnew
  13. 0013intro i
  14. 0014intro q
  15. 0015intro n
  16. 0016intro hi
  17. 0017intro hq
  18. 0018intro hn
  19. 0019have hsplit : i = l \/ exists gap. gap + S i = l
  20. 0020specialize finite_lt_succ_eq_or_lt l
  21. 0021specialize finite_lt_succ_eq_or_lt i
  22. 0022apply finite_lt_succ_eq_or_lt
  23. 0023exact hi
  24. 0024cases hsplit
  25. 0025rewrite hsplit_left at hq
  26. 0026rewrite hsplit_left at hq
  27. 0027rewrite hsplit_left at hn
  28. 0028rewrite hsplit_left at hn
  29. 0029have hresidue : q = a
  30. 0030specialize beta_at_unique r
  31. 0031specialize beta_at_unique s
  32. 0032specialize beta_at_unique l
  33. 0033specialize beta_at_unique q
  34. 0034specialize beta_at_unique a
  35. 0035apply beta_at_unique
  36. 0036exact hq
  37. 0037exact ha
  38. 0038have hmodulus : n = m
  39. 0039specialize beta_at_unique b
  40. 0040specialize beta_at_unique c
  41. 0041specialize beta_at_unique l
  42. 0042specialize beta_at_unique n
  43. 0043specialize beta_at_unique m
  44. 0044apply beta_at_unique
  45. 0045exact hn
  46. 0046exact hm
  47. 0047rewrite hmodulus
  48. 0048rewrite hmodulus
  49. 0049rewrite hresidue
  50. 0050exact hnew
  51. 0051specialize hprefix i
  52. 0052specialize hprefix q
  53. 0053specialize hprefix n
  54. 0054apply hprefix
  55. 0055exact hsplit_right
  56. 0056exact hq
  57. 0057exact hn