BT00RJ

floor_ceil_division_budget

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

Raw canonical division data closes both B6 quotient-budget inequalities.

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 r s e. (((exists bcs_sqrt_lower_gap_division_bridge_floor. bcs_sqrt_lower_gap_division_bridge_floor + (s) * (s) = (2 * n)) /\ exists bcs_sqrt_upper_gap_division_bridge_floor. bcs_sqrt_upper_gap_division_bridge_floor + S (2 * n) = S (s) * S (s))) -> (((exists bcs_lower_gap_division_bridge_ceil. bcs_lower_gap_division_bridge_ceil + (s * s) = 6 * (e)) /\ exists bcs_upper_gap_division_bridge_ceil. bcs_upper_gap_division_bridge_ceil + S (6 * (e)) = (s * s) + 6)) -> (((2 * (n) = 3 * (q) + (r)) /\ exists bqb_remainder_gap_division_bridge_source. bqb_remainder_gap_division_bridge_source + S (r) = 3)) -> exists c. ((((((q) + (c) = (n)) /\ exists bqb_budget_gap_division_bridge_result. bqb_budget_gap_division_bridge_result + 2 * (n) = 6 * (c))) /\ ((exists bqb_le_gap_division_bridge_ec. bqb_le_gap_division_bridge_ec + (e) = (c)) /\ (exists bqb_le_gap_division_bridge_sum. bqb_le_gap_division_bridge_sum + (q + e) = (n)))) /\ exists bqb_remainder_gap_division_bridge_preserved. bqb_remainder_gap_division_bridge_preserved + S r = 3)

Structural proof guide

Raw canonical division data closes both B6 quotient-budget inequalities.

Direct prerequisites: canonical_double_triple_remainder_complement_budget, floor_ceil_complement_budget. The authored body proceeds by case analysis (3), intermediate claims (2).

Proof neighborhood

Direct dependencies

BT00RH canonical_double_triple_remainder_complement_budget BT00RI floor_ceil_complement_budget

Direct dependents

BT00X6 bertrand_main_inequality_factorized_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

34 script commands · 8 reading checkpoints · 2 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 (2)
canonical double triple remainder complement budgetfloor ceil complement budget
01Fix variables and assumptionsL1–8

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

  1. L1
    intro n
  2. L2
    intro q
  3. L3
    intro r
  4. L4
    intro s
  5. L5
    intro e
  6. L6
    intro hfloor
  7. L7
    intro hceil
  8. L8
    intro hcanonical
02Establish hdataL9–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply canonical double triple remainder complement budget.

  1. L9
    have hdata : exists c. (((((q) + (c) = (n)) /\ exists bqb_budget_gap_division_bridge_data. bqb_budget_gap_division_bridge_data + 2 * (n) = 6 * (c))) /\ exists bqb_remainder_gap_division_bridge_data. bqb_remainder_gap_division_bridge_data + S r = 3)
  2. L10
    specialize canonical_double_triple_remainder_complement_budget n
  3. L11
    specialize canonical_double_triple_remainder_complement_budget q
  4. L12
    specialize canonical_double_triple_remainder_complement_budget r
  5. L13
    apply canonical_double_triple_remainder_complement_budget
  6. L14
    exact hcanonical
03Separate the logical casesL15–17

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

  1. L15
    cases hdata
  2. L16
    cases hdata_witness
  3. L17
    cases hdata_witness_left
04Establish hbridgeL18–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply floor ceil complement budget.

  1. L18
    have hbridge : (exists k. k + e = x) /\ exists k. k + (q + e) = n
  2. L19
    specialize floor_ceil_complement_budget n
  3. L20
    specialize floor_ceil_complement_budget q
  4. L21
    specialize floor_ceil_complement_budget s
  5. L22
    specialize floor_ceil_complement_budget e
  6. L23
    specialize floor_ceil_complement_budget x
  7. L24
    apply floor_ceil_complement_budget
  8. L25
    exact hfloor
  9. L26
    exact hceil
  10. L27
    exact hdata_witness_left_left
05Use earlier factsL28–28

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

  1. L28
    exact hdata_witness_left_right
06Construct an explicit witnessL29–29

Supply the displayed value, then prove that it has the required property.

  1. L29
    exists x
07Separate the logical casesL30–31

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

  1. L30
    split
  2. L31
    split
08Use earlier factsL32–34

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

  1. L32
    exact hdata_witness_left
  2. L33
    exact hbridge
  3. L34
    exact hdata_witness_right

Library-wide reading audit

Original exact command ledger · 34 lines
  1. 0001intro n
  2. 0002intro q
  3. 0003intro r
  4. 0004intro s
  5. 0005intro e
  6. 0006intro hfloor
  7. 0007intro hceil
  8. 0008intro hcanonical
  9. 0009have hdata : exists c. (((((q) + (c) = (n)) /\ exists bqb_budget_gap_division_bridge_data. bqb_budget_gap_division_bridge_data + 2 * (n) = 6 * (c))) /\ exists bqb_remainder_gap_division_bridge_data. bqb_remainder_gap_division_bridge_data + S r = 3)
  10. 0010specialize canonical_double_triple_remainder_complement_budget n
  11. 0011specialize canonical_double_triple_remainder_complement_budget q
  12. 0012specialize canonical_double_triple_remainder_complement_budget r
  13. 0013apply canonical_double_triple_remainder_complement_budget
  14. 0014exact hcanonical
  15. 0015cases hdata
  16. 0016cases hdata_witness
  17. 0017cases hdata_witness_left
  18. 0018have hbridge : (exists k. k + e = x) /\ exists k. k + (q + e) = n
  19. 0019specialize floor_ceil_complement_budget n
  20. 0020specialize floor_ceil_complement_budget q
  21. 0021specialize floor_ceil_complement_budget s
  22. 0022specialize floor_ceil_complement_budget e
  23. 0023specialize floor_ceil_complement_budget x
  24. 0024apply floor_ceil_complement_budget
  25. 0025exact hfloor
  26. 0026exact hceil
  27. 0027exact hdata_witness_left_left
  28. 0028exact hdata_witness_left_right
  29. 0029exists x
  30. 0030split
  31. 0031split
  32. 0032exact hdata_witness_left
  33. 0033exact hbridge
  34. 0034exact hdata_witness_right