PC001E

primorial_cutoff_weighted_lower

Every prime strictly beyond the cutoff contributes at least the cutoff to the actual primorial product.

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.

These are the exact finite integer inequalities with constant 8, for every N≥2. The proof uses constructive binomial and primorial infrastructure; it does not assume logarithms, asymptotic estimates, the prime number theorem, or a factorization oracle.

Exact theorem in conservative defined notation

∀ u. ∀ b. ∀ c. ∀ d. ∀ f. ∀ g. ∀ h. ∀ l. (∀ x. Lt(x,l) → ∃ y. BetaAt(b,c,x,y) ∧ (Prime(S x) ∧ y = S x ∨ ¬Prime(S x) ∧ y = 1)) → PrimeBitPrefix(d,f,l) → BetaCutoffPrefix(u,d,f,g,h,l) → ∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(g,h,x,z) → z = 0 ∧ Lt(0,y) ∨ z = 1 ∧ Le(u,y)

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

Definition DAG

PrimeBitPrefix(b,c,l) · 1BetaCutoffPrefix(u,b,c,d,f,l) · 1Le(a,b) · 2Lt(a,b) · 5Prime(p) · 6BetaAt(b,c,i,x) · 4

Actual proof prerequisites

primorial_prefix_decoded_choiceprimorial_factor_choice_one_lebeta_cutoff_prefix_entryprime_bit_prefix_entryle_succ · checked external prerequisite
Original expanded first-order statement 
forall u b c d f g h l. (forall bpr_index_pc_prim_weight_factors. (exists bpr_gap_pc_prim_weight_factors_bound. bpr_gap_pc_prim_weight_factors_bound + S (bpr_index_pc_prim_weight_factors) = l) -> exists bpr_value_pc_prim_weight_factors. ((((exists bpr_height_pc_prim_weight_factors_decoded. bpr_height_pc_prim_weight_factors_decoded + S (bpr_value_pc_prim_weight_factors) = S ((S (bpr_index_pc_prim_weight_factors)) * c)) /\ exists bpr_quotient_pc_prim_weight_factors_decoded. b = bpr_quotient_pc_prim_weight_factors_decoded * S ((S (bpr_index_pc_prim_weight_factors)) * c) + (bpr_value_pc_prim_weight_factors))) /\ (((((~(S (bpr_index_pc_prim_weight_factors) = 1) /\ forall bpr_left_pc_prim_weight_factors_choice_prime bpr_right_pc_prim_weight_factors_choice_prime. S (bpr_index_pc_prim_weight_factors) = bpr_left_pc_prim_weight_factors_choice_prime * bpr_right_pc_prim_weight_factors_choice_prime -> bpr_left_pc_prim_weight_factors_choice_prime = 1 \/ bpr_right_pc_prim_weight_factors_choice_prime = 1)) /\ bpr_value_pc_prim_weight_factors = S (bpr_index_pc_prim_weight_factors)) \/ (~((~(S (bpr_index_pc_prim_weight_factors) = 1) /\ forall bpr_left_pc_prim_weight_factors_choice_prime bpr_right_pc_prim_weight_factors_choice_prime. S (bpr_index_pc_prim_weight_factors) = bpr_left_pc_prim_weight_factors_choice_prime * bpr_right_pc_prim_weight_factors_choice_prime -> bpr_left_pc_prim_weight_factors_choice_prime = 1 \/ bpr_right_pc_prim_weight_factors_choice_prime = 1)) /\ bpr_value_pc_prim_weight_factors = 1))))) -> (forall pc_index_prim_weight_mask. (exists pc_lt_prim_weight_mask_bound. pc_lt_prim_weight_mask_bound + S (pc_index_prim_weight_mask) = (l)) -> exists pc_bit_prim_weight_mask. (((exists fs_h_pc_prim_weight_mask_entry. fs_h_pc_prim_weight_mask_entry + S (pc_bit_prim_weight_mask) = S ((S (pc_index_prim_weight_mask)) * f)) /\ exists fs_q_pc_prim_weight_mask_entry. d = fs_q_pc_prim_weight_mask_entry * S ((S (pc_index_prim_weight_mask)) * f) + (pc_bit_prim_weight_mask))) /\ (((((~(S (pc_index_prim_weight_mask) = 1) /\ forall bpr_left_pc_prim_weight_mask_choice_prime bpr_right_pc_prim_weight_mask_choice_prime. S (pc_index_prim_weight_mask) = bpr_left_pc_prim_weight_mask_choice_prime * bpr_right_pc_prim_weight_mask_choice_prime -> bpr_left_pc_prim_weight_mask_choice_prime = 1 \/ bpr_right_pc_prim_weight_mask_choice_prime = 1)) /\ pc_bit_prim_weight_mask = 1) \/ (~((~(S (pc_index_prim_weight_mask) = 1) /\ forall bpr_left_pc_prim_weight_mask_choice_prime bpr_right_pc_prim_weight_mask_choice_prime. S (pc_index_prim_weight_mask) = bpr_left_pc_prim_weight_mask_choice_prime * bpr_right_pc_prim_weight_mask_choice_prime -> bpr_left_pc_prim_weight_mask_choice_prime = 1 \/ bpr_right_pc_prim_weight_mask_choice_prime = 1)) /\ pc_bit_prim_weight_mask = 0)))) -> (forall pc_index_prim_weight_cutoff. (exists pc_lt_prim_weight_cutoff_bound. pc_lt_prim_weight_cutoff_bound + S (pc_index_prim_weight_cutoff) = (l)) -> exists pc_bit_prim_weight_cutoff. (((exists fs_h_pc_prim_weight_cutoff_entry. fs_h_pc_prim_weight_cutoff_entry + S (pc_bit_prim_weight_cutoff) = S ((S (pc_index_prim_weight_cutoff)) * h)) /\ exists fs_q_pc_prim_weight_cutoff_entry. g = fs_q_pc_prim_weight_cutoff_entry * S ((S (pc_index_prim_weight_cutoff)) * h) + (pc_bit_prim_weight_cutoff))) /\ ((((exists pc_lt_prim_weight_cutoff_choice_below. pc_lt_prim_weight_cutoff_choice_below + S (pc_index_prim_weight_cutoff) = (u)) /\ pc_bit_prim_weight_cutoff = 0) \/ ((exists pc_le_prim_weight_cutoff_choice_above. pc_le_prim_weight_cutoff_choice_above + (u) = (pc_index_prim_weight_cutoff)) /\ (((exists fs_h_pc_prim_weight_cutoff_choice_source. fs_h_pc_prim_weight_cutoff_choice_source + S (pc_bit_prim_weight_cutoff) = S ((S (pc_index_prim_weight_cutoff)) * f)) /\ exists fs_q_pc_prim_weight_cutoff_choice_source. d = fs_q_pc_prim_weight_cutoff_choice_source * S ((S (pc_index_prim_weight_cutoff)) * f) + (pc_bit_prim_weight_cutoff))))))) -> (forall pc_index_prim_weight_result pc_factor_prim_weight_result pc_bit_prim_weight_result. (exists pc_lt_prim_weight_result_index. pc_lt_prim_weight_result_index + S (pc_index_prim_weight_result) = (l)) -> (((exists fs_h_pc_prim_weight_result_factor. fs_h_pc_prim_weight_result_factor + S (pc_factor_prim_weight_result) = S ((S (pc_index_prim_weight_result)) * c)) /\ exists fs_q_pc_prim_weight_result_factor. b = fs_q_pc_prim_weight_result_factor * S ((S (pc_index_prim_weight_result)) * c) + (pc_factor_prim_weight_result))) -> (((exists fs_h_pc_prim_weight_result_bit. fs_h_pc_prim_weight_result_bit + S (pc_bit_prim_weight_result) = S ((S (pc_index_prim_weight_result)) * h)) /\ exists fs_q_pc_prim_weight_result_bit. g = fs_q_pc_prim_weight_result_bit * S ((S (pc_index_prim_weight_result)) * h) + (pc_bit_prim_weight_result))) -> ((pc_bit_prim_weight_result = 0 /\ (exists pc_le_prim_weight_result_zero. pc_le_prim_weight_result_zero + (1) = (pc_factor_prim_weight_result))) \/ (pc_bit_prim_weight_result = 1 /\ (exists pc_le_prim_weight_result_one. pc_le_prim_weight_result_one + (u) = (pc_factor_prim_weight_result)))))

