CR0007

crt_prefix_solution_last

The last residue/modulus pair of a solved successor list satisfies its actual congruence.

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,S l,x) → Beta(r,s,l,a) → Beta(b,c,l,m) → ModEq(m,x,a)

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) · 1ModEq(m,a,b) · 1

Actual proof prerequisites

le_refl · checked external prerequisite
Original expanded first-order statement 
forall r s b c l x a m. (forall gcrt_solution_index_solution_last_source gcrt_solution_residue_solution_last_source gcrt_solution_modulus_solution_last_source. (exists ff_lt_gcrt_solution_last_source_bound. ff_lt_gcrt_solution_last_source_bound + S gcrt_solution_index_solution_last_source = S l) -> (((exists ff_h_gcrt_solution_last_source_residue. ff_h_gcrt_solution_last_source_residue + S (gcrt_solution_residue_solution_last_source) = S ((S (gcrt_solution_index_solution_last_source)) * s)) /\ exists ff_q_gcrt_solution_last_source_residue. r = ff_q_gcrt_solution_last_source_residue * S ((S (gcrt_solution_index_solution_last_source)) * s) + (gcrt_solution_residue_solution_last_source))) -> (((exists ff_h_gcrt_solution_last_source_modulus. ff_h_gcrt_solution_last_source_modulus + S (gcrt_solution_modulus_solution_last_source) = S ((S (gcrt_solution_index_solution_last_source)) * c)) /\ exists ff_q_gcrt_solution_last_source_modulus. b = ff_q_gcrt_solution_last_source_modulus * S ((S (gcrt_solution_index_solution_last_source)) * c) + (gcrt_solution_modulus_solution_last_source))) -> (exists hgcrt_mod_left_gcrt_solution_last_source_congruence hgcrt_mod_right_gcrt_solution_last_source_congruence. x + gcrt_solution_modulus_solution_last_source * hgcrt_mod_left_gcrt_solution_last_source_congruence = gcrt_solution_residue_solution_last_source + gcrt_solution_modulus_solution_last_source * hgcrt_mod_right_gcrt_solution_last_source_congruence)) -> (((exists ff_h_gcrt_solution_last_residue. ff_h_gcrt_solution_last_residue + S (a) = S ((S (l)) * s)) /\ exists ff_q_gcrt_solution_last_residue. r = ff_q_gcrt_solution_last_residue * S ((S (l)) * s) + (a))) -> (((exists ff_h_gcrt_solution_last_modulus. ff_h_gcrt_solution_last_modulus + S (m) = S ((S (l)) * c)) /\ exists ff_q_gcrt_solution_last_modulus. b = ff_q_gcrt_solution_last_modulus * S ((S (l)) * c) + (m))) -> (exists hgcrt_mod_left_gcrt_solution_last_result hgcrt_mod_right_gcrt_solution_last_result. x + m * hgcrt_mod_left_gcrt_solution_last_result = a + m * hgcrt_mod_right_gcrt_solution_last_result)

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

19 script commands · 3 reading checkpoints · 0 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 hsolution
  10. L10
    intro ha
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hm
03Use earlier factsL12–19

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

  1. L12
    specialize hsolution l
  2. L13
    specialize hsolution a
  3. L14
    specialize hsolution m
  4. L15
    apply hsolution
  5. L16
    specialize le_refl (S l)
  6. L17
    exact le_refl
  7. L18
    exact ha
  8. L19
    exact hm

Library-wide reading audit

Original defined command ledger · 19 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 hsolution
  10. 0010intro ha
  11. 0011intro hm
  12. 0012specialize hsolution l
  13. 0013specialize hsolution a
  14. 0014specialize hsolution m
  15. 0015apply hsolution
  16. 0016specialize le_refl (S l)
  17. 0017exact le_refl
  18. 0018exact ha
  19. 0019exact hm