CR000A

crt_positive_moduli_prefix_product_nonzero

A genuine beta-coded product of an arbitrary positive finite modulus list is nonzero.

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

∀ b. ∀ c. ∀ l. ∀ x. CRTPositiveModuliPrefix(b,c,l) → (∃ y. ∃ z. Beta(y,z,0,1) ∧ (Beta(y,z,l,x) ∧ (∀ n. Lt(n,l) → ∃ m. ∃ k. ∃ i. Beta(b,c,n,m) ∧ (Beta(y,z,n,k) ∧ (Beta(y,z,S n,i) ∧ i = k · m))))) → ¬x = 0

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

Definition DAG

Beta(b,c,i,x) · 5CRTPositiveModuliPrefix(b,c,l) · 1Lt(a,b) · 1

Actual proof prerequisites

beta_product_zero · checked external prerequisitesucc_ne_zero · checked external prerequisitebeta_product_succ_decompose · checked external prerequisitecrt_positive_moduli_prefix_drop_lastcrt_positive_moduli_prefix_last_nonzeromul_ne_zero · checked external prerequisite
Original expanded first-order statement 
forall b c l x. (forall gcrt_positive_index_product_nonzero_source gcrt_positive_value_product_nonzero_source. (exists ff_lt_gcrt_product_nonzero_source_bound. ff_lt_gcrt_product_nonzero_source_bound + S gcrt_positive_index_product_nonzero_source = l) -> (((exists ff_h_gcrt_product_nonzero_source_entry. ff_h_gcrt_product_nonzero_source_entry + S (gcrt_positive_value_product_nonzero_source) = S ((S (gcrt_positive_index_product_nonzero_source)) * c)) /\ exists ff_q_gcrt_product_nonzero_source_entry. b = ff_q_gcrt_product_nonzero_source_entry * S ((S (gcrt_positive_index_product_nonzero_source)) * c) + (gcrt_positive_value_product_nonzero_source))) -> ~(gcrt_positive_value_product_nonzero_source = 0)) -> (exists ff_u_gcrt_product_nonzero ff_v_gcrt_product_nonzero. ((((exists ff_h_gcrt_product_nonzero_start. ff_h_gcrt_product_nonzero_start + S (1) = S ((S (0)) * ff_v_gcrt_product_nonzero)) /\ exists ff_q_gcrt_product_nonzero_start. ff_u_gcrt_product_nonzero = ff_q_gcrt_product_nonzero_start * S ((S (0)) * ff_v_gcrt_product_nonzero) + (1))) /\ ((((exists ff_h_gcrt_product_nonzero_terminal. ff_h_gcrt_product_nonzero_terminal + S (x) = S ((S (l)) * ff_v_gcrt_product_nonzero)) /\ exists ff_q_gcrt_product_nonzero_terminal. ff_u_gcrt_product_nonzero = ff_q_gcrt_product_nonzero_terminal * S ((S (l)) * ff_v_gcrt_product_nonzero) + (x))) /\ forall ff_i_gcrt_product_nonzero. (exists ff_lt_gcrt_product_nonzero_bound. ff_lt_gcrt_product_nonzero_bound + S ff_i_gcrt_product_nonzero = l) -> exists ff_p_gcrt_product_nonzero ff_r_gcrt_product_nonzero ff_s_gcrt_product_nonzero. ((((exists ff_h_gcrt_product_nonzero_factor. ff_h_gcrt_product_nonzero_factor + S (ff_p_gcrt_product_nonzero) = S ((S (ff_i_gcrt_product_nonzero)) * c)) /\ exists ff_q_gcrt_product_nonzero_factor. b = ff_q_gcrt_product_nonzero_factor * S ((S (ff_i_gcrt_product_nonzero)) * c) + (ff_p_gcrt_product_nonzero))) /\ ((((exists ff_h_gcrt_product_nonzero_partial. ff_h_gcrt_product_nonzero_partial + S (ff_r_gcrt_product_nonzero) = S ((S (ff_i_gcrt_product_nonzero)) * ff_v_gcrt_product_nonzero)) /\ exists ff_q_gcrt_product_nonzero_partial. ff_u_gcrt_product_nonzero = ff_q_gcrt_product_nonzero_partial * S ((S (ff_i_gcrt_product_nonzero)) * ff_v_gcrt_product_nonzero) + (ff_r_gcrt_product_nonzero))) /\ ((((exists ff_h_gcrt_product_nonzero_successor. ff_h_gcrt_product_nonzero_successor + S (ff_s_gcrt_product_nonzero) = S ((S (S ff_i_gcrt_product_nonzero)) * ff_v_gcrt_product_nonzero)) /\ exists ff_q_gcrt_product_nonzero_successor. ff_u_gcrt_product_nonzero = ff_q_gcrt_product_nonzero_successor * S ((S (S ff_i_gcrt_product_nonzero)) * ff_v_gcrt_product_nonzero) + (ff_s_gcrt_product_nonzero))) /\ ff_s_gcrt_product_nonzero = ff_r_gcrt_product_nonzero * ff_p_gcrt_product_nonzero)))))) -> ~(x = 0)

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

