BT0057 · Bertrand theorem

beta_value_lt_scaled_base

Stable checked-use theorem · independently kernel verified

An old beta value fits every modulus after a constructive scaled-base rebase.

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. ∀ i. ∀ x. ∀ C. ∀ s. ∀ j. BetaAt(b,c,i,x) → ¬C = 0 → Lt(x,S (S j · (C · S (b + s))))

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

2 occurrences

In local proof propositions

PD0001 Le PD0002 Lt

7 occurrences

Exact expanded native-PA statement
forall b c i x C s j. ((exists h. h + S x = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + x) -> ~(C = 0) -> exists h. h + S x = S ((S j) * (C * S (b + s)))

Proof neighborhood

Direct theorem prerequisites

BT0053 beta_value_le_code BT0013 le_add_right BT0016 succ_le_succ BT000F le_trans BT0055 le_scaled_nonzero BT0054 base_le_beta_modulus

Direct theorem dependents

BT005D beta_prefix_extend

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

54 script commands · 8 reading checkpoints · 7 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 (6)
beta value le codele add rightsucc le succle transle scaled nonzerobase le beta modulus
01Fix variables and assumptionsL1–9

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro i
  4. L4
    intro x
  5. L5
    intro C
  6. L6
    intro s
  7. L7
    intro j
  8. L8
    intro hat
  9. L9
    intro hC
02Establish hxbL10–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta value le code.

  1. L10
  2. L11
    specialize beta_value_le_code b
  3. L12
    specialize beta_value_le_code c
  4. L13
    specialize beta_value_le_code i
  5. L14
    specialize beta_value_le_code x
  6. L15
    apply beta_value_le_code
  7. L16
    exact hat
03Establish hbsL17–20

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

  1. L17
  2. L18
    specialize le_add_right b
  3. L19
    specialize le_add_right s
  4. L20
    exact le_add_right
04Establish hxsL21–27

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

  1. L21
  2. L22
    specialize le_trans x
  3. L23
    specialize le_trans b
  4. L24
    specialize le_trans (b + s)
  5. L25
    apply le_trans
  6. L26
    exact hxb
  7. L27
    exact hbs
05Establish hsxL28–32

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

  1. L28
  2. L29
    specialize succ_le_succ x
  3. L30
    specialize succ_le_succ (b + s)
  4. L31
    apply succ_le_succ
  5. L32
    exact hxs
06Establish hscaleL33–37

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

  1. L33
    have hscale : Lt(b + s,C · S (b + s))Definitions: Lt(b + s,C · S (b + s))Original native command in the exact edition
  2. L34
    specialize le_scaled_nonzero C
  3. L35
    specialize le_scaled_nonzero (S (b + s))
  4. L36
    apply le_scaled_nonzero
  5. L37
    exact hC
07Establish hxbaseL38–44

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

  1. L38
    have hxbase : Lt(x,C · S (b + s))Definitions: Lt(x,C · S (b + s))Original native command in the exact edition
  2. L39
    specialize le_trans (S x)
  3. L40
    specialize le_trans (S (b + s))
  4. L41
    specialize le_trans (C * S (b + s))
  5. L42
    apply le_trans
  6. L43
    exact hsx
  7. L44
    exact hscale
08Establish hmodL45–54

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

  1. L45
    have hmod : Le(C · S (b + s),S (S j · (C · S (b + s))))Definitions: Le(C · S (b + s),S (S j · (C · S (b + s))))Original native command in the exact edition
  2. L46
    specialize base_le_beta_modulus (C * S (b + s))
  3. L47
    specialize base_le_beta_modulus j
  4. L48
    exact base_le_beta_modulus
  5. L49
    specialize le_trans (S x)
  6. L50
    specialize le_trans (C * S (b + s))
  7. L51
    specialize le_trans (S ((S j) * (C * S (b + s))))
  8. L52
    apply le_trans
  9. L53
    exact hxbase
  10. L54
    exact hmod

Library-wide reading audit

Original defined command ledger · 54 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro i
  4. 0004intro x
  5. 0005intro C
  6. 0006intro s
  7. 0007intro j
  8. 0008intro hat
  9. 0009intro hC
  10. 0010have hxb : Le(x,b)
    Exact native replay linehave hxb : exists h. h + x = b
  11. 0011specialize beta_value_le_code b
  12. 0012specialize beta_value_le_code c
  13. 0013specialize beta_value_le_code i
  14. 0014specialize beta_value_le_code x
  15. 0015apply beta_value_le_code
  16. 0016exact hat
  17. 0017have hbs : Le(b,b + s)
    Exact native replay linehave hbs : exists h. h + b = b + s
  18. 0018specialize le_add_right b
  19. 0019specialize le_add_right s
  20. 0020exact le_add_right
  21. 0021have hxs : Le(x,b + s)
    Exact native replay linehave hxs : exists h. h + x = b + s
  22. 0022specialize le_trans x
  23. 0023specialize le_trans b
  24. 0024specialize le_trans (b + s)
  25. 0025apply le_trans
  26. 0026exact hxb
  27. 0027exact hbs
  28. 0028have hsx : Lt(x,S (b + s))
    Exact native replay linehave hsx : exists h. h + S x = S (b + s)
  29. 0029specialize succ_le_succ x
  30. 0030specialize succ_le_succ (b + s)
  31. 0031apply succ_le_succ
  32. 0032exact hxs
  33. 0033have hscale : Lt(b + s,C · S (b + s))
    Exact native replay linehave hscale : exists h. h + S (b + s) = C * S (b + s)
  34. 0034specialize le_scaled_nonzero C
  35. 0035specialize le_scaled_nonzero (S (b + s))
  36. 0036apply le_scaled_nonzero
  37. 0037exact hC
  38. 0038have hxbase : Lt(x,C · S (b + s))
    Exact native replay linehave hxbase : exists h. h + S x = C * S (b + s)
  39. 0039specialize le_trans (S x)
  40. 0040specialize le_trans (S (b + s))
  41. 0041specialize le_trans (C * S (b + s))
  42. 0042apply le_trans
  43. 0043exact hsx
  44. 0044exact hscale
  45. 0045have hmod : Le(C · S (b + s),S (S j · (C · S (b + s))))
    Exact native replay linehave hmod : exists h. h + C * S (b + s) = S ((S j) * (C * S (b + s)))
  46. 0046specialize base_le_beta_modulus (C * S (b + s))
  47. 0047specialize base_le_beta_modulus j
  48. 0048exact base_le_beta_modulus
  49. 0049specialize le_trans (S x)
  50. 0050specialize le_trans (C * S (b + s))
  51. 0051specialize le_trans (S ((S j) * (C * S (b + s))))
  52. 0052apply le_trans
  53. 0053exact hxbase
  54. 0054exact hmod