BT00T8 · Bertrand theorem

choose_exists

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

The recurrence-defined Choose relation has a value for every pair.

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

∀ n. ∀ k. ∃ z. Choose(n,k,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

PD0041 Choose

1 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

14 occurrences

Exact expanded native-PA statement
forall n k. exists z. (((exists bcf_lt_gap_bce_result_out_of_range. bcf_lt_gap_bce_result_out_of_range + S (n) = k) /\ z = 0) \/ ((exists bcf_le_gap_bce_result_in_range. bcf_le_gap_bce_result_in_range + (k) = n) /\ (exists bcf_row_code_code_bce_result bcf_row_code_scale_bce_result bcf_row_scale_code_bce_result bcf_row_scale_scale_bce_result bcf_row_code_bce_result bcf_row_scale_bce_result. ((forall bcf_row_index_bce_result_table. (exists bcf_lt_gap_bce_result_table_row_bound. bcf_lt_gap_bce_result_table_row_bound + S (bcf_row_index_bce_result_table) = S (n)) -> exists bcf_row_code_bce_result_table bcf_row_scale_bce_result_table. ((((exists bcf_height_bce_result_table_decoded_row_code. bcf_height_bce_result_table_decoded_row_code + S (bcf_row_code_bce_result_table) = S ((S (bcf_row_index_bce_result_table)) * bcf_row_code_scale_bce_result)) /\ exists bcf_quotient_bce_result_table_decoded_row_code. bcf_row_code_code_bce_result = bcf_quotient_bce_result_table_decoded_row_code * S ((S (bcf_row_index_bce_result_table)) * bcf_row_code_scale_bce_result) + (bcf_row_code_bce_result_table))) /\ ((((exists bcf_height_bce_result_table_decoded_row_scale. bcf_height_bce_result_table_decoded_row_scale + S (bcf_row_scale_bce_result_table) = S ((S (bcf_row_index_bce_result_table)) * bcf_row_scale_scale_bce_result)) /\ exists bcf_quotient_bce_result_table_decoded_row_scale. bcf_row_scale_code_bce_result = bcf_quotient_bce_result_table_decoded_row_scale * S ((S (bcf_row_index_bce_result_table)) * bcf_row_scale_scale_bce_result) + (bcf_row_scale_bce_result_table))) /\ ((bcf_row_index_bce_result_table = 0 /\ (forall bcf_index_bce_result_table_zero_row. (exists bcf_lt_gap_bce_result_table_zero_row_bound. bcf_lt_gap_bce_result_table_zero_row_bound + S (bcf_index_bce_result_table_zero_row) = S (n)) -> exists bcf_value_bce_result_table_zero_row. ((((exists bcf_height_bce_result_table_zero_row_entry. bcf_height_bce_result_table_zero_row_entry + S (bcf_value_bce_result_table_zero_row) = S ((S (bcf_index_bce_result_table_zero_row)) * bcf_row_scale_bce_result_table)) /\ exists bcf_quotient_bce_result_table_zero_row_entry. bcf_row_code_bce_result_table = bcf_quotient_bce_result_table_zero_row_entry * S ((S (bcf_index_bce_result_table_zero_row)) * bcf_row_scale_bce_result_table) + (bcf_value_bce_result_table_zero_row))) /\ ((bcf_index_bce_result_table_zero_row = 0 /\ bcf_value_bce_result_table_zero_row = 1) \/ exists bcf_predecessor_bce_result_table_zero_row. bcf_index_bce_result_table_zero_row = S bcf_predecessor_bce_result_table_zero_row /\ bcf_value_bce_result_table_zero_row = 0)))) \/ exists bcf_predecessor_bce_result_table bcf_previous_code_bce_result_table bcf_previous_scale_bce_result_table. bcf_row_index_bce_result_table = S bcf_predecessor_bce_result_table /\ ((((exists bcf_height_bce_result_table_decoded_previous_code. bcf_height_bce_result_table_decoded_previous_code + S (bcf_previous_code_bce_result_table) = S ((S (bcf_predecessor_bce_result_table)) * bcf_row_code_scale_bce_result)) /\ exists bcf_quotient_bce_result_table_decoded_previous_code. bcf_row_code_code_bce_result = bcf_quotient_bce_result_table_decoded_previous_code * S ((S (bcf_predecessor_bce_result_table)) * bcf_row_code_scale_bce_result) + (bcf_previous_code_bce_result_table))) /\ ((((exists bcf_height_bce_result_table_decoded_previous_scale. bcf_height_bce_result_table_decoded_previous_scale + S (bcf_previous_scale_bce_result_table) = S ((S (bcf_predecessor_bce_result_table)) * bcf_row_scale_scale_bce_result)) /\ exists bcf_quotient_bce_result_table_decoded_previous_scale. bcf_row_scale_code_bce_result = bcf_quotient_bce_result_table_decoded_previous_scale * S ((S (bcf_predecessor_bce_result_table)) * bcf_row_scale_scale_bce_result) + (bcf_previous_scale_bce_result_table))) /\ (forall bcf_index_bce_result_table_row_step. (exists bcf_lt_gap_bce_result_table_row_step_bound. bcf_lt_gap_bce_result_table_row_step_bound + S (bcf_index_bce_result_table_row_step) = S (n)) -> exists bcf_value_bce_result_table_row_step. ((((exists bcf_height_bce_result_table_row_step_entry. bcf_height_bce_result_table_row_step_entry + S (bcf_value_bce_result_table_row_step) = S ((S (bcf_index_bce_result_table_row_step)) * bcf_row_scale_bce_result_table)) /\ exists bcf_quotient_bce_result_table_row_step_entry. bcf_row_code_bce_result_table = bcf_quotient_bce_result_table_row_step_entry * S ((S (bcf_index_bce_result_table_row_step)) * bcf_row_scale_bce_result_table) + (bcf_value_bce_result_table_row_step))) /\ ((bcf_index_bce_result_table_row_step = 0 /\ bcf_value_bce_result_table_row_step = 1) \/ exists bcf_predecessor_bce_result_table_row_step bcf_left_bce_result_table_row_step bcf_right_bce_result_table_row_step. bcf_index_bce_result_table_row_step = S bcf_predecessor_bce_result_table_row_step /\ ((((exists bcf_height_bce_result_table_row_step_previous_left. bcf_height_bce_result_table_row_step_previous_left + S (bcf_left_bce_result_table_row_step) = S ((S (bcf_predecessor_bce_result_table_row_step)) * bcf_previous_scale_bce_result_table)) /\ exists bcf_quotient_bce_result_table_row_step_previous_left. bcf_previous_code_bce_result_table = bcf_quotient_bce_result_table_row_step_previous_left * S ((S (bcf_predecessor_bce_result_table_row_step)) * bcf_previous_scale_bce_result_table) + (bcf_left_bce_result_table_row_step))) /\ ((((exists bcf_height_bce_result_table_row_step_previous_right. bcf_height_bce_result_table_row_step_previous_right + S (bcf_right_bce_result_table_row_step) = S ((S (S (bcf_predecessor_bce_result_table_row_step))) * bcf_previous_scale_bce_result_table)) /\ exists bcf_quotient_bce_result_table_row_step_previous_right. bcf_previous_code_bce_result_table = bcf_quotient_bce_result_table_row_step_previous_right * S ((S (S (bcf_predecessor_bce_result_table_row_step))) * bcf_previous_scale_bce_result_table) + (bcf_right_bce_result_table_row_step))) /\ bcf_value_bce_result_table_row_step = bcf_left_bce_result_table_row_step + bcf_right_bce_result_table_row_step))))))))))) /\ ((((exists bcf_height_bce_result_decoded_row_code. bcf_height_bce_result_decoded_row_code + S (bcf_row_code_bce_result) = S ((S (n)) * bcf_row_code_scale_bce_result)) /\ exists bcf_quotient_bce_result_decoded_row_code. bcf_row_code_code_bce_result = bcf_quotient_bce_result_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bce_result) + (bcf_row_code_bce_result))) /\ ((((exists bcf_height_bce_result_decoded_row_scale. bcf_height_bce_result_decoded_row_scale + S (bcf_row_scale_bce_result) = S ((S (n)) * bcf_row_scale_scale_bce_result)) /\ exists bcf_quotient_bce_result_decoded_row_scale. bcf_row_scale_code_bce_result = bcf_quotient_bce_result_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bce_result) + (bcf_row_scale_bce_result))) /\ (((exists bcf_height_bce_result_decoded_value. bcf_height_bce_result_decoded_value + S (z) = S ((S (k)) * bcf_row_scale_bce_result)) /\ exists bcf_quotient_bce_result_decoded_value. bcf_row_code_bce_result = bcf_quotient_bce_result_decoded_value * S ((S (k)) * bcf_row_scale_bce_result) + (z)))))))))

