PA001U

beta_exclusive_accumulated_product_step

Stable checked-use theorem · independently closed

Extend the accumulated target-modulus product for an exclusive prefix.

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 PA statement

forall N c k P. (forall t. (exists h. S t + S h = S N) -> exists q. c = S t * q) -> (exists h. h + S k = N) -> ~(P = 0) -> (forall i. (exists h. h + S i = k) -> exists q. P = S ((S i) * c) * q) -> (forall j. (exists g. g + k = j) -> (exists h. h + j = N) -> forall d. (exists u. P = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1) -> (~(P * S ((S k) * c) = 0) /\ ((forall i. (exists h. h + S i = S k) -> exists q. P * S ((S k) * c) = S ((S i) * c) * q) /\ forall j. (exists g. g + S k = j) -> (exists h. h + j = N) -> forall d. (exists u. P * S ((S k) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1))

Structural proof guide

Generated structural guide

Extend the accumulated target-modulus product for an exclusive prefix.

Use the direct prerequisites mul_ne_zero, right_factor_divides_product, beta_modulus_nonzero, le_of_succ_le_succ, le_eq_or_lt, multiple_mul_right, le_succ_self, le_trans, lt_to_le, lt_irrefl_expanded, beta_moduli_pairwise_coprime_bounded, coprime_mul_left as previously established PA formulas.

The proof proceeds by case analysis (1), intermediate claims (11), equality transport (2).

Referenced ingredients

PA000S mul_ne_zero PA000T right_factor_divides_product PA000U beta_modulus_nonzero PA000V le_of_succ_le_succ PA000W le_eq_or_lt PA000C multiple_mul_right PA000Q le_succ_self PA000R le_trans PA000X lt_to_le PA0010 lt_irrefl_expanded PA001S beta_moduli_pairwise_coprime_bounded PA001T coprime_mul_left

Proof neighborhood

Direct dependencies

PA000S mul_ne_zero PA000T right_factor_divides_product PA000U beta_modulus_nonzero PA000V le_of_succ_le_succ PA000W le_eq_or_lt PA000C multiple_mul_right PA000Q le_succ_self PA000R le_trans PA000X lt_to_le PA0010 lt_irrefl_expanded PA001S beta_moduli_pairwise_coprime_bounded PA001T coprime_mul_left

Direct dependents

PA002H beta_exclusive_recode_invariant_step

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

Read the argument

Proof checkpoints

95 script commands · 23 reading checkpoints · 11 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 (12)
mul ne zeroright factor divides productbeta modulus nonzerole of succ le succle eq or ltmultiple mul rightle succ selfle translt to lelt irrefl expandedbeta moduli pairwise coprime boundedcoprime mul left
01Fix variables and assumptionsL1–9

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

  1. L1
    intro N
  2. L2
    intro c
  3. L3
    intro k
  4. L4
    intro P
  5. L5
    intro hcm
  6. L6
    intro hkN
  7. L7
    intro hP
  8. L8
    intro hdiv
  9. L9
    intro hfuture
02Establish hnewL10–13

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

  1. L10
    have hnew : ~(S ((S k) * c) = 0)
  2. L11
    specialize beta_modulus_nonzero c
  3. L12
    specialize beta_modulus_nonzero k
  4. L13
    exact beta_modulus_nonzero
03Separate the logical casesL14–14

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

  1. L14
    split
04Use earlier factsL15–16

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

  1. L15
    specialize mul_ne_zero P
  2. L16
    specialize mul_ne_zero (S ((S k) * c))
05Fix variables and assumptionsL17–17

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

  1. L17
    intro hzero
06Use earlier factsL18–21

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

  1. L18
    apply mul_ne_zero
  2. L19
    exact hP
  3. L20
    exact hnew
  4. L21
    exact hzero
07Separate the logical casesL22–22

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

  1. L22
    split
08Fix variables and assumptionsL23–24

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

  1. L23
    intro i
  2. L24
    intro hi
09Establish hikL25–29

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

  1. L25
    have hik : exists r. r + i = k
  2. L26
    specialize le_of_succ_le_succ i
  3. L27
    specialize le_of_succ_le_succ k
  4. L28
    apply le_of_succ_le_succ
  5. L29
    exact hi
10Establish hsplitL30–34

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

  1. L30
    have hsplit : i = k \/ exists r. r + S i = k
  2. L31
    specialize le_eq_or_lt i
  3. L32
    specialize le_eq_or_lt k
  4. L33
    apply le_eq_or_lt
  5. L34
    exact hik
11Separate the logical casesL35–35

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

  1. L35
    cases hsplit
12Calculate and transport equalitiesL36–36

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

  1. L36
    rewrite hsplit_left
13Use earlier factsL37–39

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

  1. L37
    specialize right_factor_divides_product P
  2. L38
    specialize right_factor_divides_product (S ((S k) * c))
  3. L39
    exact right_factor_divides_product
14Establish hiPL40–49

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

  1. L40
    have hiP : exists q. P = S ((S i) * c) * q
  2. L41
    specialize hdiv i
  3. L42
    apply hdiv
  4. L43
    exact hsplit_right
  5. L44
    specialize multiple_mul_right (S ((S i) * c))
  6. L45
    specialize multiple_mul_right P
  7. L46
    specialize multiple_mul_right (S ((S k) * c))
  8. L47
    apply multiple_mul_right
  9. L48
    exact hiP
  10. L49
    intro j
15Fix variables and assumptionsL50–51

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

  1. L50
    intro hSkj
  2. L51
    intro hjN
16Establish hkjL52–52

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

  1. L52
    have hkj : exists r. r + k = j
17Establish hkSkL53–61

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

  1. L53
    have hkSk : exists r. r + k = S k
  2. L54
    specialize le_succ_self k
  3. L55
    exact le_succ_self
  4. L56
    specialize le_trans k
  5. L57
    specialize le_trans (S k)
  6. L58
    specialize le_trans j
  7. L59
    apply le_trans
  8. L60
    exact hkSk
  9. L61
    exact hSkj
18Establish hPjL62–66

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

  1. L62
    have hPj : forall d. (exists u. P = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1
  2. L63
    specialize hfuture j
  3. L64
    apply hfuture
  4. L65
    exact hkj
  5. L66
    exact hjN
19Establish hneqL67–72

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

  1. L67
    have hneq : ~(k = j)
  2. L68
    intro heq
  3. L69
    rewrite <- heq at hSkj
  4. L70
    specialize lt_irrefl_expanded k
  5. L71
    apply lt_irrefl_expanded
  6. L72
    exact hSkj
20Establish hkboundL73–77

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

  1. L73
    have hkbound : exists r. r + k = N
  2. L74
    specialize lt_to_le k
  3. L75
    specialize lt_to_le N
  4. L76
    apply lt_to_le
  5. L77
    exact hkN
21Establish hpairsL78–82

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta moduli pairwise coprime bounded.

  1. L78
    have hpairs : forall i j. ~(i = j) -> (exists hi. hi + i = N) -> (exists hj. hj + j = N) -> forall d. (exists u. S ((S i) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1
  2. L79
    specialize beta_moduli_pairwise_coprime_bounded N
  3. L80
    specialize beta_moduli_pairwise_coprime_bounded c
  4. L81
    apply beta_moduli_pairwise_coprime_bounded
  5. L82
    exact hcm
22Establish hnewjL83–92

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

  1. L83
    have hnewj : forall d. (exists u. S ((S k) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1
  2. L84
    specialize hpairs k
  3. L85
    specialize hpairs j
  4. L86
    apply hpairs
  5. L87
    exact hneq
  6. L88
    exact hkbound
  7. L89
    exact hjN
  8. L90
    specialize coprime_mul_left P
  9. L91
    specialize coprime_mul_left (S ((S k) * c))
  10. L92
    specialize coprime_mul_left (S ((S j) * c))
23Use earlier factsL93–95

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

  1. L93
    apply coprime_mul_left
  2. L94
    exact hPj
  3. L95
    exact hnewj

Library-wide reading audit

Original exact command ledger · 95 lines
  1. 0001intro N
  2. 0002intro c
  3. 0003intro k
  4. 0004intro P
  5. 0005intro hcm
  6. 0006intro hkN
  7. 0007intro hP
  8. 0008intro hdiv
  9. 0009intro hfuture
  10. 0010have hnew : ~(S ((S k) * c) = 0)
  11. 0011specialize beta_modulus_nonzero c
  12. 0012specialize beta_modulus_nonzero k
  13. 0013exact beta_modulus_nonzero
  14. 0014split
  15. 0015specialize mul_ne_zero P
  16. 0016specialize mul_ne_zero (S ((S k) * c))
  17. 0017intro hzero
  18. 0018apply mul_ne_zero
  19. 0019exact hP
  20. 0020exact hnew
  21. 0021exact hzero
  22. 0022split
  23. 0023intro i
  24. 0024intro hi
  25. 0025have hik : exists r. r + i = k
  26. 0026specialize le_of_succ_le_succ i
  27. 0027specialize le_of_succ_le_succ k
  28. 0028apply le_of_succ_le_succ
  29. 0029exact hi
  30. 0030have hsplit : i = k \/ exists r. r + S i = k
  31. 0031specialize le_eq_or_lt i
  32. 0032specialize le_eq_or_lt k
  33. 0033apply le_eq_or_lt
  34. 0034exact hik
  35. 0035cases hsplit
  36. 0036rewrite hsplit_left
  37. 0037specialize right_factor_divides_product P
  38. 0038specialize right_factor_divides_product (S ((S k) * c))
  39. 0039exact right_factor_divides_product
  40. 0040have hiP : exists q. P = S ((S i) * c) * q
  41. 0041specialize hdiv i
  42. 0042apply hdiv
  43. 0043exact hsplit_right
  44. 0044specialize multiple_mul_right (S ((S i) * c))
  45. 0045specialize multiple_mul_right P
  46. 0046specialize multiple_mul_right (S ((S k) * c))
  47. 0047apply multiple_mul_right
  48. 0048exact hiP
  49. 0049intro j
  50. 0050intro hSkj
  51. 0051intro hjN
  52. 0052have hkj : exists r. r + k = j
  53. 0053have hkSk : exists r. r + k = S k
  54. 0054specialize le_succ_self k
  55. 0055exact le_succ_self
  56. 0056specialize le_trans k
  57. 0057specialize le_trans (S k)
  58. 0058specialize le_trans j
  59. 0059apply le_trans
  60. 0060exact hkSk
  61. 0061exact hSkj
  62. 0062have hPj : forall d. (exists u. P = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1
  63. 0063specialize hfuture j
  64. 0064apply hfuture
  65. 0065exact hkj
  66. 0066exact hjN
  67. 0067have hneq : ~(k = j)
  68. 0068intro heq
  69. 0069rewrite <- heq at hSkj
  70. 0070specialize lt_irrefl_expanded k
  71. 0071apply lt_irrefl_expanded
  72. 0072exact hSkj
  73. 0073have hkbound : exists r. r + k = N
  74. 0074specialize lt_to_le k
  75. 0075specialize lt_to_le N
  76. 0076apply lt_to_le
  77. 0077exact hkN
  78. 0078have hpairs : forall i j. ~(i = j) -> (exists hi. hi + i = N) -> (exists hj. hj + j = N) -> forall d. (exists u. S ((S i) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1
  79. 0079specialize beta_moduli_pairwise_coprime_bounded N
  80. 0080specialize beta_moduli_pairwise_coprime_bounded c
  81. 0081apply beta_moduli_pairwise_coprime_bounded
  82. 0082exact hcm
  83. 0083have hnewj : forall d. (exists u. S ((S k) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1
  84. 0084specialize hpairs k
  85. 0085specialize hpairs j
  86. 0086apply hpairs
  87. 0087exact hneq
  88. 0088exact hkbound
  89. 0089exact hjN
  90. 0090specialize coprime_mul_left P
  91. 0091specialize coprime_mul_left (S ((S k) * c))
  92. 0092specialize coprime_mul_left (S ((S j) * c))
  93. 0093apply coprime_mul_left
  94. 0094exact hPj
  95. 0095exact hnewj