CR0013

crt_pairwise_coprime_prefix_solution_exists

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

Every arbitrary finite beta-coded list of positive pairwise-coprime moduli has an actual simultaneous CRT solution.

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. (forall gcrt_positive_index_fold_positive gcrt_positive_value_fold_positive. (exists ff_lt_gcrt_fold_positive_bound. ff_lt_gcrt_fold_positive_bound + S gcrt_positive_index_fold_positive = l) -> (((exists ff_h_gcrt_fold_positive_entry. ff_h_gcrt_fold_positive_entry + S (gcrt_positive_value_fold_positive) = S ((S (gcrt_positive_index_fold_positive)) * c)) /\ exists ff_q_gcrt_fold_positive_entry. b = ff_q_gcrt_fold_positive_entry * S ((S (gcrt_positive_index_fold_positive)) * c) + (gcrt_positive_value_fold_positive))) -> ~(gcrt_positive_value_fold_positive = 0)) -> (forall bpr_left_index_gcrt_fold_pairwise bpr_right_index_gcrt_fold_pairwise bpr_left_value_gcrt_fold_pairwise bpr_right_value_gcrt_fold_pairwise. (exists bpr_gap_gcrt_fold_pairwise_left_bound. bpr_gap_gcrt_fold_pairwise_left_bound + S (bpr_left_index_gcrt_fold_pairwise) = l) -> (exists bpr_gap_gcrt_fold_pairwise_right_bound. bpr_gap_gcrt_fold_pairwise_right_bound + S (bpr_right_index_gcrt_fold_pairwise) = l) -> (((exists bpr_height_gcrt_fold_pairwise_left_at. bpr_height_gcrt_fold_pairwise_left_at + S (bpr_left_value_gcrt_fold_pairwise) = S ((S (bpr_left_index_gcrt_fold_pairwise)) * c)) /\ exists bpr_quotient_gcrt_fold_pairwise_left_at. b = bpr_quotient_gcrt_fold_pairwise_left_at * S ((S (bpr_left_index_gcrt_fold_pairwise)) * c) + (bpr_left_value_gcrt_fold_pairwise))) -> (((exists bpr_height_gcrt_fold_pairwise_right_at. bpr_height_gcrt_fold_pairwise_right_at + S (bpr_right_value_gcrt_fold_pairwise) = S ((S (bpr_right_index_gcrt_fold_pairwise)) * c)) /\ exists bpr_quotient_gcrt_fold_pairwise_right_at. b = bpr_quotient_gcrt_fold_pairwise_right_at * S ((S (bpr_right_index_gcrt_fold_pairwise)) * c) + (bpr_right_value_gcrt_fold_pairwise))) -> ~(bpr_left_index_gcrt_fold_pairwise = bpr_right_index_gcrt_fold_pairwise) -> (forall bpr_coprime_divisor_gcrt_fold_pairwise_coprime. (exists bpr_coprime_left_factor_gcrt_fold_pairwise_coprime. bpr_left_value_gcrt_fold_pairwise = bpr_coprime_divisor_gcrt_fold_pairwise_coprime * bpr_coprime_left_factor_gcrt_fold_pairwise_coprime) -> (exists bpr_coprime_right_factor_gcrt_fold_pairwise_coprime. bpr_right_value_gcrt_fold_pairwise = bpr_coprime_divisor_gcrt_fold_pairwise_coprime * bpr_coprime_right_factor_gcrt_fold_pairwise_coprime) -> bpr_coprime_divisor_gcrt_fold_pairwise_coprime = 1)) -> exists x. (forall gcrt_solution_index_fold_result gcrt_solution_residue_fold_result gcrt_solution_modulus_fold_result. (exists ff_lt_gcrt_fold_result_bound. ff_lt_gcrt_fold_result_bound + S gcrt_solution_index_fold_result = l) -> (((exists ff_h_gcrt_fold_result_residue. ff_h_gcrt_fold_result_residue + S (gcrt_solution_residue_fold_result) = S ((S (gcrt_solution_index_fold_result)) * s)) /\ exists ff_q_gcrt_fold_result_residue. r = ff_q_gcrt_fold_result_residue * S ((S (gcrt_solution_index_fold_result)) * s) + (gcrt_solution_residue_fold_result))) -> (((exists ff_h_gcrt_fold_result_modulus. ff_h_gcrt_fold_result_modulus + S (gcrt_solution_modulus_fold_result) = S ((S (gcrt_solution_index_fold_result)) * c)) /\ exists ff_q_gcrt_fold_result_modulus. b = ff_q_gcrt_fold_result_modulus * S ((S (gcrt_solution_index_fold_result)) * c) + (gcrt_solution_modulus_fold_result))) -> (exists hgcrt_mod_left_gcrt_fold_result_congruence hgcrt_mod_right_gcrt_fold_result_congruence. x + gcrt_solution_modulus_fold_result * hgcrt_mod_left_gcrt_fold_result_congruence = gcrt_solution_residue_fold_result + gcrt_solution_modulus_fold_result * hgcrt_mod_right_gcrt_fold_result_congruence))