Proof neighborhood

Direct theorem prerequisites

BT001G le_or_lt BT0041 beta_at_exists BT00T7 beta_pascal_table_prefix_exists

Direct theorem dependents

BT00TL choose_symmetry BT00TM choose_positive BT00TN central_binom_exists BT00TS central_binom_succ_double_middle BT00TT choose_weighted_vertical BT00TX choose_factorial_bridge BT00VU primorial_four_power_support_package

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

53 script commands · 25 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 (3)
le or ltbeta at existsbeta pascal table prefix exists
01Fix variables and assumptionsL1–2

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

  1. L1
    intro n
  2. L2
    intro k
02Use earlier factsL3–4

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

  1. L3
    specialize le_or_lt k
  2. L4
    specialize le_or_lt n
03Separate the logical casesL5–5

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

  1. L5
    cases le_or_lt
04Establish htableL6–9

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

  1. L6
    have htable : ∃ bb. ∃ bc. ∃ sb. ∃ sc. ∀ x. Lt(x,S n) → ∃ y. ∃ z. BetaAt(bb,bc,x,y) ∧ (BetaAt(sb,sc,x,z) ∧ (x = 0 ∧ (∀ m. Lt(m,S n) → ∃ k. BetaAt(y,z,m,k) ∧ (m = 0 ∧ k = 1 ∨ (∃ i. m = S i ∧ k = 0))) ∨ (∃ m. ∃ k. ∃ i. x = S m ∧ (BetaAt(bb,bc,m,k) ∧ (BetaAt(sb,sc,m,i) ∧ (∀ j. Lt(j,S n) → ∃ u. BetaAt(y,z,j,u) ∧ (j = 0 ∧ u = 1 ∨ (∃ v. ∃ w. ∃ x0. j = S v ∧ (BetaAt(k,i,v,w) ∧ (BetaAt(k,i,S v,x0) ∧ u = w + x0))))))))))Definitions: Lt(x,S n)BetaAt(bb,bc,x,y)BetaAt(sb,sc,x,z)Lt(m,S n)BetaAt(y,z,m,k)BetaAt(bb,bc,m,k)BetaAt(sb,sc,m,i)Lt(j,S n)BetaAt(y,z,j,u)BetaAt(k,i,v,w)BetaAt(k,i,S v,x0)Original native command in the exact edition
  2. L7
    specialize beta_pascal_table_prefix_exists (S n)
  3. L8
    specialize beta_pascal_table_prefix_exists (S n)
  4. L9
    exact beta_pascal_table_prefix_exists
