BT00UW

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.

Exact expanded 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)))

Structural proof guide

Align a full Primorial mask with an independent offset interval.

Direct prerequisites: add_le_add_left, beta_at_unique, primorial_factor_choice_functional. The authored body proceeds by case analysis (4), intermediate claims (8), equality transport (3).

Proof neighborhood

Direct dependencies

BT0015 add_le_add_left BT0042 beta_at_unique BT00U6 primorial_factor_choice_functional

Direct dependents

BT00UY primorial_prefix_interval_split

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

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.

Named ingredients (3)
add le add leftbeta at uniqueprimorial factor choice functional

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–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 : exists bpr_gap_bpifps_shifted_bound. bpr_gap_bpifps_shifted_bound + (a + S i) = a + l
  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 : exists bpr_gap_bpifps_source_bound. bpr_gap_bpifps_source_bound + S (a + i) = a + l
  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: PrimeBetaAt
  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: PrimeBetaAt
  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 exact 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 : 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 : 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 : 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 : 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