Complete tactic proof in conservative notation

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

83 script commands · 19 reading checkpoints · 4 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 (4)
primorial prefix decoded choiceprimorial factor choice one lebeta cutoff prefix entryprime bit prefix entry
01Fix variables and assumptionsL1–10

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

  1. L1
    intro u
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro d
  5. L5
    intro f
  6. L6
    intro g
  7. L7
    intro h
  8. L8
    intro l
  9. L9
    intro hf
  10. L10
    intro hm
02Fix variables and assumptionsL11–17

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

  1. L11
    intro hc
  2. L12
    intro i
  3. L13
    intro a
  4. L14
    intro e
  5. L15
    intro hi
  6. L16
    intro ha
  7. L17
    intro he
03Establish hvL18–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply primorial prefix decoded choice.

  1. L18
    have hv : Prime(S i) ∧ a = S i ∨ ¬Prime(S i) ∧ a = 1Definitions: Prime(S i)Original native command in the exact edition
  2. L19
    specialize primorial_prefix_decoded_choice b
  3. L20
    specialize primorial_prefix_decoded_choice c
  4. L21
    specialize primorial_prefix_decoded_choice l
  5. L22
    specialize primorial_prefix_decoded_choice i
  6. L23
    specialize primorial_prefix_decoded_choice a
  7. L24
    apply primorial_prefix_decoded_choice
  8. L25
    exact hf
  9. L26
    exact hi
  10. L27
    exact ha