05Separate the logical casesL10–13

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

  1. L10
    cases htable
  2. L11
    cases htable_witness
  3. L12
    cases htable_witness_witness
  4. L13
    cases htable_witness_witness_witness
06Establish hrow_codeL14–18

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

  1. L14
    have hrow_code : ∃ b. BetaAt(x,x1,n,b)Definitions: BetaAt(x,x1,n,b)Original native command in the exact edition
  2. L15
    specialize beta_at_exists x
  3. L16
    specialize beta_at_exists x1
  4. L17
    specialize beta_at_exists n
  5. L18
    exact beta_at_exists
07Separate the logical casesL19–19

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

  1. L19
    cases hrow_code
08Establish hrow_scaleL20–24

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

  1. L20
    have hrow_scale : ∃ c. BetaAt(x2,x3,n,c)Definitions: BetaAt(x2,x3,n,c)Original native command in the exact edition
  2. L21
    specialize beta_at_exists x2
  3. L22
    specialize beta_at_exists x3
  4. L23
    specialize beta_at_exists n
  5. L24
    exact beta_at_exists
09Separate the logical casesL25–25

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

  1. L25
    cases hrow_scale
10Establish hvalueL26–30

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

  1. L26
    have hvalue : ∃ z. BetaAt(x4,x5,k,z)Definitions: BetaAt(x4,x5,k,z)Original native command in the exact edition
  2. L27
    specialize beta_at_exists x4
  3. L28
    specialize beta_at_exists x5
  4. L29
    specialize beta_at_exists k
  5. L30
    exact beta_at_exists
