FC0012

crt_prefix_solution_normalized_exists

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

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

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.

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 3 declared prerequisites and contains 44 exact native proof lines.

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

Proof neighborhood

Direct dependencies

eq_decidable Stable theorem; checked-use authorized crt_prefix_solution_canonical_remainder Alpha theorem; checked-use authorized FC0010 crt_canonical_prefix_solution_implies_normalized

Direct dependents

FC0013 crt_pairwise_compatible_prefix_normalized_exists_unique

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

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.

Named ingredients (1)
crt canonical prefix solution implies normalized

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–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: CRTPrefixSolutionCRTPrefixLCMLt
  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 exact 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 : exists y. ((((forall gcrt_common_index_gfull_normalize_canonical_lcm_own gcrt_common_modulus_gfull_normalize_canonical_lcm_own. (exists ff_lt_gcrt_gfull_normalize_canonical_lcm_own_bound. ff_lt_gcrt_gfull_normalize_canonical_lcm_own_bound + S gcrt_common_index_gfull_normalize_canonical_lcm_own = l) -> (((exists ff_h_gcrt_gfull_normalize_canonical_lcm_own_entry. ff_h_gcrt_gfull_normalize_canonical_lcm_own_entry + S (gcrt_common_modulus_gfull_normalize_canonical_lcm_own) = S ((S (gcrt_common_index_gfull_normalize_canonical_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_normalize_canonical_lcm_own_entry. b = ff_q_gcrt_gfull_normalize_canonical_lcm_own_entry * S ((S (gcrt_common_index_gfull_normalize_canonical_lcm_own)) * c) + (gcrt_common_modulus_gfull_normalize_canonical_lcm_own))) -> exists gcrt_common_quotient_gfull_normalize_canonical_lcm_own. M = gcrt_common_modulus_gfull_normalize_canonical_lcm_own * gcrt_common_quotient_gfull_normalize_canonical_lcm_own) /\ forall gcrt_lcm_common_gfull_normalize_canonical_lcm. (forall gcrt_common_index_gfull_normalize_canonical_lcm_other gcrt_common_modulus_gfull_normalize_canonical_lcm_other. (exists ff_lt_gcrt_gfull_normalize_canonical_lcm_other_bound. ff_lt_gcrt_gfull_normalize_canonical_lcm_other_bound + S gcrt_common_index_gfull_normalize_canonical_lcm_other = l) -> (((exists ff_h_gcrt_gfull_normalize_canonical_lcm_other_entry. ff_h_gcrt_gfull_normalize_canonical_lcm_other_entry + S (gcrt_common_modulus_gfull_normalize_canonical_lcm_other) = S ((S (gcrt_common_index_gfull_normalize_canonical_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_normalize_canonical_lcm_other_entry. b = ff_q_gcrt_gfull_normalize_canonical_lcm_other_entry * S ((S (gcrt_common_index_gfull_normalize_canonical_lcm_other)) * c) + (gcrt_common_modulus_gfull_normalize_canonical_lcm_other))) -> exists gcrt_common_quotient_gfull_normalize_canonical_lcm_other. gcrt_lcm_common_gfull_normalize_canonical_lcm = gcrt_common_modulus_gfull_normalize_canonical_lcm_other * gcrt_common_quotient_gfull_normalize_canonical_lcm_other) -> exists gcrt_lcm_quotient_gfull_normalize_canonical_lcm. gcrt_lcm_common_gfull_normalize_canonical_lcm = M * gcrt_lcm_quotient_gfull_normalize_canonical_lcm)) /\ ((exists ff_lt_gcrt_gfull_normalize_canonical_bounded. ff_lt_gcrt_gfull_normalize_canonical_bounded + S y = M) /\ (forall gcrt_solution_index_gfull_normalize_canonical_solution gcrt_solution_residue_gfull_normalize_canonical_solution gcrt_solution_modulus_gfull_normalize_canonical_solution. (exists ff_lt_gcrt_gfull_normalize_canonical_solution_bound. ff_lt_gcrt_gfull_normalize_canonical_solution_bound + S gcrt_solution_index_gfull_normalize_canonical_solution = l) -> (((exists ff_h_gcrt_gfull_normalize_canonical_solution_residue. ff_h_gcrt_gfull_normalize_canonical_solution_residue + S (gcrt_solution_residue_gfull_normalize_canonical_solution) = S ((S (gcrt_solution_index_gfull_normalize_canonical_solution)) * s)) /\ exists ff_q_gcrt_gfull_normalize_canonical_solution_residue. r = ff_q_gcrt_gfull_normalize_canonical_solution_residue * S ((S (gcrt_solution_index_gfull_normalize_canonical_solution)) * s) + (gcrt_solution_residue_gfull_normalize_canonical_solution))) -> (((exists ff_h_gcrt_gfull_normalize_canonical_solution_modulus. ff_h_gcrt_gfull_normalize_canonical_solution_modulus + S (gcrt_solution_modulus_gfull_normalize_canonical_solution) = S ((S (gcrt_solution_index_gfull_normalize_canonical_solution)) * c)) /\ exists ff_q_gcrt_gfull_normalize_canonical_solution_modulus. b = ff_q_gcrt_gfull_normalize_canonical_solution_modulus * S ((S (gcrt_solution_index_gfull_normalize_canonical_solution)) * c) + (gcrt_solution_modulus_gfull_normalize_canonical_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_normalize_canonical_solution_congruence hgcrt_mod_right_gcrt_gfull_normalize_canonical_solution_congruence. y + gcrt_solution_modulus_gfull_normalize_canonical_solution * hgcrt_mod_left_gcrt_gfull_normalize_canonical_solution_congruence = gcrt_solution_residue_gfull_normalize_canonical_solution + gcrt_solution_modulus_gfull_normalize_canonical_solution * hgcrt_mod_right_gcrt_gfull_normalize_canonical_solution_congruence))))
  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