BT00SF

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.

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

Structural proof guide

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

Direct prerequisites: add_eq_zero_right, succ_ne_zero, eisenstein_initial_segment_indicator_choice, eisenstein_initial_segment_prefix_extend. The authored body proceeds by structural induction (1), case analysis (3), intermediate claims (4).

Proof neighborhood

Direct dependencies

BT000L add_eq_zero_right BT000C succ_ne_zero BT00SD eisenstein_initial_segment_indicator_choice BT00SE eisenstein_initial_segment_prefix_extend

Direct dependents

BT00SU initial_segment_prefix_sum_exists

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

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.

Named ingredients (4)
add eq zero rightsucc ne zeroeisenstein initial segment indicator choiceeisenstein initial segment prefix extend

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–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: LtBetaAt
  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 : 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))))
  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: LtBetaAt
  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 exact 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 : 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 : 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 : 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