11Separate the logical casesL31–31

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

  1. L31
    cases hvalue
12Construct an explicit witnessL32–32

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

  1. L32
    exists x6
13Separate the logical casesL33–34

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

  1. L33
    right
  2. L34
    split
14Use earlier factsL35–35

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

  1. L35
    exact le_or_lt_left
15Construct an explicit witnessL36–41

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

  1. L36
    exists x
  2. L37
    exists x1
  3. L38
    exists x2
  4. L39
    exists x3
  5. L40
    exists x4
  6. L41
    exists x5
16Separate the logical casesL42–42

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

  1. L42
    split
17Use earlier factsL43–43

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

  1. L43
    exact htable_witness_witness_witness_witness
18Separate the logical casesL44–44

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

  1. L44
    split
19Use earlier factsL45–45

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

  1. L45
    exact hrow_code_witness
20Separate the logical casesL46–46

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

  1. L46
    split
21Use earlier factsL47–48

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

  1. L47
    exact hrow_scale_witness
  2. L48
    exact hvalue_witness
22Construct an explicit witnessL49–49

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

  1. L49
    exists 0
23Separate the logical casesL50–51

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

  1. L50
    left
  2. L51
    split
24Use earlier factsL52–52

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

  1. L52
    exact le_or_lt_right
25Calculate and transport equalitiesL53–53

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

  1. L53
    refl

Library-wide reading audit

