BT00R5

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.

Exact expanded 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)

Structural proof guide

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

Direct prerequisites: ceil_div_six_shift, square_six_shift_identity, ceil_div_six_functional. The authored body proceeds by intermediate claims (3), equality transport (2).

Proof neighborhood

Direct dependencies

BT00R0 ceil_div_six_shift BT00R4 square_six_shift_identity BT00R2 ceil_div_six_functional

Direct dependents

BT00SW bertrand_h_six_step_transport_from_total

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

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.

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 : ((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)
  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 : ((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)
  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 exact command ledger · 24 lines
  1. 0001intro s
  2. 0002intro e
  3. 0003intro f
  4. 0004intro he
  5. 0005intro hf
  6. 0006have 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 : ((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