BT00SF · Bertrand theorem

eisenstein_initial_segment_prefix_exists

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

Every threshold and finite length has an exact beta-coded indicator.

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

∀ q. ∀ k. ∃ x. ∃ y. ∀ z. Lt(z,k) → ∃ n. BetaAt(x,y,z,n) ∧ (n = 1 ∧ Lt(z,q) ∨ n = 0 ∧ Lt(q,S z))

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 PD0013 BetaAt

4 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

10 occurrences

Exact expanded native-PA statement
forall q k. (exists b c. (forall eis_index_initial_segment_exists_result. (exists eis_lt_gap_initial_segment_exists_result_bound. eis_lt_gap_initial_segment_exists_result_bound + S (eis_index_initial_segment_exists_result) = k) -> exists eis_bit_initial_segment_exists_result. ((((exists ff_h_eis_initial_segment_exists_result_decoded. ff_h_eis_initial_segment_exists_result_decoded + S (eis_bit_initial_segment_exists_result) = S ((S (eis_index_initial_segment_exists_result)) * c)) /\ exists ff_q_eis_initial_segment_exists_result_decoded. b = ff_q_eis_initial_segment_exists_result_decoded * S ((S (eis_index_initial_segment_exists_result)) * c) + (eis_bit_initial_segment_exists_result))) /\ (((eis_bit_initial_segment_exists_result = 1 /\ (exists eis_le_gap_initial_segment_exists_result_choice_inside. eis_le_gap_initial_segment_exists_result_choice_inside + (S eis_index_initial_segment_exists_result) = q)) \/ (eis_bit_initial_segment_exists_result = 0 /\ (exists eis_lt_gap_initial_segment_exists_result_choice_outside. eis_lt_gap_initial_segment_exists_result_choice_outside + S (q) = S eis_index_initial_segment_exists_result)))))))

Proof neighborhood

Direct theorem prerequisites

BT000L add_eq_zero_right BT000C succ_ne_zero BT00SD eisenstein_initial_segment_indicator_choice BT00SE eisenstein_initial_segment_prefix_extend

Direct theorem dependents

BT00SU initial_segment_prefix_sum_exists

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

33 script commands · 10 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)
add eq zero rightsucc ne zeroeisenstein initial segment indicator choiceeisenstein initial segment prefix extend
01Fix variables and assumptionsL1–1

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

  1. L1
    intro q
02Induction on kL2–2

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction k
03Construct an explicit witnessL3–4

Supply the displayed value, then prove that it has the required property.

  1. L3
    exists 0
  2. L4
    exists 0
04Fix variables and assumptionsL5–6

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

  1. L5
    intro j
  2. L6
    intro hj
05Separate the logical casesL7–8

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

  1. L7
    exfalso
  2. L8
    cases hj
06Establish hsjL9–16

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

  1. L9
    have hsj : S j = 0
  2. L10
    specialize add_eq_zero_right x
  3. L11
    specialize add_eq_zero_right (S j)
  4. L12
    apply add_eq_zero_right
  5. L13
    exact hj_witness
  6. L14
    specialize succ_ne_zero j
  7. L15
    apply succ_ne_zero
  8. L16
    exact hsj
07Establish hpreviousL17–18

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

  1. L17
    have hprevious : ∃ b. ∃ c. ∀ x. Lt(x,k) → ∃ y. BetaAt(b,c,x,y) ∧ (y = 1 ∧ Lt(x,q) ∨ y = 0 ∧ Lt(q,S x))Definitions: Lt(x,k)BetaAt(b,c,x,y)Lt(x,q)Lt(q,S x)Original native command in the exact edition
  2. L18
    exact IH
08Separate the logical casesL19–20

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

  1. L19
    cases hprevious
  2. L20
    cases hprevious_witness
09Establish hlastL21–24

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

  1. L21
    have hlast : ∃ bit. bit = 1 ∧ Lt(k,q) ∨ bit = 0 ∧ Lt(q,S k)Definitions: Lt(k,q)Lt(q,S k)Original native command in the exact edition
  2. L22
    specialize eisenstein_initial_segment_indicator_choice q
  3. L23
    specialize eisenstein_initial_segment_indicator_choice k
  4. L24
    exact eisenstein_initial_segment_indicator_choice
10Establish hnextL25–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein initial segment prefix extend.

  1. L25
    have hnext : ∃ b. ∃ c. ∀ x. Lt(x,S k) → ∃ y. BetaAt(b,c,x,y) ∧ (y = 1 ∧ Lt(x,q) ∨ y = 0 ∧ Lt(q,S x))Definitions: Lt(x,S k)BetaAt(b,c,x,y)Lt(x,q)Lt(q,S x)Original native command in the exact edition
  2. L26
    specialize eisenstein_initial_segment_prefix_extend q
  3. L27
    specialize eisenstein_initial_segment_prefix_extend x
  4. L28
    specialize eisenstein_initial_segment_prefix_extend x1
  5. L29
    specialize eisenstein_initial_segment_prefix_extend k
  6. L30
    apply eisenstein_initial_segment_prefix_extend
  7. L31
    exact hprevious_witness_witness
  8. L32
    exact hlast
  9. L33
    exact hnext

Library-wide reading audit

