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.

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.

  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