FC0016

crt_normalized_prefix_solution_class_iff_lcm

All simultaneous solutions form exactly the congruence class of the normalized solution modulo the exact list LCM, also when that LCM is zero.

Alpha v34 checked-use · first admitted v27 · 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.

All finite lists are included, even the empty list and zero moduli. A positive LCM gives x<M; at zero LCM congruence is exact equality and normalization deliberately does not require the impossible x<0.

Exact theorem in conservative defined notation

∀ r. ∀ s. ∀ b. ∀ c. ∀ l. ∀ M. ∀ x. ∀ y. CRTNormalizedPrefixSolution(r,s,b,c,l,x,M) → (CRTPrefixSolution(r,s,b,c,l,y) → ModEq(M,y,x)) ∧ (ModEq(M,y,x) → CRTPrefixSolution(r,s,b,c,l,y))

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

Definition DAG

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

Actual proof prerequisites

crt_prefix_solution_class_iff_lcm · checked external prerequisite
Original expanded first-order statement 
forall r s b c l M x y. (((((forall gcrt_common_index_gfull_normalized_class_source_lcm_own gcrt_common_modulus_gfull_normalized_class_source_lcm_own. (exists ff_lt_gcrt_gfull_normalized_class_source_lcm_own_bound. ff_lt_gcrt_gfull_normalized_class_source_lcm_own_bound + S gcrt_common_index_gfull_normalized_class_source_lcm_own = l) -> (((exists ff_h_gcrt_gfull_normalized_class_source_lcm_own_entry. ff_h_gcrt_gfull_normalized_class_source_lcm_own_entry + S (gcrt_common_modulus_gfull_normalized_class_source_lcm_own) = S ((S (gcrt_common_index_gfull_normalized_class_source_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_normalized_class_source_lcm_own_entry. b = ff_q_gcrt_gfull_normalized_class_source_lcm_own_entry * S ((S (gcrt_common_index_gfull_normalized_class_source_lcm_own)) * c) + (gcrt_common_modulus_gfull_normalized_class_source_lcm_own))) -> exists gcrt_common_quotient_gfull_normalized_class_source_lcm_own. M = gcrt_common_modulus_gfull_normalized_class_source_lcm_own * gcrt_common_quotient_gfull_normalized_class_source_lcm_own) /\ forall gcrt_lcm_common_gfull_normalized_class_source_lcm. (forall gcrt_common_index_gfull_normalized_class_source_lcm_other gcrt_common_modulus_gfull_normalized_class_source_lcm_other. (exists ff_lt_gcrt_gfull_normalized_class_source_lcm_other_bound. ff_lt_gcrt_gfull_normalized_class_source_lcm_other_bound + S gcrt_common_index_gfull_normalized_class_source_lcm_other = l) -> (((exists ff_h_gcrt_gfull_normalized_class_source_lcm_other_entry. ff_h_gcrt_gfull_normalized_class_source_lcm_other_entry + S (gcrt_common_modulus_gfull_normalized_class_source_lcm_other) = S ((S (gcrt_common_index_gfull_normalized_class_source_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_normalized_class_source_lcm_other_entry. b = ff_q_gcrt_gfull_normalized_class_source_lcm_other_entry * S ((S (gcrt_common_index_gfull_normalized_class_source_lcm_other)) * c) + (gcrt_common_modulus_gfull_normalized_class_source_lcm_other))) -> exists gcrt_common_quotient_gfull_normalized_class_source_lcm_other. gcrt_lcm_common_gfull_normalized_class_source_lcm = gcrt_common_modulus_gfull_normalized_class_source_lcm_other * gcrt_common_quotient_gfull_normalized_class_source_lcm_other) -> exists gcrt_lcm_quotient_gfull_normalized_class_source_lcm. gcrt_lcm_common_gfull_normalized_class_source_lcm = M * gcrt_lcm_quotient_gfull_normalized_class_source_lcm)) /\ ((M = 0 \/ (exists ff_lt_gcrt_gfull_normalized_class_source_bound. ff_lt_gcrt_gfull_normalized_class_source_bound + S x = M)) /\ (forall gcrt_solution_index_gfull_normalized_class_source_solution gcrt_solution_residue_gfull_normalized_class_source_solution gcrt_solution_modulus_gfull_normalized_class_source_solution. (exists ff_lt_gcrt_gfull_normalized_class_source_solution_bound. ff_lt_gcrt_gfull_normalized_class_source_solution_bound + S gcrt_solution_index_gfull_normalized_class_source_solution = l) -> (((exists ff_h_gcrt_gfull_normalized_class_source_solution_residue. ff_h_gcrt_gfull_normalized_class_source_solution_residue + S (gcrt_solution_residue_gfull_normalized_class_source_solution) = S ((S (gcrt_solution_index_gfull_normalized_class_source_solution)) * s)) /\ exists ff_q_gcrt_gfull_normalized_class_source_solution_residue. r = ff_q_gcrt_gfull_normalized_class_source_solution_residue * S ((S (gcrt_solution_index_gfull_normalized_class_source_solution)) * s) + (gcrt_solution_residue_gfull_normalized_class_source_solution))) -> (((exists ff_h_gcrt_gfull_normalized_class_source_solution_modulus. ff_h_gcrt_gfull_normalized_class_source_solution_modulus + S (gcrt_solution_modulus_gfull_normalized_class_source_solution) = S ((S (gcrt_solution_index_gfull_normalized_class_source_solution)) * c)) /\ exists ff_q_gcrt_gfull_normalized_class_source_solution_modulus. b = ff_q_gcrt_gfull_normalized_class_source_solution_modulus * S ((S (gcrt_solution_index_gfull_normalized_class_source_solution)) * c) + (gcrt_solution_modulus_gfull_normalized_class_source_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_normalized_class_source_solution_congruence hgcrt_mod_right_gcrt_gfull_normalized_class_source_solution_congruence. x + gcrt_solution_modulus_gfull_normalized_class_source_solution * hgcrt_mod_left_gcrt_gfull_normalized_class_source_solution_congruence = gcrt_solution_residue_gfull_normalized_class_source_solution + gcrt_solution_modulus_gfull_normalized_class_source_solution * hgcrt_mod_right_gcrt_gfull_normalized_class_source_solution_congruence))))) -> (((forall gcrt_solution_index_gfull_normalized_class_solution_forward gcrt_solution_residue_gfull_normalized_class_solution_forward gcrt_solution_modulus_gfull_normalized_class_solution_forward. (exists ff_lt_gcrt_gfull_normalized_class_solution_forward_bound. ff_lt_gcrt_gfull_normalized_class_solution_forward_bound + S gcrt_solution_index_gfull_normalized_class_solution_forward = l) -> (((exists ff_h_gcrt_gfull_normalized_class_solution_forward_residue. ff_h_gcrt_gfull_normalized_class_solution_forward_residue + S (gcrt_solution_residue_gfull_normalized_class_solution_forward) = S ((S (gcrt_solution_index_gfull_normalized_class_solution_forward)) * s)) /\ exists ff_q_gcrt_gfull_normalized_class_solution_forward_residue. r = ff_q_gcrt_gfull_normalized_class_solution_forward_residue * S ((S (gcrt_solution_index_gfull_normalized_class_solution_forward)) * s) + (gcrt_solution_residue_gfull_normalized_class_solution_forward))) -> (((exists ff_h_gcrt_gfull_normalized_class_solution_forward_modulus. ff_h_gcrt_gfull_normalized_class_solution_forward_modulus + S (gcrt_solution_modulus_gfull_normalized_class_solution_forward) = S ((S (gcrt_solution_index_gfull_normalized_class_solution_forward)) * c)) /\ exists ff_q_gcrt_gfull_normalized_class_solution_forward_modulus. b = ff_q_gcrt_gfull_normalized_class_solution_forward_modulus * S ((S (gcrt_solution_index_gfull_normalized_class_solution_forward)) * c) + (gcrt_solution_modulus_gfull_normalized_class_solution_forward))) -> (exists hgcrt_mod_left_gcrt_gfull_normalized_class_solution_forward_congruence hgcrt_mod_right_gcrt_gfull_normalized_class_solution_forward_congruence. y + gcrt_solution_modulus_gfull_normalized_class_solution_forward * hgcrt_mod_left_gcrt_gfull_normalized_class_solution_forward_congruence = gcrt_solution_residue_gfull_normalized_class_solution_forward + gcrt_solution_modulus_gfull_normalized_class_solution_forward * hgcrt_mod_right_gcrt_gfull_normalized_class_solution_forward_congruence)) -> (exists hgcrt_mod_left_gfull_normalized_class_mod_forward hgcrt_mod_right_gfull_normalized_class_mod_forward. y + M * hgcrt_mod_left_gfull_normalized_class_mod_forward = x + M * hgcrt_mod_right_gfull_normalized_class_mod_forward)) /\ ((exists hgcrt_mod_left_gfull_normalized_class_mod_backward hgcrt_mod_right_gfull_normalized_class_mod_backward. y + M * hgcrt_mod_left_gfull_normalized_class_mod_backward = x + M * hgcrt_mod_right_gfull_normalized_class_mod_backward) -> (forall gcrt_solution_index_gfull_normalized_class_solution_backward gcrt_solution_residue_gfull_normalized_class_solution_backward gcrt_solution_modulus_gfull_normalized_class_solution_backward. (exists ff_lt_gcrt_gfull_normalized_class_solution_backward_bound. ff_lt_gcrt_gfull_normalized_class_solution_backward_bound + S gcrt_solution_index_gfull_normalized_class_solution_backward = l) -> (((exists ff_h_gcrt_gfull_normalized_class_solution_backward_residue. ff_h_gcrt_gfull_normalized_class_solution_backward_residue + S (gcrt_solution_residue_gfull_normalized_class_solution_backward) = S ((S (gcrt_solution_index_gfull_normalized_class_solution_backward)) * s)) /\ exists ff_q_gcrt_gfull_normalized_class_solution_backward_residue. r = ff_q_gcrt_gfull_normalized_class_solution_backward_residue * S ((S (gcrt_solution_index_gfull_normalized_class_solution_backward)) * s) + (gcrt_solution_residue_gfull_normalized_class_solution_backward))) -> (((exists ff_h_gcrt_gfull_normalized_class_solution_backward_modulus. ff_h_gcrt_gfull_normalized_class_solution_backward_modulus + S (gcrt_solution_modulus_gfull_normalized_class_solution_backward) = S ((S (gcrt_solution_index_gfull_normalized_class_solution_backward)) * c)) /\ exists ff_q_gcrt_gfull_normalized_class_solution_backward_modulus. b = ff_q_gcrt_gfull_normalized_class_solution_backward_modulus * S ((S (gcrt_solution_index_gfull_normalized_class_solution_backward)) * c) + (gcrt_solution_modulus_gfull_normalized_class_solution_backward))) -> (exists hgcrt_mod_left_gcrt_gfull_normalized_class_solution_backward_congruence hgcrt_mod_right_gcrt_gfull_normalized_class_solution_backward_congruence. y + gcrt_solution_modulus_gfull_normalized_class_solution_backward * hgcrt_mod_left_gcrt_gfull_normalized_class_solution_backward_congruence = gcrt_solution_residue_gfull_normalized_class_solution_backward + gcrt_solution_modulus_gfull_normalized_class_solution_backward * hgcrt_mod_right_gcrt_gfull_normalized_class_solution_backward_congruence))))

Complete tactic proof in conservative notation

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

22 script commands · 4 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–9

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 M
  7. L7
    intro x
  8. L8
    intro y
  9. L9
    intro hx
02Separate the logical casesL10–11

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

  1. L10
    cases hx
  2. L11
    cases hx_right
03Use earlier factsL12–21

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

  1. L12
    specialize crt_prefix_solution_class_iff_lcm r
  2. L13
    specialize crt_prefix_solution_class_iff_lcm s
  3. L14
    specialize crt_prefix_solution_class_iff_lcm b
  4. L15
    specialize crt_prefix_solution_class_iff_lcm c
  5. L16
    specialize crt_prefix_solution_class_iff_lcm l
  6. L17
    specialize crt_prefix_solution_class_iff_lcm M
  7. L18
    specialize crt_prefix_solution_class_iff_lcm x
  8. L19
    specialize crt_prefix_solution_class_iff_lcm y
  9. L20
    apply crt_prefix_solution_class_iff_lcm
  10. L21
    exact hx_left
04Use earlier factsL22–22

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

  1. L22
    exact hx_right_right

Library-wide reading audit

Original defined command ledger · 22 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro M
  7. 0007intro x
  8. 0008intro y
  9. 0009intro hx
  10. 0010cases hx
  11. 0011cases hx_right
  12. 0012specialize crt_prefix_solution_class_iff_lcm r
  13. 0013specialize crt_prefix_solution_class_iff_lcm s
  14. 0014specialize crt_prefix_solution_class_iff_lcm b
  15. 0015specialize crt_prefix_solution_class_iff_lcm c
  16. 0016specialize crt_prefix_solution_class_iff_lcm l
  17. 0017specialize crt_prefix_solution_class_iff_lcm M
  18. 0018specialize crt_prefix_solution_class_iff_lcm x
  19. 0019specialize crt_prefix_solution_class_iff_lcm y
  20. 0020apply crt_prefix_solution_class_iff_lcm
  21. 0021exact hx_left
  22. 0022exact hx_right_right