04Establish hpositiveL28–32

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

  1. L28
    have hpositive : Lt(0,a)Definitions: Lt(0,a)Original native command in the exact edition
  2. L29
    specialize primorial_factor_choice_one_le i
  3. L30
    specialize primorial_factor_choice_one_le a
  4. L31
    apply primorial_factor_choice_one_le
  5. L32
    exact hv
05Establish hcutL33–42

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

  1. L33
    have hcut : Lt(i,u) ∧ e = 0 ∨ Le(u,i) ∧ BetaAt(d,f,i,e)Definitions: Lt(i,u)Le(u,i)BetaAt(d,f,i,e)Original native command in the exact edition
  2. L34
    specialize beta_cutoff_prefix_entry u
  3. L35
    specialize beta_cutoff_prefix_entry d
  4. L36
    specialize beta_cutoff_prefix_entry f
  5. L37
    specialize beta_cutoff_prefix_entry g
  6. L38
    specialize beta_cutoff_prefix_entry h
  7. L39
    specialize beta_cutoff_prefix_entry l
  8. L40
    specialize beta_cutoff_prefix_entry i
  9. L41
    specialize beta_cutoff_prefix_entry e
  10. L42
    apply beta_cutoff_prefix_entry
06Use earlier factsL43–45

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

  1. L43
    exact hc
  2. L44
    exact hi
  3. L45
    exact he
07Separate the logical casesL46–49

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

  1. L46
    cases hcut
  2. L47
    cases hcut_left
  3. L48
    left
  4. L49
    split
08Use earlier factsL50–51

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

  1. L50
    exact hcut_left_right
  2. L51
    exact hpositive
09Separate the logical casesL52–52

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

  1. L52
    cases hcut_right
10Establish hbL53–62

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime bit prefix entry.

  1. L53
    have hb : Prime(S i) ∧ e = 1 ∨ ¬Prime(S i) ∧ e = 0Definitions: Prime(S i)Original native command in the exact edition
  2. L54
    specialize prime_bit_prefix_entry d
  3. L55
    specialize prime_bit_prefix_entry f
  4. L56
    specialize prime_bit_prefix_entry l
  5. L57
    specialize prime_bit_prefix_entry i
  6. L58
    specialize prime_bit_prefix_entry e
  7. L59
    apply prime_bit_prefix_entry
  8. L60
    exact hm
  9. L61
    exact hi
  10. L62
    exact hcut_right_right
11Separate the logical casesL63–66

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

  1. L63
    cases hb
  2. L64
    cases hb_left
  3. L65
    right
  4. L66
    split
12Use earlier factsL67–67

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

  1. L67
    exact hb_left_right
13Separate the logical casesL68–69

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

  1. L68
    cases hv
  2. L69
    cases hv_left
