PC0011

beta_cutoff_prefix_entry

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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 first-order arithmetic 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))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 1 declared prerequisite and contains 30 exact native proof lines.

Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

beta_at_unique Stable theorem; checked-use authorized

Direct dependents

PC0014 beta_cutoff_count_comparison PC001E primorial_cutoff_weighted_lower

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 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: LeLtBetaAt
  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 exact 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 : exists a. (((exists fs_h_pc_cut_entry_actual. fs_h_pc_cut_entry_actual + S (a) = S ((S (i)) * f)) /\ exists fs_q_pc_cut_entry_actual. d = fs_q_pc_cut_entry_actual * S ((S (i)) * f) + (a))) /\ ((((exists pc_lt_cut_entry_actual_choice_below. pc_lt_cut_entry_actual_choice_below + S (i) = (u)) /\ a = 0) \/ ((exists pc_le_cut_entry_actual_choice_above. pc_le_cut_entry_actual_choice_above + (u) = (i)) /\ (((exists fs_h_pc_cut_entry_actual_choice_source. fs_h_pc_cut_entry_actual_choice_source + S (a) = S ((S (i)) * c)) /\ exists fs_q_pc_cut_entry_actual_choice_source. b = fs_q_pc_cut_entry_actual_choice_source * S ((S (i)) * c) + (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