PA002Q

new_value_lt_scaled_base

Stable checked-use theorem · independently closed

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

Generated structural guide

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

Use the direct prerequisites le_add_left, succ_le_succ, le_scaled_nonzero, le_trans, base_le_beta_modulus as previously established PA formulas.

The proof proceeds by intermediate claims (5).

Referenced ingredients

PA002J le_add_left PA002K succ_le_succ PA002N le_scaled_nonzero PA000R le_trans PA002P base_le_beta_modulus

Proof neighborhood

Direct dependencies

PA002J le_add_left PA002K succ_le_succ PA002N le_scaled_nonzero PA000R le_trans PA002P base_le_beta_modulus

Direct dependents

PA002X beta_prefix_extend

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

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