BT00UW · Bertrand theorem

primorial_interval_factor_prefix_shift

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

Align a full Primorial mask with an independent offset interval.

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.

Statement with defined notation

∀ a. ∀ b. ∀ c. ∀ d. ∀ e. ∀ l. (∀ x. Lt(x,a + l) → ∃ y. BetaAt(b,c,x,y) ∧ (Prime(S x) ∧ y = S x ∨ ¬Prime(S x) ∧ y = 1)) → (∀ x. Lt(x,l) → ∃ y. BetaAt(d,e,x,y) ∧ (Prime(S (a + x)) ∧ y = S (a + x) ∨ ¬Prime(S (a + x)) ∧ y = 1)) → ∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,a + x,y) → BetaAt(d,e,x,y)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0004 Prime PD0013 BetaAt

11 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0004 Prime PD0013 BetaAt

8 occurrences

Exact expanded native-PA statement
forall a b c d e l. (forall bpr_index_bpifps_source. (exists bpr_gap_bpifps_source_bound. bpr_gap_bpifps_source_bound + S (bpr_index_bpifps_source) = a + l) -> exists bpr_value_bpifps_source. ((((exists bpr_height_bpifps_source_decoded. bpr_height_bpifps_source_decoded + S (bpr_value_bpifps_source) = S ((S (bpr_index_bpifps_source)) * c)) /\ exists bpr_quotient_bpifps_source_decoded. b = bpr_quotient_bpifps_source_decoded * S ((S (bpr_index_bpifps_source)) * c) + (bpr_value_bpifps_source))) /\ (((((~(S (bpr_index_bpifps_source) = 1) /\ forall bpr_left_bpifps_source_choice_prime bpr_right_bpifps_source_choice_prime. S (bpr_index_bpifps_source) = bpr_left_bpifps_source_choice_prime * bpr_right_bpifps_source_choice_prime -> bpr_left_bpifps_source_choice_prime = 1 \/ bpr_right_bpifps_source_choice_prime = 1)) /\ bpr_value_bpifps_source = S (bpr_index_bpifps_source)) \/ (~((~(S (bpr_index_bpifps_source) = 1) /\ forall bpr_left_bpifps_source_choice_prime bpr_right_bpifps_source_choice_prime. S (bpr_index_bpifps_source) = bpr_left_bpifps_source_choice_prime * bpr_right_bpifps_source_choice_prime -> bpr_left_bpifps_source_choice_prime = 1 \/ bpr_right_bpifps_source_choice_prime = 1)) /\ bpr_value_bpifps_source = 1))))) -> (forall bpr_index_bpifps_interval. (exists bpr_gap_bpifps_interval_bound. bpr_gap_bpifps_interval_bound + S (bpr_index_bpifps_interval) = l) -> exists bpr_value_bpifps_interval. ((((exists bpr_height_bpifps_interval_decoded. bpr_height_bpifps_interval_decoded + S (bpr_value_bpifps_interval) = S ((S (bpr_index_bpifps_interval)) * e)) /\ exists bpr_quotient_bpifps_interval_decoded. d = bpr_quotient_bpifps_interval_decoded * S ((S (bpr_index_bpifps_interval)) * e) + (bpr_value_bpifps_interval))) /\ (((((~(S (a + bpr_index_bpifps_interval) = 1) /\ forall bpr_left_bpifps_interval_choice_prime bpr_right_bpifps_interval_choice_prime. S (a + bpr_index_bpifps_interval) = bpr_left_bpifps_interval_choice_prime * bpr_right_bpifps_interval_choice_prime -> bpr_left_bpifps_interval_choice_prime = 1 \/ bpr_right_bpifps_interval_choice_prime = 1)) /\ bpr_value_bpifps_interval = S (a + bpr_index_bpifps_interval)) \/ (~((~(S (a + bpr_index_bpifps_interval) = 1) /\ forall bpr_left_bpifps_interval_choice_prime bpr_right_bpifps_interval_choice_prime. S (a + bpr_index_bpifps_interval) = bpr_left_bpifps_interval_choice_prime * bpr_right_bpifps_interval_choice_prime -> bpr_left_bpifps_interval_choice_prime = 1 \/ bpr_right_bpifps_interval_choice_prime = 1)) /\ bpr_value_bpifps_interval = 1))))) -> forall i p. (exists bpr_gap_bpifps_bound. bpr_gap_bpifps_bound + S (i) = l) -> (((exists bpr_height_bpifps_source_entry. bpr_height_bpifps_source_entry + S (p) = S ((S (a + i)) * c)) /\ exists bpr_quotient_bpifps_source_entry. b = bpr_quotient_bpifps_source_entry * S ((S (a + i)) * c) + (p))) -> (((exists bpr_height_bpifps_target_entry. bpr_height_bpifps_target_entry + S (p) = S ((S (i)) * e)) /\ exists bpr_quotient_bpifps_target_entry. d = bpr_quotient_bpifps_target_entry * S ((S (i)) * e) + (p)))

