BT00RI

floor_ceil_complement_budget

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

Floor-square and ceiling budgets imply e<=c and q+e<=n.

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 n q s e c. (((exists bcs_sqrt_lower_gap_complement_bridge_floor. bcs_sqrt_lower_gap_complement_bridge_floor + (s) * (s) = (2 * n)) /\ exists bcs_sqrt_upper_gap_complement_bridge_floor. bcs_sqrt_upper_gap_complement_bridge_floor + S (2 * n) = S (s) * S (s))) -> (((exists bcs_lower_gap_complement_bridge_ceil. bcs_lower_gap_complement_bridge_ceil + (s * s) = 6 * (e)) /\ exists bcs_upper_gap_complement_bridge_ceil. bcs_upper_gap_complement_bridge_ceil + S (6 * (e)) = (s * s) + 6)) -> q + c = n -> (exists k. k + 2 * n = 6 * c) -> ((exists bqb_le_gap_complement_bridge_ec. bqb_le_gap_complement_bridge_ec + (e) = (c)) /\ (exists bqb_le_gap_complement_bridge_sum. bqb_le_gap_complement_bridge_sum + (q + e) = (n)))

Structural proof guide

Floor-square and ceiling budgets imply e<=c and q+e<=n.

Direct prerequisites: le_trans, ceil_div_six_le_of_upper, add_le_add_left. The authored body proceeds by case analysis (1), intermediate claims (3), equality transport (1).

Proof neighborhood

Direct dependencies

BT000F le_trans BT00RF ceil_div_six_le_of_upper BT0015 add_le_add_left

Direct dependents

BT00RJ floor_ceil_division_budget

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

34 script commands · 9 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)
le transceil div six le of upperadd le add left
01Fix variables and assumptionsL1–9

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

  1. L1
    intro n
  2. L2
    intro q
  3. L3
    intro s
  4. L4
    intro e
  5. L5
    intro c
  6. L6
    intro hfloor
  7. L7
    intro hceil
  8. L8
    intro hcomp
  9. L9
    intro hbudget
02Separate the logical casesL10–10

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

  1. L10
    cases hfloor
03Establish hsquareL11–17

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

  1. L11
    have hsquare : exists k. k + s * s = 6 * c
  2. L12
    specialize le_trans (s * s)
  3. L13
    specialize le_trans (2 * n)
  4. L14
    specialize le_trans (6 * c)
  5. L15
    apply le_trans
  6. L16
    exact hfloor_left
  7. L17
    exact hbudget
04Establish hecL18–24

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

  1. L18
    have hec : exists k. k + e = c
  2. L19
    specialize ceil_div_six_le_of_upper (s * s)
  3. L20
    specialize ceil_div_six_le_of_upper e
  4. L21
    specialize ceil_div_six_le_of_upper c
  5. L22
    apply ceil_div_six_le_of_upper
  6. L23
    exact hceil
  7. L24
    exact hsquare
05Establish hsumL25–30

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

  1. L25
    have hsum : exists k. k + (q + e) = q + c
  2. L26
    specialize add_le_add_left e
  3. L27
    specialize add_le_add_left c
  4. L28
    specialize add_le_add_left q
  5. L29
    apply add_le_add_left
  6. L30
    exact hec
06Separate the logical casesL31–31

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

  1. L31
    split
07Use earlier factsL32–32

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

  1. L32
    exact hec
08Calculate and transport equalitiesL33–33

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L33
    rewrite <- hcomp
09Use earlier factsL34–34

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

  1. L34
    exact hsum

Library-wide reading audit

Original exact command ledger · 34 lines
  1. 0001intro n
  2. 0002intro q
  3. 0003intro s
  4. 0004intro e
  5. 0005intro c
  6. 0006intro hfloor
  7. 0007intro hceil
  8. 0008intro hcomp
  9. 0009intro hbudget
  10. 0010cases hfloor
  11. 0011have hsquare : exists k. k + s * s = 6 * c
  12. 0012specialize le_trans (s * s)
  13. 0013specialize le_trans (2 * n)
  14. 0014specialize le_trans (6 * c)
  15. 0015apply le_trans
  16. 0016exact hfloor_left
  17. 0017exact hbudget
  18. 0018have hec : exists k. k + e = c
  19. 0019specialize ceil_div_six_le_of_upper (s * s)
  20. 0020specialize ceil_div_six_le_of_upper e
  21. 0021specialize ceil_div_six_le_of_upper c
  22. 0022apply ceil_div_six_le_of_upper
  23. 0023exact hceil
  24. 0024exact hsquare
  25. 0025have hsum : exists k. k + (q + e) = q + c
  26. 0026specialize add_le_add_left e
  27. 0027specialize add_le_add_left c
  28. 0028specialize add_le_add_left q
  29. 0029apply add_le_add_left
  30. 0030exact hec
  31. 0031split
  32. 0032exact hec
  33. 0033rewrite <- hcomp
  34. 0034exact hsum