PC0011

beta_cutoff_prefix_entry

Every decoded cutoff entry obeys its actual below/above-threshold choice.

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. ∀ l. ∀ i. ∀ e. BetaCutoffPrefix(u,b,c,d,f,l) → Lt(i,l) → BetaAt(d,f,i,e) → Lt(i,u) ∧ e = 0 ∨ Le(u,i) ∧ BetaAt(b,c,i,e)

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

Definition DAG

BetaCutoffPrefix(u,b,c,d,f,l) · 1Le(a,b) · 2Lt(a,b) · 3BetaAt(b,c,i,x) · 4

Actual proof prerequisites

beta_at_unique · checked external prerequisite
Original expanded first-order statement 
forall u b c d f l i e. (forall pc_index_cut_entry_source. (exists pc_lt_cut_entry_source_bound. pc_lt_cut_entry_source_bound + S (pc_index_cut_entry_source) = (l)) -> exists pc_bit_cut_entry_source. (((exists fs_h_pc_cut_entry_source_entry. fs_h_pc_cut_entry_source_entry + S (pc_bit_cut_entry_source) = S ((S (pc_index_cut_entry_source)) * f)) /\ exists fs_q_pc_cut_entry_source_entry. d = fs_q_pc_cut_entry_source_entry * S ((S (pc_index_cut_entry_source)) * f) + (pc_bit_cut_entry_source))) /\ ((((exists pc_lt_cut_entry_source_choice_below. pc_lt_cut_entry_source_choice_below + S (pc_index_cut_entry_source) = (u)) /\ pc_bit_cut_entry_source = 0) \/ ((exists pc_le_cut_entry_source_choice_above. pc_le_cut_entry_source_choice_above + (u) = (pc_index_cut_entry_source)) /\ (((exists fs_h_pc_cut_entry_source_choice_source. fs_h_pc_cut_entry_source_choice_source + S (pc_bit_cut_entry_source) = S ((S (pc_index_cut_entry_source)) * c)) /\ exists fs_q_pc_cut_entry_source_choice_source. b = fs_q_pc_cut_entry_source_choice_source * S ((S (pc_index_cut_entry_source)) * c) + (pc_bit_cut_entry_source))))))) -> (exists pc_lt_cut_entry_bound. pc_lt_cut_entry_bound + S (i) = (l)) -> (((exists fs_h_pc_cut_entry_given. fs_h_pc_cut_entry_given + S (e) = S ((S (i)) * f)) /\ exists fs_q_pc_cut_entry_given. d = fs_q_pc_cut_entry_given * S ((S (i)) * f) + (e))) -> ((((exists pc_lt_cut_entry_choice_below. pc_lt_cut_entry_choice_below + S (i) = (u)) /\ e = 0) \/ ((exists pc_le_cut_entry_choice_above. pc_le_cut_entry_choice_above + (u) = (i)) /\ (((exists fs_h_pc_cut_entry_choice_source. fs_h_pc_cut_entry_choice_source + S (e) = S ((S (i)) * c)) /\ exists fs_q_pc_cut_entry_choice_source. b = fs_q_pc_cut_entry_choice_source * S ((S (i)) * c) + (e))))))

Complete tactic proof in conservative notation

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

30 script commands · 7 reading checkpoints · 2 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.

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 l
  7. L7
    intro i
  8. L8
    intro e
  9. L9
    intro h
  10. L10
    intro hi
02Fix variables and assumptionsL11–11

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

  1. L11
    intro he
03Establish hpL12–15

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

  1. L12
    have hp : ∃ a. BetaAt(d,f,i,a) ∧ (Lt(i,u) ∧ a = 0 ∨ Le(u,i) ∧ BetaAt(b,c,i,a))Definitions: BetaAt(d,f,i,a)Lt(i,u)Le(u,i)BetaAt(b,c,i,a)Original native command in the exact edition
  2. L13
    specialize h i
  3. L14
    apply h
  4. L15
    exact hi
04Separate the logical casesL16–17

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

  1. L16
    cases hp
  2. L17
    cases hp_witness
05Establish heqL18–27

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

  1. L18
    have heq : x = e
  2. L19
    specialize beta_at_unique d
  3. L20
    specialize beta_at_unique f
  4. L21
    specialize beta_at_unique i
  5. L22
    specialize beta_at_unique x
  6. L23
    specialize beta_at_unique e
  7. L24
    apply beta_at_unique
  8. L25
    exact hp_witness_left
  9. L26
    exact he
  10. L27
    rewrite heq at hp_witness_right
06Calculate and transport equalitiesL28–29

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

  1. L28
    rewrite heq at hp_witness_right
  2. L29
    rewrite heq at hp_witness_right
07Use earlier factsL30–30

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

  1. L30
    exact hp_witness_right

Library-wide reading audit

Original defined command ledger · 30 lines
  1. 0001intro u
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro f
  6. 0006intro l
  7. 0007intro i
  8. 0008intro e
  9. 0009intro h
  10. 0010intro hi
  11. 0011intro he
  12. 0012have hp : ∃ a. BetaAt(d,f,i,a) ∧ (Lt(i,u) ∧ a = 0 ∨ Le(u,i) ∧ BetaAt(b,c,i,a))
  13. 0013specialize h i
  14. 0014apply h
  15. 0015exact hi
  16. 0016cases hp
  17. 0017cases hp_witness
  18. 0018have heq : x = e
  19. 0019specialize beta_at_unique d
  20. 0020specialize beta_at_unique f
  21. 0021specialize beta_at_unique i
  22. 0022specialize beta_at_unique x
  23. 0023specialize beta_at_unique e
  24. 0024apply beta_at_unique
  25. 0025exact hp_witness_left
  26. 0026exact he
  27. 0027rewrite heq at hp_witness_right
  28. 0028rewrite heq at hp_witness_right
  29. 0029rewrite heq at hp_witness_right
  30. 0030exact hp_witness_right