BT0056

scaled_bounded_common_multiple

Stable checked-use theorem · independently kernel verified

A right multiple of a bounded common multiple remains such a common multiple.

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 C B. (forall t. (exists h. S t + S h = S N) -> exists q. C = S t * q) -> forall t. (exists h. S t + S h = S N) -> exists q. C * B = S t * q

Structural proof guide

A right multiple of a bounded common multiple remains such a common multiple.

Direct prerequisites: multiple_mul_right. The authored body proceeds by intermediate claims (1).

Proof neighborhood

Direct dependencies

BT002A multiple_mul_right

Direct dependents

BT005D beta_prefix_extend

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

15 script commands · 2 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)
multiple mul right
01Fix variables and assumptionsL1–6

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

  1. L1
    intro N
  2. L2
    intro C
  3. L3
    intro B
  4. L4
    intro hcm
  5. L5
    intro t
  6. L6
    intro ht
02Establish htCL7–15

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

  1. L7
    have htC : exists q. C = S t * q
  2. L8
    specialize hcm t
  3. L9
    apply hcm
  4. L10
    exact ht
  5. L11
    specialize multiple_mul_right (S t)
  6. L12
    specialize multiple_mul_right C
  7. L13
    specialize multiple_mul_right B
  8. L14
    apply multiple_mul_right
  9. L15
    exact htC

Library-wide reading audit

Original exact command ledger · 15 lines
  1. 0001intro N
  2. 0002intro C
  3. 0003intro B
  4. 0004intro hcm
  5. 0005intro t
  6. 0006intro ht
  7. 0007have htC : exists q. C = S t * q
  8. 0008specialize hcm t
  9. 0009apply hcm
  10. 0010exact ht
  11. 0011specialize multiple_mul_right (S t)
  12. 0012specialize multiple_mul_right C
  13. 0013specialize multiple_mul_right B
  14. 0014apply multiple_mul_right
  15. 0015exact htC