Constructive proof overview

Generated structural guide

Every arbitrary finite beta-coded list of positive pairwise-coprime moduli has an actual simultaneous CRT solution.

The unchanged tactic script uses 11 declared prerequisites and contains 134 exact native proof lines.

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

Proof neighborhood

Direct dependencies

CR0005 crt_prefix_solution_empty CR0002 crt_positive_moduli_prefix_drop_last CR0004 crt_pairwise_coprime_prefix_drop_last beta_product_exists_unique Stable theorem; checked-use authorized beta_at_exists Stable theorem; checked-use authorized CR000A crt_positive_moduli_prefix_product_nonzero CR0003 crt_positive_moduli_prefix_last_nonzero CR0012 crt_pairwise_coprime_prefix_product_coprime_last binary_crt_fold_step Stable theorem; checked-use authorized beta_factor_divides_product Stable theorem; checked-use authorized CR0008 crt_prefix_solution_successor_intro

Direct dependents

CR001B crt_pairwise_coprime_prefix_canonical_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

134 script commands · 27 reading checkpoints · 10 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 (7)
crt prefix solution emptycrt positive moduli prefix drop lastcrt pairwise coprime prefix drop lastcrt positive moduli prefix product nonzerocrt positive moduli prefix last nonzerocrt pairwise coprime prefix product coprime lastcrt prefix solution successor intro

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–4

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
02Induction on lL5–7

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L5
    induction l
  2. L6
    intro hpositive
  3. L7
    intro hpairs
03Construct an explicit witnessL8–8

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

  1. L8
    exists 0
04Use earlier factsL9–15

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

  1. L9
    specialize crt_prefix_solution_empty r
  2. L10
    specialize crt_prefix_solution_empty s
  3. L11
    specialize crt_prefix_solution_empty b
  4. L12
    specialize crt_prefix_solution_empty c
  5. L13
    specialize crt_prefix_solution_empty 0
  6. L14
    specialize crt_prefix_solution_empty 0
  7. L15
    apply crt_prefix_solution_empty
05Calculate and transport equalitiesL16–16

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

  1. L16
    refl
06Fix variables and assumptionsL17–18

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

  1. L17
    intro hpositive
  2. L18
    intro hpairs
07Establish hpositive_prefixL19–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply crt positive moduli prefix drop last.

  1. L19
    have hpositive_prefix : CRTPositiveModuliPrefix(b,c,l)Definitions: CRTPositiveModuliPrefix
  2. L20
    specialize crt_positive_moduli_prefix_drop_last b
  3. L21
    specialize crt_positive_moduli_prefix_drop_last c
  4. L22
    specialize crt_positive_moduli_prefix_drop_last l
  5. L23
    apply crt_positive_moduli_prefix_drop_last
  6. L24
    exact hpositive