Original defined command ledger · 53 lines
  1. 0001intro n
  2. 0002intro k
  3. 0003specialize le_or_lt k
  4. 0004specialize le_or_lt n
  5. 0005cases le_or_lt
  6. 0006have htable : ∃ bb. ∃ bc. ∃ sb. ∃ sc. ∀ x. Lt(x,S n) → ∃ y. ∃ z. BetaAt(bb,bc,x,y) ∧ (BetaAt(sb,sc,x,z) ∧ (x = 0 ∧ (∀ m. Lt(m,S n) → ∃ k. BetaAt(y,z,m,k) ∧ (m = 0 ∧ k = 1 ∨ (∃ i. m = S i ∧ k = 0))) ∨ (∃ m. ∃ k. ∃ i. x = S m ∧ (BetaAt(bb,bc,m,k) ∧ (BetaAt(sb,sc,m,i) ∧ (∀ j. Lt(j,S n) → ∃ u. BetaAt(y,z,j,u) ∧ (j = 0 ∧ u = 1 ∨ (∃ v. ∃ w. ∃ x0. j = S v ∧ (BetaAt(k,i,v,w) ∧ (BetaAt(k,i,S v,x0) ∧ u = w + x0))))))))))
    Exact native replay linehave htable : exists bb bc sb sc. (forall i. (exists gap. gap + S i = S n) -> exists b c. (((exists h. h + S b = S ((S i) * bc)) /\ exists q. bb = q * S ((S i) * bc) + b) /\ (((exists h. h + S c = S ((S i) * sc)) /\ exists q. sb = q * S ((S i) * sc) + c) /\ (((i = 0 /\ (forall j. (exists gap. gap + S j = S n) -> exists value. (((exists h. h + S value = S ((S j) * c)) /\ exists q. b = q * S ((S j) * c) + value) /\ ((j = 0 /\ value = 1) \/ exists p. j = S p /\ value = 0)))) \/ exists predecessor previous_code previous_scale. i = S predecessor /\ (((exists h. h + S previous_code = S ((S predecessor) * bc)) /\ exists q. bb = q * S ((S predecessor) * bc) + previous_code) /\ (((exists h. h + S previous_scale = S ((S predecessor) * sc)) /\ exists q. sb = q * S ((S predecessor) * sc) + previous_scale) /\ forall j. (exists gap. gap + S j = S n) -> exists value. (((exists h. h + S value = S ((S j) * c)) /\ exists q. b = q * S ((S j) * c) + value) /\ ((j = 0 /\ value = 1) \/ exists p u v. j = S p /\ (((exists h. h + S u = S ((S p) * previous_scale)) /\ exists q. previous_code = q * S ((S p) * previous_scale) + u) /\ (((exists h. h + S v = S ((S (S p)) * previous_scale)) /\ exists q. previous_code = q * S ((S (S p)) * previous_scale) + v) /\ value = u + v)))))))))))
  7. 0007specialize beta_pascal_table_prefix_exists (S n)
  8. 0008specialize beta_pascal_table_prefix_exists (S n)
  9. 0009exact beta_pascal_table_prefix_exists
  10. 0010cases htable
  11. 0011cases htable_witness
  12. 0012cases htable_witness_witness
  13. 0013cases htable_witness_witness_witness
  14. 0014have hrow_code : ∃ b. BetaAt(x,x1,n,b)
    Exact native replay linehave hrow_code : exists b. ((exists h. h + S b = S ((S n) * x1)) /\ exists q. x = q * S ((S n) * x1) + b)
  15. 0015specialize beta_at_exists x
  16. 0016specialize beta_at_exists x1
  17. 0017specialize beta_at_exists n
  18. 0018exact beta_at_exists
  19. 0019cases hrow_code
  20. 0020have hrow_scale : ∃ c. BetaAt(x2,x3,n,c)
    Exact native replay linehave hrow_scale : exists c. ((exists h. h + S c = S ((S n) * x3)) /\ exists q. x2 = q * S ((S n) * x3) + c)
  21. 0021specialize beta_at_exists x2
  22. 0022specialize beta_at_exists x3
  23. 0023specialize beta_at_exists n
  24. 0024exact beta_at_exists
  25. 0025cases hrow_scale
  26. 0026have hvalue : ∃ z. BetaAt(x4,x5,k,z)
    Exact native replay linehave hvalue : exists z. ((exists h. h + S z = S ((S k) * x5)) /\ exists q. x4 = q * S ((S k) * x5) + z)
  27. 0027specialize beta_at_exists x4
  28. 0028specialize beta_at_exists x5
  29. 0029specialize beta_at_exists k
  30. 0030exact beta_at_exists
  31. 0031cases hvalue
  32. 0032exists x6
  33. 0033right
  34. 0034split
  35. 0035exact le_or_lt_left
  36. 0036exists x
  37. 0037exists x1
  38. 0038exists x2
  39. 0039exists x3
  40. 0040exists x4
  41. 0041exists x5
  42. 0042split
  43. 0043exact htable_witness_witness_witness_witness
  44. 0044split
  45. 0045exact hrow_code_witness
  46. 0046split
  47. 0047exact hrow_scale_witness
  48. 0048exact hvalue_witness
  49. 0049exists 0
  50. 0050left
  51. 0051split
  52. 0052exact le_or_lt_right
  53. 0053refl