BT0058

new_value_lt_scaled_base

Stable checked-use theorem · independently kernel verified

The appended value fits every modulus after the same constructive scaled-base rebase.

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 b s C j. ~(C = 0) -> exists h. h + S s = S ((S j) * (C * S (b + s)))

Structural proof guide

The appended value fits every modulus after the same constructive scaled-base rebase.

Direct prerequisites: le_add_left, succ_le_succ, le_scaled_nonzero, le_trans, base_le_beta_modulus. The authored body proceeds by intermediate claims (5).

Proof neighborhood

Direct dependencies

BT0012 le_add_left BT0016 succ_le_succ BT0055 le_scaled_nonzero BT000F le_trans BT0054 base_le_beta_modulus

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

36 script commands · 6 reading checkpoints · 5 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 (5)
le add leftsucc le succle scaled nonzerole transbase le beta modulus
01Fix variables and assumptionsL1–5

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

  1. L1
    intro b
  2. L2
    intro s
  3. L3
    intro C
  4. L4
    intro j
  5. L5
    intro hC
02Establish hsbL6–9

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

  1. L6
    have hsb : exists h. h + s = b + s
  2. L7
    specialize le_add_left s
  3. L8
    specialize le_add_left b
  4. L9
    exact le_add_left
03Establish hssL10–14

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

  1. L10
    have hss : exists h. h + S s = S (b + s)
  2. L11
    specialize succ_le_succ s
  3. L12
    specialize succ_le_succ (b + s)
  4. L13
    apply succ_le_succ
  5. L14
    exact hsb
04Establish hscaleL15–19

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

  1. L15
    have hscale : exists h. h + S (b + s) = C * S (b + s)
  2. L16
    specialize le_scaled_nonzero C
  3. L17
    specialize le_scaled_nonzero (S (b + s))
  4. L18
    apply le_scaled_nonzero
  5. L19
    exact hC
05Establish hsbaseL20–26

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

  1. L20
    have hsbase : exists h. h + S s = C * S (b + s)
  2. L21
    specialize le_trans (S s)
  3. L22
    specialize le_trans (S (b + s))
  4. L23
    specialize le_trans (C * S (b + s))
  5. L24
    apply le_trans
  6. L25
    exact hss
  7. L26
    exact hscale
06Establish hmodL27–36

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

  1. L27
    have hmod : exists h. h + C * S (b + s) = S ((S j) * (C * S (b + s)))
  2. L28
    specialize base_le_beta_modulus (C * S (b + s))
  3. L29
    specialize base_le_beta_modulus j
  4. L30
    exact base_le_beta_modulus
  5. L31
    specialize le_trans (S s)
  6. L32
    specialize le_trans (C * S (b + s))
  7. L33
    specialize le_trans (S ((S j) * (C * S (b + s))))
  8. L34
    apply le_trans
  9. L35
    exact hsbase
  10. L36
    exact hmod

Library-wide reading audit

Original exact command ledger · 36 lines
  1. 0001intro b
  2. 0002intro s
  3. 0003intro C
  4. 0004intro j
  5. 0005intro hC
  6. 0006have hsb : exists h. h + s = b + s
  7. 0007specialize le_add_left s
  8. 0008specialize le_add_left b
  9. 0009exact le_add_left
  10. 0010have hss : exists h. h + S s = S (b + s)
  11. 0011specialize succ_le_succ s
  12. 0012specialize succ_le_succ (b + s)
  13. 0013apply succ_le_succ
  14. 0014exact hsb
  15. 0015have hscale : exists h. h + S (b + s) = C * S (b + s)
  16. 0016specialize le_scaled_nonzero C
  17. 0017specialize le_scaled_nonzero (S (b + s))
  18. 0018apply le_scaled_nonzero
  19. 0019exact hC
  20. 0020have hsbase : exists h. h + S s = C * S (b + s)
  21. 0021specialize le_trans (S s)
  22. 0022specialize le_trans (S (b + s))
  23. 0023specialize le_trans (C * S (b + s))
  24. 0024apply le_trans
  25. 0025exact hss
  26. 0026exact hscale
  27. 0027have hmod : exists h. h + C * S (b + s) = S ((S j) * (C * S (b + s)))
  28. 0028specialize base_le_beta_modulus (C * S (b + s))
  29. 0029specialize base_le_beta_modulus j
  30. 0030exact base_le_beta_modulus
  31. 0031specialize le_trans (S s)
  32. 0032specialize le_trans (C * S (b + s))
  33. 0033specialize le_trans (S ((S j) * (C * S (b + s))))
  34. 0034apply le_trans
  35. 0035exact hsbase
  36. 0036exact hmod