08Establish hpairs_prefixL25–30

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply crt pairwise coprime prefix drop last.

  1. L25
    have hpairs_prefix : CRTPairwiseCoprimePrefix(b,c,l)Definitions: CRTPairwiseCoprimePrefix
  2. L26
    specialize crt_pairwise_coprime_prefix_drop_last b
  3. L27
    specialize crt_pairwise_coprime_prefix_drop_last c
  4. L28
    specialize crt_pairwise_coprime_prefix_drop_last l
  5. L29
    apply crt_pairwise_coprime_prefix_drop_last
  6. L30
    exact hpairs
09Establish hpreviousL31–34

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

  1. L31
    have hprevious : ∃ x. CRTPrefixSolution(r,s,b,c,l,x)Definitions: CRTPrefixSolution
  2. L32
    apply IH
  3. L33
    exact hpositive_prefix
  4. L34
    exact hpairs_prefix
10Separate the logical casesL35–35

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

  1. L35
    cases hprevious
11Use earlier factsL36–38

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

  1. L36
    specialize beta_product_exists_unique b
  2. L37
    specialize beta_product_exists_unique c
  3. L38
    specialize beta_product_exists_unique l
12Separate the logical casesL39–40

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

  1. L39
    cases beta_product_exists_unique
  2. L40
    cases beta_product_exists_unique_witness
13Establish hmodulusL41–45

Establish this local claim before using it. It is not an additional assumption.

  1. L41
    have hmodulus : exists m. (((exists ff_h_gcrt_fold_last_modulus. ff_h_gcrt_fold_last_modulus + S (m) = S ((S (l)) * c)) /\ exists ff_q_gcrt_fold_last_modulus. b = ff_q_gcrt_fold_last_modulus * S ((S (l)) * c) + (m)))
  2. L42
    specialize beta_at_exists b
  3. L43
    specialize beta_at_exists c
  4. L44
    specialize beta_at_exists l
  5. L45
    exact beta_at_exists
14Separate the logical casesL46–46

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

  1. L46
    cases hmodulus
15Establish hresidueL47–51

Establish this local claim before using it. It is not an additional assumption.

  1. L47
    have hresidue : exists a. (((exists ff_h_gcrt_fold_last_residue. ff_h_gcrt_fold_last_residue + S (a) = S ((S (l)) * s)) /\ exists ff_q_gcrt_fold_last_residue. r = ff_q_gcrt_fold_last_residue * S ((S (l)) * s) + (a)))
  2. L48
    specialize beta_at_exists r
  3. L49
    specialize beta_at_exists s
  4. L50
    specialize beta_at_exists l
  5. L51
    exact beta_at_exists
16Separate the logical casesL52–52

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

  1. L52
    cases hresidue
17Establish hproduct_nonzeroL53–62

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply crt positive moduli prefix product nonzero.

  1. L53
    have hproduct_nonzero : ~(x1 = 0)
  2. L54
    specialize crt_positive_moduli_prefix_product_nonzero b
  3. L55
    specialize crt_positive_moduli_prefix_product_nonzero c
  4. L56
    specialize crt_positive_moduli_prefix_product_nonzero l
  5. L57
    specialize crt_positive_moduli_prefix_product_nonzero x1
  6. L58
    intro hzero
  7. L59
    apply crt_positive_moduli_prefix_product_nonzero
  8. L60
    exact hpositive_prefix
  9. L61
    exact beta_product_exists_unique_witness_left
  10. L62
    exact hzero
18Establish hlast_nonzeroL63–72

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply crt positive moduli prefix last nonzero.

  1. L63
    have hlast_nonzero : ~(x2 = 0)
  2. L64
    specialize crt_positive_moduli_prefix_last_nonzero b
  3. L65
    specialize crt_positive_moduli_prefix_last_nonzero c
  4. L66
    specialize crt_positive_moduli_prefix_last_nonzero l
  5. L67
    specialize crt_positive_moduli_prefix_last_nonzero x2
  6. L68
    intro hzero
  7. L69
    apply crt_positive_moduli_prefix_last_nonzero
  8. L70
    exact hpositive
  9. L71
    exact hmodulus_witness
  10. L72
    exact hzero
