FC0012

crt_prefix_solution_normalized_exists

Every simultaneous solution has a normalized representative for its exact list LCM, with zero retained rather than divided by.

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. CRTPrefixLCM(b,c,l,M) → CRTPrefixSolution(r,s,b,c,l,x) → ∃ y. CRTNormalizedPrefixSolution(r,s,b,c,l,y,M)

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

Definition DAG

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

Actual proof prerequisites

eq_decidable · checked external prerequisitecrt_prefix_solution_canonical_remainder · checked external prerequisitecrt_canonical_prefix_solution_implies_normalized
Original expanded first-order statement 
forall r s b c l M x. (((forall gcrt_common_index_gfull_normalize_lcm_own gcrt_common_modulus_gfull_normalize_lcm_own. (exists ff_lt_gcrt_gfull_normalize_lcm_own_bound. ff_lt_gcrt_gfull_normalize_lcm_own_bound + S gcrt_common_index_gfull_normalize_lcm_own = l) -> (((exists ff_h_gcrt_gfull_normalize_lcm_own_entry. ff_h_gcrt_gfull_normalize_lcm_own_entry + S (gcrt_common_modulus_gfull_normalize_lcm_own) = S ((S (gcrt_common_index_gfull_normalize_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_normalize_lcm_own_entry. b = ff_q_gcrt_gfull_normalize_lcm_own_entry * S ((S (gcrt_common_index_gfull_normalize_lcm_own)) * c) + (gcrt_common_modulus_gfull_normalize_lcm_own))) -> exists gcrt_common_quotient_gfull_normalize_lcm_own. M = gcrt_common_modulus_gfull_normalize_lcm_own * gcrt_common_quotient_gfull_normalize_lcm_own) /\ forall gcrt_lcm_common_gfull_normalize_lcm. (forall gcrt_common_index_gfull_normalize_lcm_other gcrt_common_modulus_gfull_normalize_lcm_other. (exists ff_lt_gcrt_gfull_normalize_lcm_other_bound. ff_lt_gcrt_gfull_normalize_lcm_other_bound + S gcrt_common_index_gfull_normalize_lcm_other = l) -> (((exists ff_h_gcrt_gfull_normalize_lcm_other_entry. ff_h_gcrt_gfull_normalize_lcm_other_entry + S (gcrt_common_modulus_gfull_normalize_lcm_other) = S ((S (gcrt_common_index_gfull_normalize_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_normalize_lcm_other_entry. b = ff_q_gcrt_gfull_normalize_lcm_other_entry * S ((S (gcrt_common_index_gfull_normalize_lcm_other)) * c) + (gcrt_common_modulus_gfull_normalize_lcm_other))) -> exists gcrt_common_quotient_gfull_normalize_lcm_other. gcrt_lcm_common_gfull_normalize_lcm = gcrt_common_modulus_gfull_normalize_lcm_other * gcrt_common_quotient_gfull_normalize_lcm_other) -> exists gcrt_lcm_quotient_gfull_normalize_lcm. gcrt_lcm_common_gfull_normalize_lcm = M * gcrt_lcm_quotient_gfull_normalize_lcm)) -> (forall gcrt_solution_index_gfull_normalize_solution gcrt_solution_residue_gfull_normalize_solution gcrt_solution_modulus_gfull_normalize_solution. (exists ff_lt_gcrt_gfull_normalize_solution_bound. ff_lt_gcrt_gfull_normalize_solution_bound + S gcrt_solution_index_gfull_normalize_solution = l) -> (((exists ff_h_gcrt_gfull_normalize_solution_residue. ff_h_gcrt_gfull_normalize_solution_residue + S (gcrt_solution_residue_gfull_normalize_solution) = S ((S (gcrt_solution_index_gfull_normalize_solution)) * s)) /\ exists ff_q_gcrt_gfull_normalize_solution_residue. r = ff_q_gcrt_gfull_normalize_solution_residue * S ((S (gcrt_solution_index_gfull_normalize_solution)) * s) + (gcrt_solution_residue_gfull_normalize_solution))) -> (((exists ff_h_gcrt_gfull_normalize_solution_modulus. ff_h_gcrt_gfull_normalize_solution_modulus + S (gcrt_solution_modulus_gfull_normalize_solution) = S ((S (gcrt_solution_index_gfull_normalize_solution)) * c)) /\ exists ff_q_gcrt_gfull_normalize_solution_modulus. b = ff_q_gcrt_gfull_normalize_solution_modulus * S ((S (gcrt_solution_index_gfull_normalize_solution)) * c) + (gcrt_solution_modulus_gfull_normalize_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_normalize_solution_congruence hgcrt_mod_right_gcrt_gfull_normalize_solution_congruence. x + gcrt_solution_modulus_gfull_normalize_solution * hgcrt_mod_left_gcrt_gfull_normalize_solution_congruence = gcrt_solution_residue_gfull_normalize_solution + gcrt_solution_modulus_gfull_normalize_solution * hgcrt_mod_right_gcrt_gfull_normalize_solution_congruence)) -> exists z. (((((forall gcrt_common_index_gfull_normalize_result_lcm_own gcrt_common_modulus_gfull_normalize_result_lcm_own. (exists ff_lt_gcrt_gfull_normalize_result_lcm_own_bound. ff_lt_gcrt_gfull_normalize_result_lcm_own_bound + S gcrt_common_index_gfull_normalize_result_lcm_own = l) -> (((exists ff_h_gcrt_gfull_normalize_result_lcm_own_entry. ff_h_gcrt_gfull_normalize_result_lcm_own_entry + S (gcrt_common_modulus_gfull_normalize_result_lcm_own) = S ((S (gcrt_common_index_gfull_normalize_result_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_normalize_result_lcm_own_entry. b = ff_q_gcrt_gfull_normalize_result_lcm_own_entry * S ((S (gcrt_common_index_gfull_normalize_result_lcm_own)) * c) + (gcrt_common_modulus_gfull_normalize_result_lcm_own))) -> exists gcrt_common_quotient_gfull_normalize_result_lcm_own. M = gcrt_common_modulus_gfull_normalize_result_lcm_own * gcrt_common_quotient_gfull_normalize_result_lcm_own) /\ forall gcrt_lcm_common_gfull_normalize_result_lcm. (forall gcrt_common_index_gfull_normalize_result_lcm_other gcrt_common_modulus_gfull_normalize_result_lcm_other. (exists ff_lt_gcrt_gfull_normalize_result_lcm_other_bound. ff_lt_gcrt_gfull_normalize_result_lcm_other_bound + S gcrt_common_index_gfull_normalize_result_lcm_other = l) -> (((exists ff_h_gcrt_gfull_normalize_result_lcm_other_entry. ff_h_gcrt_gfull_normalize_result_lcm_other_entry + S (gcrt_common_modulus_gfull_normalize_result_lcm_other) = S ((S (gcrt_common_index_gfull_normalize_result_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_normalize_result_lcm_other_entry. b = ff_q_gcrt_gfull_normalize_result_lcm_other_entry * S ((S (gcrt_common_index_gfull_normalize_result_lcm_other)) * c) + (gcrt_common_modulus_gfull_normalize_result_lcm_other))) -> exists gcrt_common_quotient_gfull_normalize_result_lcm_other. gcrt_lcm_common_gfull_normalize_result_lcm = gcrt_common_modulus_gfull_normalize_result_lcm_other * gcrt_common_quotient_gfull_normalize_result_lcm_other) -> exists gcrt_lcm_quotient_gfull_normalize_result_lcm. gcrt_lcm_common_gfull_normalize_result_lcm = M * gcrt_lcm_quotient_gfull_normalize_result_lcm)) /\ ((M = 0 \/ (exists ff_lt_gcrt_gfull_normalize_result_bound. ff_lt_gcrt_gfull_normalize_result_bound + S z = M)) /\ (forall gcrt_solution_index_gfull_normalize_result_solution gcrt_solution_residue_gfull_normalize_result_solution gcrt_solution_modulus_gfull_normalize_result_solution. (exists ff_lt_gcrt_gfull_normalize_result_solution_bound. ff_lt_gcrt_gfull_normalize_result_solution_bound + S gcrt_solution_index_gfull_normalize_result_solution = l) -> (((exists ff_h_gcrt_gfull_normalize_result_solution_residue. ff_h_gcrt_gfull_normalize_result_solution_residue + S (gcrt_solution_residue_gfull_normalize_result_solution) = S ((S (gcrt_solution_index_gfull_normalize_result_solution)) * s)) /\ exists ff_q_gcrt_gfull_normalize_result_solution_residue. r = ff_q_gcrt_gfull_normalize_result_solution_residue * S ((S (gcrt_solution_index_gfull_normalize_result_solution)) * s) + (gcrt_solution_residue_gfull_normalize_result_solution))) -> (((exists ff_h_gcrt_gfull_normalize_result_solution_modulus. ff_h_gcrt_gfull_normalize_result_solution_modulus + S (gcrt_solution_modulus_gfull_normalize_result_solution) = S ((S (gcrt_solution_index_gfull_normalize_result_solution)) * c)) /\ exists ff_q_gcrt_gfull_normalize_result_solution_modulus. b = ff_q_gcrt_gfull_normalize_result_solution_modulus * S ((S (gcrt_solution_index_gfull_normalize_result_solution)) * c) + (gcrt_solution_modulus_gfull_normalize_result_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_normalize_result_solution_congruence hgcrt_mod_right_gcrt_gfull_normalize_result_solution_congruence. z + gcrt_solution_modulus_gfull_normalize_result_solution * hgcrt_mod_left_gcrt_gfull_normalize_result_solution_congruence = gcrt_solution_residue_gfull_normalize_result_solution + gcrt_solution_modulus_gfull_normalize_result_solution * hgcrt_mod_right_gcrt_gfull_normalize_result_solution_congruence)))))

Complete tactic proof in conservative notation

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

44 script commands · 13 reading checkpoints · 2 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.

Named ingredients (1)
crt canonical prefix solution implies normalized
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 hM
  9. L9
    intro hs
02Establish hzL10–13

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

  1. L10
    have hz : M = 0 \/ ~(M = 0)
  2. L11
    specialize eq_decidable M
  3. L12
    specialize eq_decidable 0
  4. L13
    apply eq_decidable
03Separate the logical casesL14–14

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

  1. L14
    cases hz
04Construct an explicit witnessL15–15

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

  1. L15
    exists x
05Separate the logical casesL16–16

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

  1. L16
    split
06Use earlier factsL17–17

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

  1. L17
    exact hM
07Separate the logical casesL18–19

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

  1. L18
    split
  2. L19
    left
08Use earlier factsL20–21

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

  1. L20
    exact hz_left
  2. L21
    exact hs
09Establish hcL22–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply crt prefix solution canonical remainder.

  1. L22
    have hc : ∃ y. CRTPrefixLCM(b,c,l,M) ∧ (Lt(y,M) ∧ CRTPrefixSolution(r,s,b,c,l,y))Definitions: CRTPrefixLCM(b,c,l,M)Lt(y,M)CRTPrefixSolution(r,s,b,c,l,y)Original native command in the exact edition
  2. L23
    specialize crt_prefix_solution_canonical_remainder r
  3. L24
    specialize crt_prefix_solution_canonical_remainder s
  4. L25
    specialize crt_prefix_solution_canonical_remainder b
  5. L26
    specialize crt_prefix_solution_canonical_remainder c
  6. L27
    specialize crt_prefix_solution_canonical_remainder l
  7. L28
    specialize crt_prefix_solution_canonical_remainder M
  8. L29
    specialize crt_prefix_solution_canonical_remainder x
  9. L30
    apply crt_prefix_solution_canonical_remainder
  10. L31
    exact hz_right
10Use earlier factsL32–33

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

  1. L32
    exact hM
  2. L33
    exact hs
11Separate the logical casesL34–34

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

  1. L34
    cases hc
12Construct an explicit witnessL35–35

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

  1. L35
    exists x1
13Use earlier factsL36–44

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

  1. L36
    specialize crt_canonical_prefix_solution_implies_normalized r
  2. L37
    specialize crt_canonical_prefix_solution_implies_normalized s
  3. L38
    specialize crt_canonical_prefix_solution_implies_normalized b
  4. L39
    specialize crt_canonical_prefix_solution_implies_normalized c
  5. L40
    specialize crt_canonical_prefix_solution_implies_normalized l
  6. L41
    specialize crt_canonical_prefix_solution_implies_normalized x1
  7. L42
    specialize crt_canonical_prefix_solution_implies_normalized M
  8. L43
    apply crt_canonical_prefix_solution_implies_normalized
  9. L44
    exact hc_witness

Library-wide reading audit

Original defined command ledger · 44 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro M
  7. 0007intro x
  8. 0008intro hM
  9. 0009intro hs
  10. 0010have hz : M = 0 \/ ~(M = 0)
  11. 0011specialize eq_decidable M
  12. 0012specialize eq_decidable 0
  13. 0013apply eq_decidable
  14. 0014cases hz
  15. 0015exists x
  16. 0016split
  17. 0017exact hM
  18. 0018split
  19. 0019left
  20. 0020exact hz_left
  21. 0021exact hs
  22. 0022have hc : ∃ y. CRTPrefixLCM(b,c,l,M) ∧ (Lt(y,M) ∧ CRTPrefixSolution(r,s,b,c,l,y))
  23. 0023specialize crt_prefix_solution_canonical_remainder r
  24. 0024specialize crt_prefix_solution_canonical_remainder s
  25. 0025specialize crt_prefix_solution_canonical_remainder b
  26. 0026specialize crt_prefix_solution_canonical_remainder c
  27. 0027specialize crt_prefix_solution_canonical_remainder l
  28. 0028specialize crt_prefix_solution_canonical_remainder M
  29. 0029specialize crt_prefix_solution_canonical_remainder x
  30. 0030apply crt_prefix_solution_canonical_remainder
  31. 0031exact hz_right
  32. 0032exact hM
  33. 0033exact hs
  34. 0034cases hc
  35. 0035exists x1
  36. 0036specialize crt_canonical_prefix_solution_implies_normalized r
  37. 0037specialize crt_canonical_prefix_solution_implies_normalized s
  38. 0038specialize crt_canonical_prefix_solution_implies_normalized b
  39. 0039specialize crt_canonical_prefix_solution_implies_normalized c
  40. 0040specialize crt_canonical_prefix_solution_implies_normalized l
  41. 0041specialize crt_canonical_prefix_solution_implies_normalized x1
  42. 0042specialize crt_canonical_prefix_solution_implies_normalized M
  43. 0043apply crt_canonical_prefix_solution_implies_normalized
  44. 0044exact hc_witness