BT010U · Bertrand theorem

beta_product_all_one_exact

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

A Product whose decoded factors are all one is exactly one.

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

∀ b. ∀ c. ∀ l. ∀ z. (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → y = 1) → Product(b,c,l,z) → z = 1

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 PD0014 Product

3 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0014 Product

4 occurrences

Exact expanded native-PA statement
forall b c l z. (forall i a. (exists bcf_lt_gap_b5bpao_bound. bcf_lt_gap_b5bpao_bound + S (i) = l) -> (((exists bpr_height_b5bpao_entry. bpr_height_b5bpao_entry + S (a) = S ((S (i)) * c)) /\ exists bpr_quotient_b5bpao_entry. b = bpr_quotient_b5bpao_entry * S ((S (i)) * c) + (a))) -> a = 1) -> (exists ff_u_b5bpao_product ff_v_b5bpao_product. ((((exists ff_h_b5bpao_product_start. ff_h_b5bpao_product_start + S (1) = S ((S (0)) * ff_v_b5bpao_product)) /\ exists ff_q_b5bpao_product_start. ff_u_b5bpao_product = ff_q_b5bpao_product_start * S ((S (0)) * ff_v_b5bpao_product) + (1))) /\ ((((exists ff_h_b5bpao_product_terminal. ff_h_b5bpao_product_terminal + S (z) = S ((S (l)) * ff_v_b5bpao_product)) /\ exists ff_q_b5bpao_product_terminal. ff_u_b5bpao_product = ff_q_b5bpao_product_terminal * S ((S (l)) * ff_v_b5bpao_product) + (z))) /\ forall ff_i_b5bpao_product. (exists ff_lt_b5bpao_product_bound. ff_lt_b5bpao_product_bound + S ff_i_b5bpao_product = l) -> exists ff_p_b5bpao_product ff_r_b5bpao_product ff_s_b5bpao_product. ((((exists ff_h_b5bpao_product_factor. ff_h_b5bpao_product_factor + S (ff_p_b5bpao_product) = S ((S (ff_i_b5bpao_product)) * c)) /\ exists ff_q_b5bpao_product_factor. b = ff_q_b5bpao_product_factor * S ((S (ff_i_b5bpao_product)) * c) + (ff_p_b5bpao_product))) /\ ((((exists ff_h_b5bpao_product_partial. ff_h_b5bpao_product_partial + S (ff_r_b5bpao_product) = S ((S (ff_i_b5bpao_product)) * ff_v_b5bpao_product)) /\ exists ff_q_b5bpao_product_partial. ff_u_b5bpao_product = ff_q_b5bpao_product_partial * S ((S (ff_i_b5bpao_product)) * ff_v_b5bpao_product) + (ff_r_b5bpao_product))) /\ ((((exists ff_h_b5bpao_product_successor. ff_h_b5bpao_product_successor + S (ff_s_b5bpao_product) = S ((S (S ff_i_b5bpao_product)) * ff_v_b5bpao_product)) /\ exists ff_q_b5bpao_product_successor. ff_u_b5bpao_product = ff_q_b5bpao_product_successor * S ((S (S ff_i_b5bpao_product)) * ff_v_b5bpao_product) + (ff_s_b5bpao_product))) /\ ff_s_b5bpao_product = ff_r_b5bpao_product * ff_p_b5bpao_product)))))) -> z = 1

Proof neighborhood

Direct theorem prerequisites

BT005I beta_product_zero BT005J beta_product_succ_decompose BT0018 le_succ BT000E le_refl BT000A mul_one

Direct theorem dependents

BT0112 no_bertrand_high_contribution_interval_eq_one

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

55 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 (5)
beta product zerobeta product succ decomposele succle reflmul one
01Fix variables and assumptionsL1–2

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

  1. L1
    intro b
  2. L2
    intro c
02Induction on lL3–12

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

  1. L3
    induction l
  2. L4
    intro z
  3. L5
    intro hall
  4. L6
    intro hproduct
  5. L7
    specialize beta_product_zero b
  6. L8
    specialize beta_product_zero c
  7. L9
    specialize beta_product_zero z
  8. L10
    apply beta_product_zero
  9. L11
    exact hproduct
  10. L12
    intro z
03Fix variables and assumptionsL13–14

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

  1. L13
    intro hall
  2. L14
    intro hproduct
