BT00R5 · Bertrand theorem

ceil_div_six_square_six_step

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

Ceil((s+6)^2/6) is exactly Ceil(s^2/6)+2*s+6.

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

∀ s. ∀ e. ∀ f. CeilDivSix(s · s,e) → CeilDivSix((s + 6) · (s + 6),f) → f = e + (2 · s + 6)

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

PD0052 CeilDivSix

2 occurrences

In local proof propositions

PD0052 CeilDivSix

2 occurrences

Exact expanded native-PA statement
forall s e f. (((exists bcs_lower_gap_square_source. bcs_lower_gap_square_source + (s * s) = 6 * (e)) /\ exists bcs_upper_gap_square_source. bcs_upper_gap_square_source + S (6 * (e)) = (s * s) + 6)) -> (((exists bcs_lower_gap_square_target. bcs_lower_gap_square_target + ((s + 6) * (s + 6)) = 6 * (f)) /\ exists bcs_upper_gap_square_target. bcs_upper_gap_square_target + S (6 * (f)) = ((s + 6) * (s + 6)) + 6)) -> f = e + (2 * s + 6)

Proof neighborhood

Direct theorem prerequisites

BT00R0 ceil_div_six_shift BT00R4 square_six_shift_identity BT00R2 ceil_div_six_functional

Direct theorem dependents

BT00SW bertrand_h_six_step_transport_from_total

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

24 script commands · 4 reading checkpoints · 3 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)
ceil div six shiftsquare six shift identityceil div six functional
01Fix variables and assumptionsL1–5

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

  1. L1
    intro s
  2. L2
    intro e
  3. L3
    intro f
  4. L4
    intro he
  5. L5
    intro hf
02Establish hshiftL6–11

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply ceil div six shift.

  1. L6
    have hshift : CeilDivSix(s · s + 6 · (2 · s + 6),e + (2 · s + 6))Definitions: CeilDivSix(s · s + 6 · (2 · s + 6),e + (2 · s + 6))Original native command in the exact edition
  2. L7
    specialize ceil_div_six_shift (s * s)
  3. L8
    specialize ceil_div_six_shift e
  4. L9
    specialize ceil_div_six_shift (2 * s + 6)
  5. L10
    apply ceil_div_six_shift
  6. L11
    exact he
03Establish hidL12–14

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

  1. L12
    have hid : s * s + 6 * (2 * s + 6) = (s + 6) * (s + 6)
  2. L13
    specialize square_six_shift_identity s
  3. L14
    exact square_six_shift_identity
04Establish hnextL15–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply ceil div six functional.

  1. L15
    have hnext : CeilDivSix((s + 6) · (s + 6),e + (2 · s + 6))Definitions: CeilDivSix((s + 6) · (s + 6),e + (2 · s + 6))Original native command in the exact edition
  2. L16
    rewrite <- hid
  3. L17
    rewrite <- hid
  4. L18
    exact hshift
  5. L19
    specialize ceil_div_six_functional ((s + 6) * (s + 6))
  6. L20
    specialize ceil_div_six_functional f
  7. L21
    specialize ceil_div_six_functional (e + (2 * s + 6))
  8. L22
    apply ceil_div_six_functional
  9. L23
    exact hf
  10. L24
    exact hnext

Library-wide reading audit

Original defined command ledger · 24 lines
  1. 0001intro s
  2. 0002intro e
  3. 0003intro f
  4. 0004intro he
  5. 0005intro hf
  6. 0006have hshift : CeilDivSix(s · s + 6 · (2 · s + 6),e + (2 · s + 6))
    Exact native replay linehave hshift : ((exists bcs_lower_gap_square_shifted. bcs_lower_gap_square_shifted + (s * s + 6 * (2 * s + 6)) = 6 * (e + (2 * s + 6))) /\ exists bcs_upper_gap_square_shifted. bcs_upper_gap_square_shifted + S (6 * (e + (2 * s + 6))) = (s * s + 6 * (2 * s + 6)) + 6)
  7. 0007specialize ceil_div_six_shift (s * s)
  8. 0008specialize ceil_div_six_shift e
  9. 0009specialize ceil_div_six_shift (2 * s + 6)
  10. 0010apply ceil_div_six_shift
  11. 0011exact he
  12. 0012have hid : s * s + 6 * (2 * s + 6) = (s + 6) * (s + 6)
  13. 0013specialize square_six_shift_identity s
  14. 0014exact square_six_shift_identity
  15. 0015have hnext : CeilDivSix((s + 6) · (s + 6),e + (2 · s + 6))
    Exact native replay linehave hnext : ((exists bcs_lower_gap_square_rewritten. bcs_lower_gap_square_rewritten + ((s + 6) * (s + 6)) = 6 * (e + (2 * s + 6))) /\ exists bcs_upper_gap_square_rewritten. bcs_upper_gap_square_rewritten + S (6 * (e + (2 * s + 6))) = ((s + 6) * (s + 6)) + 6)
  16. 0016rewrite <- hid
  17. 0017rewrite <- hid
  18. 0018exact hshift
  19. 0019specialize ceil_div_six_functional ((s + 6) * (s + 6))
  20. 0020specialize ceil_div_six_functional f
  21. 0021specialize ceil_div_six_functional (e + (2 * s + 6))
  22. 0022apply ceil_div_six_functional
  23. 0023exact hf
  24. 0024exact hnext