BT011C

scaled_remainder_lift

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

Scale a quotient-remainder equation and normalize its new tail.

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 d x q t c r s u. x = d * q + t -> c * t + r = d * s + u -> c * x + r = d * (c * q + s) + u

Structural proof guide

Scale a quotient-remainder equation and normalize its new tail.

Direct prerequisites: mul_add, mul_assoc, mul_comm, add_assoc. The authored body proceeds by intermediate claims (4), equality transport (6).

Proof neighborhood

Direct dependencies

BT0007 mul_add BT0008 mul_assoc BT0006 mul_comm BT0003 add_assoc

Direct dependents

BT011E double_scaled_remainder_lift BT011K prime_eighty_three BT011L prime_one_hundred_sixty_three BT011M prime_three_hundred_seventeen

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

39 script commands · 6 reading checkpoints · 4 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 (4)
mul addmul assocmul commadd assoc
01Fix variables and assumptionsL1–10

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

  1. L1
    intro d
  2. L2
    intro x
  3. L3
    intro q
  4. L4
    intro t
  5. L5
    intro c
  6. L6
    intro r
  7. L7
    intro s
  8. L8
    intro u
  9. L9
    intro hx
  10. L10
    intro htail
02Calculate and transport equalitiesL11–11

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

  1. L11
    rewrite hx
03Establish hdistL12–17

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

  1. L12
    have hdist : c * (d * q + t) = c * (d * q) + c * t
  2. L13
    specialize mul_add c
  3. L14
    specialize mul_add (d * q)
  4. L15
    specialize mul_add t
  5. L16
    exact mul_add
  6. L17
    rewrite hdist
04Establish hassocL18–21

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

  1. L18
    have hassoc : (c * (d * q) + c * t) + r = c * (d * q) + (c * t + r)
  2. L19
    apply add_assoc
  3. L20
    rewrite hassoc
  4. L21
    rewrite htail
05Establish hfrontL22–31

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

  1. L22
    have hfront : c * (d * q) = d * (c * q)
  2. L23
    trans (c * d) * q
  3. L24
    symm
  4. L25
    apply mul_assoc
  5. L26
    trans (d * c) * q
  6. L27
    congr
  7. L28
    apply mul_comm
  8. L29
    refl
  9. L30
    apply mul_assoc
  10. L31
    rewrite hfront
06Establish hdist2L32–39

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

  1. L32
    have hdist2 : d * (c * q + s) = d * (c * q) + d * s
  2. L33
    specialize mul_add d
  3. L34
    specialize mul_add (c * q)
  4. L35
    specialize mul_add s
  5. L36
    exact mul_add
  6. L37
    rewrite hdist2
  7. L38
    symm
  8. L39
    apply add_assoc

Library-wide reading audit

Original exact command ledger · 39 lines
  1. 0001intro d
  2. 0002intro x
  3. 0003intro q
  4. 0004intro t
  5. 0005intro c
  6. 0006intro r
  7. 0007intro s
  8. 0008intro u
  9. 0009intro hx
  10. 0010intro htail
  11. 0011rewrite hx
  12. 0012have hdist : c * (d * q + t) = c * (d * q) + c * t
  13. 0013specialize mul_add c
  14. 0014specialize mul_add (d * q)
  15. 0015specialize mul_add t
  16. 0016exact mul_add
  17. 0017rewrite hdist
  18. 0018have hassoc : (c * (d * q) + c * t) + r = c * (d * q) + (c * t + r)
  19. 0019apply add_assoc
  20. 0020rewrite hassoc
  21. 0021rewrite htail
  22. 0022have hfront : c * (d * q) = d * (c * q)
  23. 0023trans (c * d) * q
  24. 0024symm
  25. 0025apply mul_assoc
  26. 0026trans (d * c) * q
  27. 0027congr
  28. 0028apply mul_comm
  29. 0029refl
  30. 0030apply mul_assoc
  31. 0031rewrite hfront
  32. 0032have hdist2 : d * (c * q + s) = d * (c * q) + d * s
  33. 0033specialize mul_add d
  34. 0034specialize mul_add (c * q)
  35. 0035specialize mul_add s
  36. 0036exact mul_add
  37. 0037rewrite hdist2
  38. 0038symm
  39. 0039apply add_assoc