14Calculate and transport equalitiesL70–70

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

  1. L70
    rewrite hv_left_right
15Use earlier factsL71–74

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

  1. L71
    specialize le_succ u
  2. L72
    specialize le_succ i
  3. L73
    apply le_succ
  4. L74
    exact hcut_right_left
16Separate the logical casesL75–76

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

  1. L75
    cases hv_right
  2. L76
    exfalso
17Use earlier factsL77–78

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

  1. L77
    apply hv_right_left
  2. L78
    exact hb_left_left
18Separate the logical casesL79–81

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

  1. L79
    cases hb_right
  2. L80
    left
  3. L81
    split
19Use earlier factsL82–83

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

  1. L82
    exact hb_right_right
  2. L83
    exact hpositive

Library-wide reading audit

Original defined command ledger · 83 lines
  1. 0001intro u
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro f
  6. 0006intro g
  7. 0007intro h
  8. 0008intro l
  9. 0009intro hf
  10. 0010intro hm
  11. 0011intro hc
  12. 0012intro i
  13. 0013intro a
  14. 0014intro e
  15. 0015intro hi
  16. 0016intro ha
  17. 0017intro he
  18. 0018have hv : Prime(S i) ∧ a = S i ∨ ¬Prime(S i) ∧ a = 1
  19. 0019specialize primorial_prefix_decoded_choice b
  20. 0020specialize primorial_prefix_decoded_choice c
  21. 0021specialize primorial_prefix_decoded_choice l
  22. 0022specialize primorial_prefix_decoded_choice i
  23. 0023specialize primorial_prefix_decoded_choice a
  24. 0024apply primorial_prefix_decoded_choice
  25. 0025exact hf
  26. 0026exact hi
  27. 0027exact ha
  28. 0028have hpositive : Lt(0,a)
  29. 0029specialize primorial_factor_choice_one_le i
  30. 0030specialize primorial_factor_choice_one_le a
  31. 0031apply primorial_factor_choice_one_le
  32. 0032exact hv
  33. 0033have hcut : Lt(i,u) ∧ e = 0 ∨ Le(u,i) ∧ BetaAt(d,f,i,e)
  34. 0034specialize beta_cutoff_prefix_entry u
  35. 0035specialize beta_cutoff_prefix_entry d
  36. 0036specialize beta_cutoff_prefix_entry f
  37. 0037specialize beta_cutoff_prefix_entry g
  38. 0038specialize beta_cutoff_prefix_entry h
  39. 0039specialize beta_cutoff_prefix_entry l
  40. 0040specialize beta_cutoff_prefix_entry i
  41. 0041specialize beta_cutoff_prefix_entry e
  42. 0042apply beta_cutoff_prefix_entry
  43. 0043exact hc
  44. 0044exact hi
  45. 0045exact he
  46. 0046cases hcut
  47. 0047cases hcut_left
  48. 0048left
  49. 0049split
  50. 0050exact hcut_left_right
  51. 0051exact hpositive
  52. 0052cases hcut_right
  53. 0053have hb : Prime(S i) ∧ e = 1 ∨ ¬Prime(S i) ∧ e = 0
  54. 0054specialize prime_bit_prefix_entry d
  55. 0055specialize prime_bit_prefix_entry f
  56. 0056specialize prime_bit_prefix_entry l
  57. 0057specialize prime_bit_prefix_entry i
  58. 0058specialize prime_bit_prefix_entry e
  59. 0059apply prime_bit_prefix_entry
  60. 0060exact hm
  61. 0061exact hi
  62. 0062exact hcut_right_right
  63. 0063cases hb
  64. 0064cases hb_left
  65. 0065right
  66. 0066split
  67. 0067exact hb_left_right
  68. 0068cases hv
  69. 0069cases hv_left
  70. 0070rewrite hv_left_right
  71. 0071specialize le_succ u
  72. 0072specialize le_succ i
  73. 0073apply le_succ
  74. 0074exact hcut_right_left
  75. 0075cases hv_right
  76. 0076exfalso
  77. 0077apply hv_right_left
  78. 0078exact hb_left_left
  79. 0079cases hb_right
  80. 0080left
  81. 0081split
  82. 0082exact hb_right_right
  83. 0083exact hpositive