19Establish hcoprimeL73–82

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply crt pairwise coprime prefix product coprime last.

  1. L73
    have hcoprime : forall frp_divisor_gcrt_fold_local_coprime. (exists frp_left_factor_gcrt_fold_local_coprime. x1 = frp_divisor_gcrt_fold_local_coprime * frp_left_factor_gcrt_fold_local_coprime) -> (exists frp_right_factor_gcrt_fold_local_coprime. x2 = frp_divisor_gcrt_fold_local_coprime * frp_right_factor_gcrt_fold_local_coprime) -> frp_divisor_gcrt_fold_local_coprime = 1
  2. L74
    specialize crt_pairwise_coprime_prefix_product_coprime_last b
  3. L75
    specialize crt_pairwise_coprime_prefix_product_coprime_last c
  4. L76
    specialize crt_pairwise_coprime_prefix_product_coprime_last l
  5. L77
    specialize crt_pairwise_coprime_prefix_product_coprime_last x1
  6. L78
    specialize crt_pairwise_coprime_prefix_product_coprime_last x2
  7. L79
    apply crt_pairwise_coprime_prefix_product_coprime_last
  8. L80
    exact hpairs
  9. L81
    exact beta_product_exists_unique_witness_left
  10. L82
    exact hmodulus_witness
20Establish hfoldL83–91

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary crt fold step.

  1. L83
    have hfold : exists z. ((forall m a. (exists q. x1 = m * q) -> (exists u v. x + m * u = a + m * v) -> exists u v. z + m * u = a + m * v) /\ exists u v. z + x2 * u = x3 + x2 * v)
  2. L84
    specialize binary_crt_fold_step x1
  3. L85
    specialize binary_crt_fold_step x2
  4. L86
    specialize binary_crt_fold_step x
  5. L87
    specialize binary_crt_fold_step x3
  6. L88
    apply binary_crt_fold_step
  7. L89
    exact hproduct_nonzero
  8. L90
    exact hlast_nonzero
  9. L91
    exact hcoprime
21Separate the logical casesL92–93

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

  1. L92
    cases hfold
  2. L93
    cases hfold_witness
22Establish htransportedL94–103

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hfold witness left.

  1. L94
    have htransported : CRTPrefixSolution(r,s,b,c,l,x4)Definitions: CRTPrefixSolution
  2. L95
    intro i
  3. L96
    intro a
  4. L97
    intro m
  5. L98
    intro hi
  6. L99
    intro ha
  7. L100
    intro hm
  8. L101
    specialize hfold_witness_left m
  9. L102
    specialize hfold_witness_left a
  10. L103
    apply hfold_witness_left
23Use earlier factsL104–113

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

  1. L104
    specialize beta_factor_divides_product b
  2. L105
    specialize beta_factor_divides_product c
  3. L106
    specialize beta_factor_divides_product l
  4. L107
    specialize beta_factor_divides_product x1
  5. L108
    specialize beta_factor_divides_product i
  6. L109
    specialize beta_factor_divides_product m
  7. L110
    apply beta_factor_divides_product
  8. L111
    exact hi
  9. L112
    exact hm
  10. L113
    exact beta_product_exists_unique_witness_left
24Use earlier factsL114–120

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

  1. L114
    specialize hprevious_witness i
  2. L115
    specialize hprevious_witness a
  3. L116
    specialize hprevious_witness m
  4. L117
    apply hprevious_witness
  5. L118
    exact hi
  6. L119
    exact ha
  7. L120
    exact hm
25Construct an explicit witnessL121–121

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

  1. L121
    exists x4