04Establish hdecompositionL15–21

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

  1. L15
    have hdecomposition : ∃ a. ∃ r. BetaAt(b,c,l,a) ∧ (Product(b,c,l,r) ∧ z = r · a)Definitions: BetaAt(b,c,l,a)Product(b,c,l,r)Original native command in the exact edition
  2. L16
    specialize beta_product_succ_decompose b
  3. L17
    specialize beta_product_succ_decompose c
  4. L18
    specialize beta_product_succ_decompose l
  5. L19
    specialize beta_product_succ_decompose z
  6. L20
    apply beta_product_succ_decompose
  7. L21
    exact hproduct
05Separate the logical casesL22–25

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

  1. L22
    cases hdecomposition
  2. L23
    cases hdecomposition_witness
  3. L24
    cases hdecomposition_witness_witness
  4. L25
    cases hdecomposition_witness_witness_right
06Establish hpreviousL26–35

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

  1. L26
    have hprevious : ∀ i. ∀ a. Lt(i,l) → BetaAt(b,c,i,a) → a = 1Definitions: Lt(i,l)BetaAt(b,c,i,a)Original native command in the exact edition
  2. L27
    intro i
  3. L28
    intro a
  4. L29
    intro hi
  5. L30
    intro ha
  6. L31
    specialize hall i
  7. L32
    specialize hall a
  8. L33
    apply hall
  9. L34
    specialize le_succ (S i)
  10. L35
    specialize le_succ l
07Use earlier factsL36–38

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

  1. L36
    apply le_succ
  2. L37
    exact hi
  3. L38
    exact ha
08Establish hprefix_oneL39–43

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

  1. L39
    have hprefix_one : x1 = 1
  2. L40
    specialize IH x1
  3. L41
    apply IH
  4. L42
    exact hprevious
  5. L43
    exact hdecomposition_witness_witness_right_left
09Establish hfactor_oneL44–53

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

  1. L44
    have hfactor_one : x = 1
  2. L45
    specialize hall l
  3. L46
    specialize hall x
  4. L47
    apply hall
  5. L48
    specialize le_refl (S l)
  6. L49
    exact le_refl
  7. L50
    exact hdecomposition_witness_witness_left
  8. L51
    rewrite hdecomposition_witness_witness_right_right
  9. L52
    rewrite hprefix_one
  10. L53
    rewrite hfactor_one
10Use earlier factsL54–55

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

  1. L54
    specialize mul_one 1
  2. L55
    exact mul_one

Library-wide reading audit