Original defined command ledger · 33 lines
  1. 0001intro q
  2. 0002induction k
  3. 0003exists 0
  4. 0004exists 0
  5. 0005intro j
  6. 0006intro hj
  7. 0007exfalso
  8. 0008cases hj
  9. 0009have hsj : S j = 0
  10. 0010specialize add_eq_zero_right x
  11. 0011specialize add_eq_zero_right (S j)
  12. 0012apply add_eq_zero_right
  13. 0013exact hj_witness
  14. 0014specialize succ_ne_zero j
  15. 0015apply succ_ne_zero
  16. 0016exact hsj
  17. 0017have hprevious : ∃ b. ∃ c. ∀ x. Lt(x,k) → ∃ y. BetaAt(b,c,x,y) ∧ (y = 1 ∧ Lt(x,q) ∨ y = 0 ∧ Lt(q,S x))
    Exact native replay linehave hprevious : exists b c. (forall eis_index_initial_segment_exists_previous. (exists eis_lt_gap_initial_segment_exists_previous_bound. eis_lt_gap_initial_segment_exists_previous_bound + S (eis_index_initial_segment_exists_previous) = k) -> exists eis_bit_initial_segment_exists_previous. ((((exists ff_h_eis_initial_segment_exists_previous_decoded. ff_h_eis_initial_segment_exists_previous_decoded + S (eis_bit_initial_segment_exists_previous) = S ((S (eis_index_initial_segment_exists_previous)) * c)) /\ exists ff_q_eis_initial_segment_exists_previous_decoded. b = ff_q_eis_initial_segment_exists_previous_decoded * S ((S (eis_index_initial_segment_exists_previous)) * c) + (eis_bit_initial_segment_exists_previous))) /\ (((eis_bit_initial_segment_exists_previous = 1 /\ (exists eis_le_gap_initial_segment_exists_previous_choice_inside. eis_le_gap_initial_segment_exists_previous_choice_inside + (S eis_index_initial_segment_exists_previous) = q)) \/ (eis_bit_initial_segment_exists_previous = 0 /\ (exists eis_lt_gap_initial_segment_exists_previous_choice_outside. eis_lt_gap_initial_segment_exists_previous_choice_outside + S (q) = S eis_index_initial_segment_exists_previous))))))
  18. 0018exact IH
  19. 0019cases hprevious
  20. 0020cases hprevious_witness
  21. 0021have hlast : ∃ bit. bit = 1 ∧ Lt(k,q) ∨ bit = 0 ∧ Lt(q,S k)
    Exact native replay linehave hlast : exists bit. (((bit = 1 /\ (exists eis_le_gap_initial_segment_exists_last_inside. eis_le_gap_initial_segment_exists_last_inside + (S k) = q)) \/ (bit = 0 /\ (exists eis_lt_gap_initial_segment_exists_last_outside. eis_lt_gap_initial_segment_exists_last_outside + S (q) = S k))))
  22. 0022specialize eisenstein_initial_segment_indicator_choice q
  23. 0023specialize eisenstein_initial_segment_indicator_choice k
  24. 0024exact eisenstein_initial_segment_indicator_choice
  25. 0025have hnext : ∃ b. ∃ c. ∀ x. Lt(x,S k) → ∃ y. BetaAt(b,c,x,y) ∧ (y = 1 ∧ Lt(x,q) ∨ y = 0 ∧ Lt(q,S x))
    Exact native replay linehave hnext : exists b c. (forall eis_index_initial_segment_exists_successor. (exists eis_lt_gap_initial_segment_exists_successor_bound. eis_lt_gap_initial_segment_exists_successor_bound + S (eis_index_initial_segment_exists_successor) = S k) -> exists eis_bit_initial_segment_exists_successor. ((((exists ff_h_eis_initial_segment_exists_successor_decoded. ff_h_eis_initial_segment_exists_successor_decoded + S (eis_bit_initial_segment_exists_successor) = S ((S (eis_index_initial_segment_exists_successor)) * c)) /\ exists ff_q_eis_initial_segment_exists_successor_decoded. b = ff_q_eis_initial_segment_exists_successor_decoded * S ((S (eis_index_initial_segment_exists_successor)) * c) + (eis_bit_initial_segment_exists_successor))) /\ (((eis_bit_initial_segment_exists_successor = 1 /\ (exists eis_le_gap_initial_segment_exists_successor_choice_inside. eis_le_gap_initial_segment_exists_successor_choice_inside + (S eis_index_initial_segment_exists_successor) = q)) \/ (eis_bit_initial_segment_exists_successor = 0 /\ (exists eis_lt_gap_initial_segment_exists_successor_choice_outside. eis_lt_gap_initial_segment_exists_successor_choice_outside + S (q) = S eis_index_initial_segment_exists_successor))))))
  26. 0026specialize eisenstein_initial_segment_prefix_extend q
  27. 0027specialize eisenstein_initial_segment_prefix_extend x
  28. 0028specialize eisenstein_initial_segment_prefix_extend x1
  29. 0029specialize eisenstein_initial_segment_prefix_extend k
  30. 0030apply eisenstein_initial_segment_prefix_extend
  31. 0031exact hprevious_witness_witness
  32. 0032exact hlast
  33. 0033exact hnext