PA002T

beta_value_lt_scaled_base

Stable checked-use theorem · independently closed

An old beta value fits every modulus after a constructive scaled-base rebase.

Exact expanded PA statement

forall b c i x C s j. ((exists h. h + S x = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + x) -> ~(C = 0) -> exists h. h + S x = S ((S j) * (C * S (b + s)))

Structural proof guide

Generated structural guide

An old beta value fits every modulus after a constructive scaled-base rebase.

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

The proof proceeds by intermediate claims (7).

Referenced ingredients

PA002R beta_value_le_code PA002S le_add_right PA002K succ_le_succ PA000R le_trans PA002N le_scaled_nonzero PA002P base_le_beta_modulus

Proof neighborhood

Direct dependencies

PA002R beta_value_le_code PA002S le_add_right PA002K succ_le_succ PA000R le_trans PA002N le_scaled_nonzero 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 c
  3. 0003intro i
  4. 0004intro x
  5. 0005intro C
  6. 0006intro s
  7. 0007intro j
  8. 0008intro hat
  9. 0009intro hC
  10. 0010have hxb : exists h. h + x = b
  11. 0011specialize beta_value_le_code b
  12. 0012specialize beta_value_le_code c
  13. 0013specialize beta_value_le_code i
  14. 0014specialize beta_value_le_code x
  15. 0015apply beta_value_le_code
  16. 0016exact hat
  17. 0017have hbs : exists h. h + b = b + s
  18. 0018specialize le_add_right b
  19. 0019specialize le_add_right s
  20. 0020exact le_add_right
  21. 0021have hxs : exists h. h + x = b + s
  22. 0022specialize le_trans x
  23. 0023specialize le_trans b
  24. 0024specialize le_trans (b + s)
  25. 0025apply le_trans
  26. 0026exact hxb
  27. 0027exact hbs
  28. 0028have hsx : exists h. h + S x = S (b + s)
  29. 0029specialize succ_le_succ x
  30. 0030specialize succ_le_succ (b + s)
  31. 0031apply succ_le_succ
  32. 0032exact hxs
  33. 0033have hscale : exists h. h + S (b + s) = C * S (b + s)
  34. 0034specialize le_scaled_nonzero C
  35. 0035specialize le_scaled_nonzero (S (b + s))
  36. 0036apply le_scaled_nonzero
  37. 0037exact hC
  38. 0038have hxbase : exists h. h + S x = C * S (b + s)
  39. 0039specialize le_trans (S x)
  40. 0040specialize le_trans (S (b + s))
  41. 0041specialize le_trans (C * S (b + s))
  42. 0042apply le_trans
  43. 0043exact hsx
  44. 0044exact hscale
  45. 0045have hmod : exists h. h + C * S (b + s) = S ((S j) * (C * S (b + s)))
  46. 0046specialize base_le_beta_modulus (C * S (b + s))
  47. 0047specialize base_le_beta_modulus j
  48. 0048exact base_le_beta_modulus
  49. 0049specialize le_trans (S x)
  50. 0050specialize le_trans (C * S (b + s))
  51. 0051specialize le_trans (S ((S j) * (C * S (b + s))))
  52. 0052apply le_trans
  53. 0053exact hxbase
  54. 0054exact hmod