62 script commands · 11 reading checkpoints · 5 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 (2)
crt positive moduli prefix drop lastcrt positive moduli prefix last nonzero

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

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

  1. L1
    intro b
  2. L2
    intro c
02Induction on lL3–7

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

  1. L3
    induction l
  2. L4
    intro x
  3. L5
    intro hpositive
  4. L6
    intro hproduct
  5. L7
    intro hzero
03Establish hunitL8–17

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

  1. L8
    have hunit : x = 1
  2. L9
    specialize beta_product_zero b
  3. L10
    specialize beta_product_zero c
  4. L11
    specialize beta_product_zero x
  5. L12
    apply beta_product_zero
  6. L13
    exact hproduct
  7. L14
    rewrite hunit at hzero
  8. L15
    specialize succ_ne_zero 0
  9. L16
    apply succ_ne_zero
  10. L17
    exact hzero
04Fix variables and assumptionsL18–21

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

  1. L18
    intro x
  2. L19
    intro hpositive
  3. L20
    intro hproduct
  4. L21
    intro hzero
05Establish hdecompositionL22–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product succ decompose.

  1. L22
    have hdecomposition : ∃ p. ∃ q. Beta(b,c,l,p) ∧ ((∃ y. ∃ z. Beta(y,z,0,1) ∧ (Beta(y,z,l,q) ∧ (∀ n. Lt(n,l) → ∃ m. ∃ k. ∃ i. Beta(b,c,n,m) ∧ (Beta(y,z,n,k) ∧ (Beta(y,z,S n,i) ∧ i = k · m))))) ∧ x = q · p)Definitions: BetaLtOriginal native command in the exact edition
  2. L23
    specialize beta_product_succ_decompose b
  3. L24
    specialize beta_product_succ_decompose c
  4. L25
    specialize beta_product_succ_decompose l
  5. L26
    specialize beta_product_succ_decompose x
  6. L27
    apply beta_product_succ_decompose
  7. L28
    exact hproduct
06Separate the logical casesL29–32

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

  1. L29
    cases hdecomposition
  2. L30
    cases hdecomposition_witness
  3. L31
    cases hdecomposition_witness_witness
  4. L32
    cases hdecomposition_witness_witness_right
07Establish hrestrictedL33–38

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. L33
    have hrestricted : CRTPositiveModuliPrefix(b,c,l)Definitions: CRTPositiveModuliPrefixOriginal native command in the exact edition
  2. L34
    specialize crt_positive_moduli_prefix_drop_last b
  3. L35
    specialize crt_positive_moduli_prefix_drop_last c
  4. L36
    specialize crt_positive_moduli_prefix_drop_last l
  5. L37
    apply crt_positive_moduli_prefix_drop_last
  6. L38
    exact hpositive
08Establish hprefix_nonzeroL39–45

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

  1. L39
    have hprefix_nonzero : ~(x2 = 0)
  2. L40
    specialize IH x2
  3. L41
    intro hprefix_zero
  4. L42
    apply IH
  5. L43
    exact hrestricted
  6. L44
    exact hdecomposition_witness_witness_right_left
  7. L45
    exact hprefix_zero
09Establish hlast_nonzeroL46–55

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. L46
    have hlast_nonzero : ~(x1 = 0)
  2. L47
    specialize crt_positive_moduli_prefix_last_nonzero b
  3. L48
    specialize crt_positive_moduli_prefix_last_nonzero c
  4. L49
    specialize crt_positive_moduli_prefix_last_nonzero l
  5. L50
    specialize crt_positive_moduli_prefix_last_nonzero x1
  6. L51
    intro hlast_zero
  7. L52
    apply crt_positive_moduli_prefix_last_nonzero
  8. L53
    exact hpositive
  9. L54
    exact hdecomposition_witness_witness_left
  10. L55
    exact hlast_zero