Original defined command ledger · 55 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003induction l
  4. 0004intro z
  5. 0005intro hall
  6. 0006intro hproduct
  7. 0007specialize beta_product_zero b
  8. 0008specialize beta_product_zero c
  9. 0009specialize beta_product_zero z
  10. 0010apply beta_product_zero
  11. 0011exact hproduct
  12. 0012intro z
  13. 0013intro hall
  14. 0014intro hproduct
  15. 0015have hdecomposition : ∃ a. ∃ r. BetaAt(b,c,l,a) ∧ (Product(b,c,l,r) ∧ z = r · a)
    Exact native replay linehave hdecomposition : exists a r. (((exists bpr_height_b5bpao_decomposition_entry. bpr_height_b5bpao_decomposition_entry + S (a) = S ((S (l)) * c)) /\ exists bpr_quotient_b5bpao_decomposition_entry. b = bpr_quotient_b5bpao_decomposition_entry * S ((S (l)) * c) + (a))) /\ ((exists ff_u_b5bpao_decomposition_product ff_v_b5bpao_decomposition_product. ((((exists ff_h_b5bpao_decomposition_product_start. ff_h_b5bpao_decomposition_product_start + S (1) = S ((S (0)) * ff_v_b5bpao_decomposition_product)) /\ exists ff_q_b5bpao_decomposition_product_start. ff_u_b5bpao_decomposition_product = ff_q_b5bpao_decomposition_product_start * S ((S (0)) * ff_v_b5bpao_decomposition_product) + (1))) /\ ((((exists ff_h_b5bpao_decomposition_product_terminal. ff_h_b5bpao_decomposition_product_terminal + S (r) = S ((S (l)) * ff_v_b5bpao_decomposition_product)) /\ exists ff_q_b5bpao_decomposition_product_terminal. ff_u_b5bpao_decomposition_product = ff_q_b5bpao_decomposition_product_terminal * S ((S (l)) * ff_v_b5bpao_decomposition_product) + (r))) /\ forall ff_i_b5bpao_decomposition_product. (exists ff_lt_b5bpao_decomposition_product_bound. ff_lt_b5bpao_decomposition_product_bound + S ff_i_b5bpao_decomposition_product = l) -> exists ff_p_b5bpao_decomposition_product ff_r_b5bpao_decomposition_product ff_s_b5bpao_decomposition_product. ((((exists ff_h_b5bpao_decomposition_product_factor. ff_h_b5bpao_decomposition_product_factor + S (ff_p_b5bpao_decomposition_product) = S ((S (ff_i_b5bpao_decomposition_product)) * c)) /\ exists ff_q_b5bpao_decomposition_product_factor. b = ff_q_b5bpao_decomposition_product_factor * S ((S (ff_i_b5bpao_decomposition_product)) * c) + (ff_p_b5bpao_decomposition_product))) /\ ((((exists ff_h_b5bpao_decomposition_product_partial. ff_h_b5bpao_decomposition_product_partial + S (ff_r_b5bpao_decomposition_product) = S ((S (ff_i_b5bpao_decomposition_product)) * ff_v_b5bpao_decomposition_product)) /\ exists ff_q_b5bpao_decomposition_product_partial. ff_u_b5bpao_decomposition_product = ff_q_b5bpao_decomposition_product_partial * S ((S (ff_i_b5bpao_decomposition_product)) * ff_v_b5bpao_decomposition_product) + (ff_r_b5bpao_decomposition_product))) /\ ((((exists ff_h_b5bpao_decomposition_product_successor. ff_h_b5bpao_decomposition_product_successor + S (ff_s_b5bpao_decomposition_product) = S ((S (S ff_i_b5bpao_decomposition_product)) * ff_v_b5bpao_decomposition_product)) /\ exists ff_q_b5bpao_decomposition_product_successor. ff_u_b5bpao_decomposition_product = ff_q_b5bpao_decomposition_product_successor * S ((S (S ff_i_b5bpao_decomposition_product)) * ff_v_b5bpao_decomposition_product) + (ff_s_b5bpao_decomposition_product))) /\ ff_s_b5bpao_decomposition_product = ff_r_b5bpao_decomposition_product * ff_p_b5bpao_decomposition_product)))))) /\ z = r * a)
  16. 0016specialize beta_product_succ_decompose b
  17. 0017specialize beta_product_succ_decompose c
  18. 0018specialize beta_product_succ_decompose l
  19. 0019specialize beta_product_succ_decompose z
  20. 0020apply beta_product_succ_decompose
  21. 0021exact hproduct
  22. 0022cases hdecomposition
  23. 0023cases hdecomposition_witness
  24. 0024cases hdecomposition_witness_witness
  25. 0025cases hdecomposition_witness_witness_right
  26. 0026have hprevious : ∀ i. ∀ a. Lt(i,l) → BetaAt(b,c,i,a) → a = 1
    Exact native replay linehave hprevious : forall i a. (exists bcf_lt_gap_b5bpao_previous_bound. bcf_lt_gap_b5bpao_previous_bound + S (i) = l) -> (((exists bpr_height_b5bpao_previous_entry. bpr_height_b5bpao_previous_entry + S (a) = S ((S (i)) * c)) /\ exists bpr_quotient_b5bpao_previous_entry. b = bpr_quotient_b5bpao_previous_entry * S ((S (i)) * c) + (a))) -> a = 1
  27. 0027intro i
  28. 0028intro a
  29. 0029intro hi
  30. 0030intro ha
  31. 0031specialize hall i
  32. 0032specialize hall a
  33. 0033apply hall
  34. 0034specialize le_succ (S i)
  35. 0035specialize le_succ l
  36. 0036apply le_succ
  37. 0037exact hi
  38. 0038exact ha
  39. 0039have hprefix_one : x1 = 1
  40. 0040specialize IH x1
  41. 0041apply IH
  42. 0042exact hprevious
  43. 0043exact hdecomposition_witness_witness_right_left
  44. 0044have hfactor_one : x = 1
  45. 0045specialize hall l
  46. 0046specialize hall x
  47. 0047apply hall
  48. 0048specialize le_refl (S l)
  49. 0049exact le_refl
  50. 0050exact hdecomposition_witness_witness_left
  51. 0051rewrite hdecomposition_witness_witness_right_right
  52. 0052rewrite hprefix_one
  53. 0053rewrite hfactor_one
  54. 0054specialize mul_one 1
  55. 0055exact mul_one