26Use earlier factsL122–131

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

  1. L122
    specialize crt_prefix_solution_successor_intro r
  2. L123
    specialize crt_prefix_solution_successor_intro s
  3. L124
    specialize crt_prefix_solution_successor_intro b
  4. L125
    specialize crt_prefix_solution_successor_intro c
  5. L126
    specialize crt_prefix_solution_successor_intro l
  6. L127
    specialize crt_prefix_solution_successor_intro x4
  7. L128
    specialize crt_prefix_solution_successor_intro x3
  8. L129
    specialize crt_prefix_solution_successor_intro x2
  9. L130
    apply crt_prefix_solution_successor_intro
  10. L131
    exact htransported
27Use earlier factsL132–134

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

  1. L132
    exact hresidue_witness
  2. L133
    exact hmodulus_witness
  3. L134
    exact hfold_witness_right

Library-wide reading audit

Original exact command ledger · 134 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005induction l
  6. 0006intro hpositive
  7. 0007intro hpairs
  8. 0008exists 0
  9. 0009specialize crt_prefix_solution_empty r
  10. 0010specialize crt_prefix_solution_empty s
  11. 0011specialize crt_prefix_solution_empty b
  12. 0012specialize crt_prefix_solution_empty c
  13. 0013specialize crt_prefix_solution_empty 0
  14. 0014specialize crt_prefix_solution_empty 0
  15. 0015apply crt_prefix_solution_empty
  16. 0016refl
  17. 0017intro hpositive
  18. 0018intro hpairs
  19. 0019have hpositive_prefix : forall gcrt_positive_index_fold_positive_prefix gcrt_positive_value_fold_positive_prefix. (exists ff_lt_gcrt_fold_positive_prefix_bound. ff_lt_gcrt_fold_positive_prefix_bound + S gcrt_positive_index_fold_positive_prefix = l) -> (((exists ff_h_gcrt_fold_positive_prefix_entry. ff_h_gcrt_fold_positive_prefix_entry + S (gcrt_positive_value_fold_positive_prefix) = S ((S (gcrt_positive_index_fold_positive_prefix)) * c)) /\ exists ff_q_gcrt_fold_positive_prefix_entry. b = ff_q_gcrt_fold_positive_prefix_entry * S ((S (gcrt_positive_index_fold_positive_prefix)) * c) + (gcrt_positive_value_fold_positive_prefix))) -> ~(gcrt_positive_value_fold_positive_prefix = 0)
  20. 0020specialize crt_positive_moduli_prefix_drop_last b
  21. 0021specialize crt_positive_moduli_prefix_drop_last c
  22. 0022specialize crt_positive_moduli_prefix_drop_last l
  23. 0023apply crt_positive_moduli_prefix_drop_last
  24. 0024exact hpositive
  25. 0025have hpairs_prefix : forall bpr_left_index_gcrt_fold_pairwise_prefix bpr_right_index_gcrt_fold_pairwise_prefix bpr_left_value_gcrt_fold_pairwise_prefix bpr_right_value_gcrt_fold_pairwise_prefix. (exists bpr_gap_gcrt_fold_pairwise_prefix_left_bound. bpr_gap_gcrt_fold_pairwise_prefix_left_bound + S (bpr_left_index_gcrt_fold_pairwise_prefix) = l) -> (exists bpr_gap_gcrt_fold_pairwise_prefix_right_bound. bpr_gap_gcrt_fold_pairwise_prefix_right_bound + S (bpr_right_index_gcrt_fold_pairwise_prefix) = l) -> (((exists bpr_height_gcrt_fold_pairwise_prefix_left_at. bpr_height_gcrt_fold_pairwise_prefix_left_at + S (bpr_left_value_gcrt_fold_pairwise_prefix) = S ((S (bpr_left_index_gcrt_fold_pairwise_prefix)) * c)) /\ exists bpr_quotient_gcrt_fold_pairwise_prefix_left_at. b = bpr_quotient_gcrt_fold_pairwise_prefix_left_at * S ((S (bpr_left_index_gcrt_fold_pairwise_prefix)) * c) + (bpr_left_value_gcrt_fold_pairwise_prefix))) -> (((exists bpr_height_gcrt_fold_pairwise_prefix_right_at. bpr_height_gcrt_fold_pairwise_prefix_right_at + S (bpr_right_value_gcrt_fold_pairwise_prefix) = S ((S (bpr_right_index_gcrt_fold_pairwise_prefix)) * c)) /\ exists bpr_quotient_gcrt_fold_pairwise_prefix_right_at. b = bpr_quotient_gcrt_fold_pairwise_prefix_right_at * S ((S (bpr_right_index_gcrt_fold_pairwise_prefix)) * c) + (bpr_right_value_gcrt_fold_pairwise_prefix))) -> ~(bpr_left_index_gcrt_fold_pairwise_prefix = bpr_right_index_gcrt_fold_pairwise_prefix) -> (forall bpr_coprime_divisor_gcrt_fold_pairwise_prefix_coprime. (exists bpr_coprime_left_factor_gcrt_fold_pairwise_prefix_coprime. bpr_left_value_gcrt_fold_pairwise_prefix = bpr_coprime_divisor_gcrt_fold_pairwise_prefix_coprime * bpr_coprime_left_factor_gcrt_fold_pairwise_prefix_coprime) -> (exists bpr_coprime_right_factor_gcrt_fold_pairwise_prefix_coprime. bpr_right_value_gcrt_fold_pairwise_prefix = bpr_coprime_divisor_gcrt_fold_pairwise_prefix_coprime * bpr_coprime_right_factor_gcrt_fold_pairwise_prefix_coprime) -> bpr_coprime_divisor_gcrt_fold_pairwise_prefix_coprime = 1)
  26. 0026specialize crt_pairwise_coprime_prefix_drop_last b
  27. 0027specialize crt_pairwise_coprime_prefix_drop_last c
  28. 0028specialize crt_pairwise_coprime_prefix_drop_last l
  29. 0029apply crt_pairwise_coprime_prefix_drop_last
  30. 0030exact hpairs
  31. 0031have hprevious : exists x. (forall gcrt_solution_index_fold_previous gcrt_solution_residue_fold_previous gcrt_solution_modulus_fold_previous. (exists ff_lt_gcrt_fold_previous_bound. ff_lt_gcrt_fold_previous_bound + S gcrt_solution_index_fold_previous = l) -> (((exists ff_h_gcrt_fold_previous_residue. ff_h_gcrt_fold_previous_residue + S (gcrt_solution_residue_fold_previous) = S ((S (gcrt_solution_index_fold_previous)) * s)) /\ exists ff_q_gcrt_fold_previous_residue. r = ff_q_gcrt_fold_previous_residue * S ((S (gcrt_solution_index_fold_previous)) * s) + (gcrt_solution_residue_fold_previous))) -> (((exists ff_h_gcrt_fold_previous_modulus. ff_h_gcrt_fold_previous_modulus + S (gcrt_solution_modulus_fold_previous) = S ((S (gcrt_solution_index_fold_previous)) * c)) /\ exists ff_q_gcrt_fold_previous_modulus. b = ff_q_gcrt_fold_previous_modulus * S ((S (gcrt_solution_index_fold_previous)) * c) + (gcrt_solution_modulus_fold_previous))) -> (exists hgcrt_mod_left_gcrt_fold_previous_congruence hgcrt_mod_right_gcrt_fold_previous_congruence. x + gcrt_solution_modulus_fold_previous * hgcrt_mod_left_gcrt_fold_previous_congruence = gcrt_solution_residue_fold_previous + gcrt_solution_modulus_fold_previous * hgcrt_mod_right_gcrt_fold_previous_congruence))
  32. 0032apply IH
  33. 0033exact hpositive_prefix
  34. 0034exact hpairs_prefix
  35. 0035cases hprevious
  36. 0036specialize beta_product_exists_unique b
  37. 0037specialize beta_product_exists_unique c
  38. 0038specialize beta_product_exists_unique l
  39. 0039cases beta_product_exists_unique
  40. 0040cases beta_product_exists_unique_witness
  41. 0041have hmodulus : exists m. (((exists ff_h_gcrt_fold_last_modulus. ff_h_gcrt_fold_last_modulus + S (m) = S ((S (l)) * c)) /\ exists ff_q_gcrt_fold_last_modulus. b = ff_q_gcrt_fold_last_modulus * S ((S (l)) * c) + (m)))
  42. 0042specialize beta_at_exists b
  43. 0043specialize beta_at_exists c
  44. 0044specialize beta_at_exists l
  45. 0045exact beta_at_exists
  46. 0046cases hmodulus
  47. 0047have hresidue : exists a. (((exists ff_h_gcrt_fold_last_residue. ff_h_gcrt_fold_last_residue + S (a) = S ((S (l)) * s)) /\ exists ff_q_gcrt_fold_last_residue. r = ff_q_gcrt_fold_last_residue * S ((S (l)) * s) + (a)))
  48. 0048specialize beta_at_exists r
  49. 0049specialize beta_at_exists s
  50. 0050specialize beta_at_exists l
  51. 0051exact beta_at_exists
  52. 0052cases hresidue
  53. 0053have hproduct_nonzero : ~(x1 = 0)
  54. 0054specialize crt_positive_moduli_prefix_product_nonzero b
  55. 0055specialize crt_positive_moduli_prefix_product_nonzero c
  56. 0056specialize crt_positive_moduli_prefix_product_nonzero l
  57. 0057specialize crt_positive_moduli_prefix_product_nonzero x1
  58. 0058intro hzero
  59. 0059apply crt_positive_moduli_prefix_product_nonzero
  60. 0060exact hpositive_prefix
  61. 0061exact beta_product_exists_unique_witness_left
  62. 0062exact hzero
  63. 0063have hlast_nonzero : ~(x2 = 0)
  64. 0064specialize crt_positive_moduli_prefix_last_nonzero b
  65. 0065specialize crt_positive_moduli_prefix_last_nonzero c
  66. 0066specialize crt_positive_moduli_prefix_last_nonzero l
  67. 0067specialize crt_positive_moduli_prefix_last_nonzero x2
  68. 0068intro hzero
  69. 0069apply crt_positive_moduli_prefix_last_nonzero
  70. 0070exact hpositive
  71. 0071exact hmodulus_witness
  72. 0072exact hzero
  73. 0073have hcoprime : forall frp_divisor_gcrt_fold_local_coprime. (exists frp_left_factor_gcrt_fold_local_coprime. x1 = frp_divisor_gcrt_fold_local_coprime * frp_left_factor_gcrt_fold_local_coprime) -> (exists frp_right_factor_gcrt_fold_local_coprime. x2 = frp_divisor_gcrt_fold_local_coprime * frp_right_factor_gcrt_fold_local_coprime) -> frp_divisor_gcrt_fold_local_coprime = 1
  74. 0074specialize crt_pairwise_coprime_prefix_product_coprime_last b
  75. 0075specialize crt_pairwise_coprime_prefix_product_coprime_last c
  76. 0076specialize crt_pairwise_coprime_prefix_product_coprime_last l
  77. 0077specialize crt_pairwise_coprime_prefix_product_coprime_last x1
  78. 0078specialize crt_pairwise_coprime_prefix_product_coprime_last x2
  79. 0079apply crt_pairwise_coprime_prefix_product_coprime_last
  80. 0080exact hpairs
  81. 0081exact beta_product_exists_unique_witness_left
  82. 0082exact hmodulus_witness
  83. 0083have hfold : exists z. ((forall m a. (exists q. x1 = m * q) -> (exists u v. x + m * u = a + m * v) -> exists u v. z + m * u = a + m * v) /\ exists u v. z + x2 * u = x3 + x2 * v)
  84. 0084specialize binary_crt_fold_step x1
  85. 0085specialize binary_crt_fold_step x2
  86. 0086specialize binary_crt_fold_step x
  87. 0087specialize binary_crt_fold_step x3
  88. 0088apply binary_crt_fold_step
  89. 0089exact hproduct_nonzero
  90. 0090exact hlast_nonzero
  91. 0091exact hcoprime
  92. 0092cases hfold
  93. 0093cases hfold_witness
  94. 0094have htransported : forall gcrt_solution_index_fold_transported gcrt_solution_residue_fold_transported gcrt_solution_modulus_fold_transported. (exists ff_lt_gcrt_fold_transported_bound. ff_lt_gcrt_fold_transported_bound + S gcrt_solution_index_fold_transported = l) -> (((exists ff_h_gcrt_fold_transported_residue. ff_h_gcrt_fold_transported_residue + S (gcrt_solution_residue_fold_transported) = S ((S (gcrt_solution_index_fold_transported)) * s)) /\ exists ff_q_gcrt_fold_transported_residue. r = ff_q_gcrt_fold_transported_residue * S ((S (gcrt_solution_index_fold_transported)) * s) + (gcrt_solution_residue_fold_transported))) -> (((exists ff_h_gcrt_fold_transported_modulus. ff_h_gcrt_fold_transported_modulus + S (gcrt_solution_modulus_fold_transported) = S ((S (gcrt_solution_index_fold_transported)) * c)) /\ exists ff_q_gcrt_fold_transported_modulus. b = ff_q_gcrt_fold_transported_modulus * S ((S (gcrt_solution_index_fold_transported)) * c) + (gcrt_solution_modulus_fold_transported))) -> (exists hgcrt_mod_left_gcrt_fold_transported_congruence hgcrt_mod_right_gcrt_fold_transported_congruence. x4 + gcrt_solution_modulus_fold_transported * hgcrt_mod_left_gcrt_fold_transported_congruence = gcrt_solution_residue_fold_transported + gcrt_solution_modulus_fold_transported * hgcrt_mod_right_gcrt_fold_transported_congruence)
  95. 0095intro i
  96. 0096intro a
  97. 0097intro m
  98. 0098intro hi
  99. 0099intro ha
  100. 0100intro hm
  101. 0101specialize hfold_witness_left m
  102. 0102specialize hfold_witness_left a
  103. 0103apply hfold_witness_left
  104. 0104specialize beta_factor_divides_product b
  105. 0105specialize beta_factor_divides_product c
  106. 0106specialize beta_factor_divides_product l
  107. 0107specialize beta_factor_divides_product x1
  108. 0108specialize beta_factor_divides_product i
  109. 0109specialize beta_factor_divides_product m
  110. 0110apply beta_factor_divides_product
  111. 0111exact hi
  112. 0112exact hm
  113. 0113exact beta_product_exists_unique_witness_left
  114. 0114specialize hprevious_witness i
  115. 0115specialize hprevious_witness a
  116. 0116specialize hprevious_witness m
  117. 0117apply hprevious_witness
  118. 0118exact hi
  119. 0119exact ha
  120. 0120exact hm
  121. 0121exists x4
  122. 0122specialize crt_prefix_solution_successor_intro r
  123. 0123specialize crt_prefix_solution_successor_intro s
  124. 0124specialize crt_prefix_solution_successor_intro b
  125. 0125specialize crt_prefix_solution_successor_intro c
  126. 0126specialize crt_prefix_solution_successor_intro l
  127. 0127specialize crt_prefix_solution_successor_intro x4
  128. 0128specialize crt_prefix_solution_successor_intro x3
  129. 0129specialize crt_prefix_solution_successor_intro x2
  130. 0130apply crt_prefix_solution_successor_intro
  131. 0131exact htransported
  132. 0132exact hresidue_witness
  133. 0133exact hmodulus_witness
  134. 0134exact hfold_witness_right

Separate complete second-wave branches: Full G011 proof · Alpha v27.