10Calculate and transport equalitiesL56–56

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

  1. L56
    rewrite hdecomposition_witness_witness_right_right at hzero
11Use earlier factsL57–62

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

  1. L57
    specialize mul_ne_zero x2
  2. L58
    specialize mul_ne_zero x1
  3. L59
    apply mul_ne_zero
  4. L60
    exact hprefix_nonzero
  5. L61
    exact hlast_nonzero
  6. L62
    exact hzero

Library-wide reading audit

Original defined command ledger · 62 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003induction l
  4. 0004intro x
  5. 0005intro hpositive
  6. 0006intro hproduct
  7. 0007intro hzero
  8. 0008have hunit : x = 1
  9. 0009specialize beta_product_zero b
  10. 0010specialize beta_product_zero c
  11. 0011specialize beta_product_zero x
  12. 0012apply beta_product_zero
  13. 0013exact hproduct
  14. 0014rewrite hunit at hzero
  15. 0015specialize succ_ne_zero 0
  16. 0016apply succ_ne_zero
  17. 0017exact hzero
  18. 0018intro x
  19. 0019intro hpositive
  20. 0020intro hproduct
  21. 0021intro hzero
  22. 0022have hdecomposition : exists p q. ((((exists ff_h_gcrt_nonzero_decompose_last. ff_h_gcrt_nonzero_decompose_last + S (p) = S ((S (l)) * c)) /\ exists ff_q_gcrt_nonzero_decompose_last. b = ff_q_gcrt_nonzero_decompose_last * S ((S (l)) * c) + (p))) /\ ((exists ff_u_gcrt_nonzero_decompose_prefix ff_v_gcrt_nonzero_decompose_prefix. ((((exists ff_h_gcrt_nonzero_decompose_prefix_start. ff_h_gcrt_nonzero_decompose_prefix_start + S (1) = S ((S (0)) * ff_v_gcrt_nonzero_decompose_prefix)) /\ exists ff_q_gcrt_nonzero_decompose_prefix_start. ff_u_gcrt_nonzero_decompose_prefix = ff_q_gcrt_nonzero_decompose_prefix_start * S ((S (0)) * ff_v_gcrt_nonzero_decompose_prefix) + (1))) /\ ((((exists ff_h_gcrt_nonzero_decompose_prefix_terminal. ff_h_gcrt_nonzero_decompose_prefix_terminal + S (q) = S ((S (l)) * ff_v_gcrt_nonzero_decompose_prefix)) /\ exists ff_q_gcrt_nonzero_decompose_prefix_terminal. ff_u_gcrt_nonzero_decompose_prefix = ff_q_gcrt_nonzero_decompose_prefix_terminal * S ((S (l)) * ff_v_gcrt_nonzero_decompose_prefix) + (q))) /\ forall ff_i_gcrt_nonzero_decompose_prefix. (exists ff_lt_gcrt_nonzero_decompose_prefix_bound. ff_lt_gcrt_nonzero_decompose_prefix_bound + S ff_i_gcrt_nonzero_decompose_prefix = l) -> exists ff_p_gcrt_nonzero_decompose_prefix ff_r_gcrt_nonzero_decompose_prefix ff_s_gcrt_nonzero_decompose_prefix. ((((exists ff_h_gcrt_nonzero_decompose_prefix_factor. ff_h_gcrt_nonzero_decompose_prefix_factor + S (ff_p_gcrt_nonzero_decompose_prefix) = S ((S (ff_i_gcrt_nonzero_decompose_prefix)) * c)) /\ exists ff_q_gcrt_nonzero_decompose_prefix_factor. b = ff_q_gcrt_nonzero_decompose_prefix_factor * S ((S (ff_i_gcrt_nonzero_decompose_prefix)) * c) + (ff_p_gcrt_nonzero_decompose_prefix))) /\ ((((exists ff_h_gcrt_nonzero_decompose_prefix_partial. ff_h_gcrt_nonzero_decompose_prefix_partial + S (ff_r_gcrt_nonzero_decompose_prefix) = S ((S (ff_i_gcrt_nonzero_decompose_prefix)) * ff_v_gcrt_nonzero_decompose_prefix)) /\ exists ff_q_gcrt_nonzero_decompose_prefix_partial. ff_u_gcrt_nonzero_decompose_prefix = ff_q_gcrt_nonzero_decompose_prefix_partial * S ((S (ff_i_gcrt_nonzero_decompose_prefix)) * ff_v_gcrt_nonzero_decompose_prefix) + (ff_r_gcrt_nonzero_decompose_prefix))) /\ ((((exists ff_h_gcrt_nonzero_decompose_prefix_successor. ff_h_gcrt_nonzero_decompose_prefix_successor + S (ff_s_gcrt_nonzero_decompose_prefix) = S ((S (S ff_i_gcrt_nonzero_decompose_prefix)) * ff_v_gcrt_nonzero_decompose_prefix)) /\ exists ff_q_gcrt_nonzero_decompose_prefix_successor. ff_u_gcrt_nonzero_decompose_prefix = ff_q_gcrt_nonzero_decompose_prefix_successor * S ((S (S ff_i_gcrt_nonzero_decompose_prefix)) * ff_v_gcrt_nonzero_decompose_prefix) + (ff_s_gcrt_nonzero_decompose_prefix))) /\ ff_s_gcrt_nonzero_decompose_prefix = ff_r_gcrt_nonzero_decompose_prefix * ff_p_gcrt_nonzero_decompose_prefix)))))) /\ x = q * p))
  23. 0023specialize beta_product_succ_decompose b
  24. 0024specialize beta_product_succ_decompose c
  25. 0025specialize beta_product_succ_decompose l
  26. 0026specialize beta_product_succ_decompose x
  27. 0027apply beta_product_succ_decompose
  28. 0028exact hproduct
  29. 0029cases hdecomposition
  30. 0030cases hdecomposition_witness
  31. 0031cases hdecomposition_witness_witness
  32. 0032cases hdecomposition_witness_witness_right
  33. 0033have hrestricted : forall gcrt_positive_index_product_nonzero_restricted gcrt_positive_value_product_nonzero_restricted. (exists ff_lt_gcrt_product_nonzero_restricted_bound. ff_lt_gcrt_product_nonzero_restricted_bound + S gcrt_positive_index_product_nonzero_restricted = l) -> (((exists ff_h_gcrt_product_nonzero_restricted_entry. ff_h_gcrt_product_nonzero_restricted_entry + S (gcrt_positive_value_product_nonzero_restricted) = S ((S (gcrt_positive_index_product_nonzero_restricted)) * c)) /\ exists ff_q_gcrt_product_nonzero_restricted_entry. b = ff_q_gcrt_product_nonzero_restricted_entry * S ((S (gcrt_positive_index_product_nonzero_restricted)) * c) + (gcrt_positive_value_product_nonzero_restricted))) -> ~(gcrt_positive_value_product_nonzero_restricted = 0)
  34. 0034specialize crt_positive_moduli_prefix_drop_last b
  35. 0035specialize crt_positive_moduli_prefix_drop_last c
  36. 0036specialize crt_positive_moduli_prefix_drop_last l
  37. 0037apply crt_positive_moduli_prefix_drop_last
  38. 0038exact hpositive
  39. 0039have hprefix_nonzero : ~(x2 = 0)
  40. 0040specialize IH x2
  41. 0041intro hprefix_zero
  42. 0042apply IH
  43. 0043exact hrestricted
  44. 0044exact hdecomposition_witness_witness_right_left
  45. 0045exact hprefix_zero
  46. 0046have hlast_nonzero : ~(x1 = 0)
  47. 0047specialize crt_positive_moduli_prefix_last_nonzero b
  48. 0048specialize crt_positive_moduli_prefix_last_nonzero c
  49. 0049specialize crt_positive_moduli_prefix_last_nonzero l
  50. 0050specialize crt_positive_moduli_prefix_last_nonzero x1
  51. 0051intro hlast_zero
  52. 0052apply crt_positive_moduli_prefix_last_nonzero
  53. 0053exact hpositive
  54. 0054exact hdecomposition_witness_witness_left
  55. 0055exact hlast_zero
  56. 0056rewrite hdecomposition_witness_witness_right_right at hzero
  57. 0057specialize mul_ne_zero x2
  58. 0058specialize mul_ne_zero x1
  59. 0059apply mul_ne_zero
  60. 0060exact hprefix_nonzero
  61. 0061exact hlast_nonzero
  62. 0062exact hzero