BT0054

base_le_beta_modulus

Stable checked-use theorem · independently kernel verified

A beta base is at most every beta modulus over that base.

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 c i. exists h. h + c = S ((S i) * c)

Structural proof guide

A beta base is at most every beta modulus over that base.

Direct prerequisites: le_add_left, mul_succ_left, le_succ. The authored body proceeds by intermediate claims (1), equality transport (1).

Proof neighborhood

Direct dependencies

BT0012 le_add_left BT0005 mul_succ_left BT0018 le_succ

Direct dependents

BT0057 beta_value_lt_scaled_base BT0058 new_value_lt_scaled_base

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

13 script commands · 3 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 (3)
le add leftmul succ leftle succ
01Fix variables and assumptionsL1–2

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

  1. L1
    intro c
  2. L2
    intro i
02Establish hproductL3–12

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

  1. L3
    have hproduct : exists h. h + c = S i * c
  2. L4
    specialize mul_succ_left i
  3. L5
    specialize mul_succ_left c
  4. L6
    rewrite mul_succ_left
  5. L7
    specialize le_add_left c
  6. L8
    specialize le_add_left (i * c)
  7. L9
    exact le_add_left
  8. L10
    specialize le_succ c
  9. L11
    specialize le_succ (S i * c)
  10. L12
    apply le_succ
03Use earlier factsL13–13

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

  1. L13
    exact hproduct

Library-wide reading audit

Original exact command ledger · 13 lines
  1. 0001intro c
  2. 0002intro i
  3. 0003have hproduct : exists h. h + c = S i * c
  4. 0004specialize mul_succ_left i
  5. 0005specialize mul_succ_left c
  6. 0006rewrite mul_succ_left
  7. 0007specialize le_add_left c
  8. 0008specialize le_add_left (i * c)
  9. 0009exact le_add_left
  10. 0010specialize le_succ c
  11. 0011specialize le_succ (S i * c)
  12. 0012apply le_succ
  13. 0013exact hproduct