BT00RH

canonical_double_triple_remainder_complement_budget

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

Canonical remainder data yields and preserves the complement budget.

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. (((2 * (n) = 3 * (q) + (r)) /\ exists bqb_remainder_gap_canonical_source. bqb_remainder_gap_canonical_source + S (r) = 3)) -> exists c. (((((q) + (c) = (n)) /\ exists bqb_budget_gap_canonical_result. bqb_budget_gap_canonical_result + 2 * (n) = 6 * (c))) /\ exists bqb_remainder_gap_canonical_preserved. bqb_remainder_gap_canonical_preserved + S r = 3)

Structural proof guide

Canonical remainder data yields and preserves the complement budget.

Direct prerequisites: double_triple_remainder_complement_budget. The authored body proceeds by case analysis (2), intermediate claims (1).

Proof neighborhood

Direct dependencies

BT00RG double_triple_remainder_complement_budget

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

16 script commands · 7 reading checkpoints · 1 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 (1)
double triple remainder complement budget
01Fix variables and assumptionsL1–4

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 hcanonical
02Separate the logical casesL5–5

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

  1. L5
    cases hcanonical
03Establish hbaseL6–11

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

  1. L6
    have hbase : exists c. ((((q) + (c) = (n)) /\ exists bqb_budget_gap_canonical_base. bqb_budget_gap_canonical_base + 2 * (n) = 6 * (c)))
  2. L7
    specialize double_triple_remainder_complement_budget n
  3. L8
    specialize double_triple_remainder_complement_budget q
  4. L9
    specialize double_triple_remainder_complement_budget r
  5. L10
    apply double_triple_remainder_complement_budget
  6. L11
    exact hcanonical_left
04Separate the logical casesL12–12

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

  1. L12
    cases hbase
05Construct an explicit witnessL13–13

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

  1. L13
    exists x
06Separate the logical casesL14–14

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

  1. L14
    split
07Use earlier factsL15–16

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

  1. L15
    exact hbase_witness
  2. L16
    exact hcanonical_right

Library-wide reading audit

Original exact command ledger · 16 lines
  1. 0001intro n
  2. 0002intro q
  3. 0003intro r
  4. 0004intro hcanonical
  5. 0005cases hcanonical
  6. 0006have hbase : exists c. ((((q) + (c) = (n)) /\ exists bqb_budget_gap_canonical_base. bqb_budget_gap_canonical_base + 2 * (n) = 6 * (c)))
  7. 0007specialize double_triple_remainder_complement_budget n
  8. 0008specialize double_triple_remainder_complement_budget q
  9. 0009specialize double_triple_remainder_complement_budget r
  10. 0010apply double_triple_remainder_complement_budget
  11. 0011exact hcanonical_left
  12. 0012cases hbase
  13. 0013exists x
  14. 0014split
  15. 0015exact hbase_witness
  16. 0016exact hcanonical_right