Proof neighborhood

Direct theorem prerequisites

BT0015 add_le_add_left BT0042 beta_at_unique BT00U6 primorial_factor_choice_functional

Direct theorem dependents

BT00UY primorial_prefix_interval_split

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

48 script commands · 12 reading checkpoints · 8 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 (3)
add le add leftbeta at uniqueprimorial factor choice functional
01Fix variables and assumptionsL1–10

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro d
  5. L5
    intro e
  6. L6
    intro l
  7. L7
    intro hsource
  8. L8
    intro hinterval
  9. L9
    intro i
  10. L10
    intro p
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hi
  2. L12
    intro hp
03Establish hsource_bound_rawL13–18

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

  1. L13
    have hsource_bound_raw : Le(a + S i,a + l)Definitions: Le(a + S i,a + l)Original native command in the exact edition
  2. L14
    specialize add_le_add_left (S i)
  3. L15
    specialize add_le_add_left l
  4. L16
    specialize add_le_add_left a
  5. L17
    apply add_le_add_left
  6. L18
    exact hi
04Establish hadd_succL19–21

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

  1. L19
    have hadd_succ : a + S i = S (a + i)
  2. L20
    apply PA4
  3. L21
    rewrite hadd_succ at hsource_bound_raw
05Establish hsource_boundL22–23

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

  1. L22
    have hsource_bound : Lt(a + i,a + l)Definitions: Lt(a + i,a + l)Original native command in the exact edition
  2. L23
    exact hsource_bound_raw
06Establish hsource_entryL24–26

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

  1. L24
    have hsource_entry : ∃ q. BetaAt(b,c,a + i,q) ∧ (Prime(S (a + i)) ∧ q = S (a + i) ∨ ¬Prime(S (a + i)) ∧ q = 1)Definitions: BetaAt(b,c,a + i,q)Prime(S (a + i))Original native command in the exact edition
  2. L25
    apply hsource
  3. L26
    exact hsource_bound
07Separate the logical casesL27–28

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

  1. L27
    cases hsource_entry
  2. L28
    cases hsource_entry_witness
08Establish hinterval_entryL29–31

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

  1. L29
    have hinterval_entry : ∃ r. BetaAt(d,e,i,r) ∧ (Prime(S (a + i)) ∧ r = S (a + i) ∨ ¬Prime(S (a + i)) ∧ r = 1)Definitions: BetaAt(d,e,i,r)Prime(S (a + i))Original native command in the exact edition
  2. L30
    apply hinterval
  3. L31
    exact hi
09Separate the logical casesL32–33

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

  1. L32
    cases hinterval_entry
  2. L33
    cases hinterval_entry_witness
10Establish hpqL34–37

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

  1. L34
    have hpq : p = x
  2. L35
    apply beta_at_unique
  3. L36
    exact hp
  4. L37
    exact hsource_entry_witness_left
11Establish hqrL38–41

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

  1. L38
    have hqr : x = x1
  2. L39
    apply primorial_factor_choice_functional
  3. L40
    exact hsource_entry_witness_right
  4. L41
    exact hinterval_entry_witness_right
12Establish hprL42–48

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

  1. L42
    have hpr : p = x1
  2. L43
    trans x
  3. L44
    exact hpq
  4. L45
    exact hqr
  5. L46
    rewrite hpr
  6. L47
    rewrite hpr
  7. L48
    exact hinterval_entry_witness_left

Library-wide reading audit

