BT0058 · Bertrand theorem

new_value_lt_scaled_base

Stable checked-use theorem · independently kernel verified

The appended value fits every modulus after the same 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. ∀ s. ∀ C. ∀ j. ¬C = 0 → Lt(s,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

1 occurrences

In local proof propositions

PD0001 Le PD0002 Lt

5 occurrences

Exact expanded native-PA statement
forall b s C j. ~(C = 0) -> exists h. h + S s = S ((S j) * (C * S (b + s)))

Proof neighborhood

Direct theorem prerequisites

BT0012 le_add_left BT0016 succ_le_succ BT0055 le_scaled_nonzero BT000F le_trans 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

36 script commands · 6 reading checkpoints · 5 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)
le add leftsucc le succle scaled nonzerole transbase le beta modulus
01Fix variables and assumptionsL1–5

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

  1. L1
    intro b
  2. L2
    intro s
  3. L3
    intro C
  4. L4
    intro j
  5. L5
    intro hC
02Establish hsbL6–9

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

  1. L6
  2. L7
    specialize le_add_left s
  3. L8
    specialize le_add_left b
  4. L9
    exact le_add_left
03Establish hssL10–14

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

  1. L10
  2. L11
    specialize succ_le_succ s
  3. L12
    specialize succ_le_succ (b + s)
  4. L13
    apply succ_le_succ
  5. L14
    exact hsb
04Establish hscaleL15–19

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

  1. L15
    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. L16
    specialize le_scaled_nonzero C
  3. L17
    specialize le_scaled_nonzero (S (b + s))
  4. L18
    apply le_scaled_nonzero
  5. L19
    exact hC
05Establish hsbaseL20–26

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

  1. L20
    have hsbase : Lt(s,C · S (b + s))Definitions: Lt(s,C · S (b + s))Original native command in the exact edition
  2. L21
    specialize le_trans (S s)
  3. L22
    specialize le_trans (S (b + s))
  4. L23
    specialize le_trans (C * S (b + s))
  5. L24
    apply le_trans
  6. L25
    exact hss
  7. L26
    exact hscale
06Establish hmodL27–36

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

  1. L27
    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. L28
    specialize base_le_beta_modulus (C * S (b + s))
  3. L29
    specialize base_le_beta_modulus j
  4. L30
    exact base_le_beta_modulus
  5. L31
    specialize le_trans (S s)
  6. L32
    specialize le_trans (C * S (b + s))
  7. L33
    specialize le_trans (S ((S j) * (C * S (b + s))))
  8. L34
    apply le_trans
  9. L35
    exact hsbase
  10. L36
    exact hmod

Library-wide reading audit

Original defined command ledger · 36 lines
  1. 0001intro b
  2. 0002intro s
  3. 0003intro C
  4. 0004intro j
  5. 0005intro hC
  6. 0006have hsb : Le(s,b + s)
    Exact native replay linehave hsb : exists h. h + s = b + s
  7. 0007specialize le_add_left s
  8. 0008specialize le_add_left b
  9. 0009exact le_add_left
  10. 0010have hss : Lt(s,S (b + s))
    Exact native replay linehave hss : exists h. h + S s = S (b + s)
  11. 0011specialize succ_le_succ s
  12. 0012specialize succ_le_succ (b + s)
  13. 0013apply succ_le_succ
  14. 0014exact hsb
  15. 0015have hscale : Lt(b + s,C · S (b + s))
    Exact native replay linehave hscale : exists h. h + S (b + s) = C * S (b + s)
  16. 0016specialize le_scaled_nonzero C
  17. 0017specialize le_scaled_nonzero (S (b + s))
  18. 0018apply le_scaled_nonzero
  19. 0019exact hC
  20. 0020have hsbase : Lt(s,C · S (b + s))
    Exact native replay linehave hsbase : exists h. h + S s = C * S (b + s)
  21. 0021specialize le_trans (S s)
  22. 0022specialize le_trans (S (b + s))
  23. 0023specialize le_trans (C * S (b + s))
  24. 0024apply le_trans
  25. 0025exact hss
  26. 0026exact hscale
  27. 0027have 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)))
  28. 0028specialize base_le_beta_modulus (C * S (b + s))
  29. 0029specialize base_le_beta_modulus j
  30. 0030exact base_le_beta_modulus
  31. 0031specialize le_trans (S s)
  32. 0032specialize le_trans (C * S (b + s))
  33. 0033specialize le_trans (S ((S j) * (C * S (b + s))))
  34. 0034apply le_trans
  35. 0035exact hsbase
  36. 0036exact hmod