Original defined command ledger · 48 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro e
  6. 0006intro l
  7. 0007intro hsource
  8. 0008intro hinterval
  9. 0009intro i
  10. 0010intro p
  11. 0011intro hi
  12. 0012intro hp
  13. 0013have hsource_bound_raw : Le(a + S i,a + l)
    Exact native replay linehave hsource_bound_raw : exists bpr_gap_bpifps_shifted_bound. bpr_gap_bpifps_shifted_bound + (a + S i) = a + l
  14. 0014specialize add_le_add_left (S i)
  15. 0015specialize add_le_add_left l
  16. 0016specialize add_le_add_left a
  17. 0017apply add_le_add_left
  18. 0018exact hi
  19. 0019have hadd_succ : a + S i = S (a + i)
  20. 0020apply PA4
  21. 0021rewrite hadd_succ at hsource_bound_raw
  22. 0022have hsource_bound : Lt(a + i,a + l)
    Exact native replay linehave hsource_bound : exists bpr_gap_bpifps_source_bound. bpr_gap_bpifps_source_bound + S (a + i) = a + l
  23. 0023exact hsource_bound_raw
  24. 0024have hsource_entry : ∃ q. BetaAt(b,c,a + i,q) ∧ (Prime(S (a + i)) ∧ q = S (a + i) ∨ ¬Prime(S (a + i)) ∧ q = 1)
    Exact native replay linehave hsource_entry : exists q. ((((exists bpr_height_bpifps_source_local. bpr_height_bpifps_source_local + S (q) = S ((S (a + i)) * c)) /\ exists bpr_quotient_bpifps_source_local. b = bpr_quotient_bpifps_source_local * S ((S (a + i)) * c) + (q))) /\ (((((~(S (a + i) = 1) /\ forall bpr_left_bpifps_source_choice_prime bpr_right_bpifps_source_choice_prime. S (a + i) = bpr_left_bpifps_source_choice_prime * bpr_right_bpifps_source_choice_prime -> bpr_left_bpifps_source_choice_prime = 1 \/ bpr_right_bpifps_source_choice_prime = 1)) /\ q = S (a + i)) \/ (~((~(S (a + i) = 1) /\ forall bpr_left_bpifps_source_choice_prime bpr_right_bpifps_source_choice_prime. S (a + i) = bpr_left_bpifps_source_choice_prime * bpr_right_bpifps_source_choice_prime -> bpr_left_bpifps_source_choice_prime = 1 \/ bpr_right_bpifps_source_choice_prime = 1)) /\ q = 1))))
  25. 0025apply hsource
  26. 0026exact hsource_bound
  27. 0027cases hsource_entry
  28. 0028cases hsource_entry_witness
  29. 0029have hinterval_entry : ∃ r. BetaAt(d,e,i,r) ∧ (Prime(S (a + i)) ∧ r = S (a + i) ∨ ¬Prime(S (a + i)) ∧ r = 1)
    Exact native replay linehave hinterval_entry : exists r. ((((exists bpr_height_bpifps_interval_local. bpr_height_bpifps_interval_local + S (r) = S ((S (i)) * e)) /\ exists bpr_quotient_bpifps_interval_local. d = bpr_quotient_bpifps_interval_local * S ((S (i)) * e) + (r))) /\ (((((~(S (a + i) = 1) /\ forall bpr_left_bpifps_interval_choice_prime bpr_right_bpifps_interval_choice_prime. S (a + i) = bpr_left_bpifps_interval_choice_prime * bpr_right_bpifps_interval_choice_prime -> bpr_left_bpifps_interval_choice_prime = 1 \/ bpr_right_bpifps_interval_choice_prime = 1)) /\ r = S (a + i)) \/ (~((~(S (a + i) = 1) /\ forall bpr_left_bpifps_interval_choice_prime bpr_right_bpifps_interval_choice_prime. S (a + i) = bpr_left_bpifps_interval_choice_prime * bpr_right_bpifps_interval_choice_prime -> bpr_left_bpifps_interval_choice_prime = 1 \/ bpr_right_bpifps_interval_choice_prime = 1)) /\ r = 1))))
  30. 0030apply hinterval
  31. 0031exact hi
  32. 0032cases hinterval_entry
  33. 0033cases hinterval_entry_witness
  34. 0034have hpq : p = x
  35. 0035apply beta_at_unique
  36. 0036exact hp
  37. 0037exact hsource_entry_witness_left
  38. 0038have hqr : x = x1
  39. 0039apply primorial_factor_choice_functional
  40. 0040exact hsource_entry_witness_right
  41. 0041exact hinterval_entry_witness_right
  42. 0042have hpr : p = x1
  43. 0043trans x
  44. 0044exact hpq
  45. 0045exact hqr
  46. 0046rewrite hpr
  47. 0047rewrite hpr
  48. 0048exact hinterval_entry_witness_left