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.

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 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.

Read the argument

Proof checkpoints

54 script commands · 8 reading checkpoints · 7 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 (6)
beta value le codele add rightsucc le succle transle scaled nonzerobase le beta modulus
01Fix variables and assumptionsL1–9

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro i
  4. L4
    intro x
  5. L5
    intro C
  6. L6
    intro s
  7. L7
    intro j
  8. L8
    intro hat
  9. L9
    intro hC
02Establish hxbL10–16

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

  1. L10
    have hxb : exists h. h + x = b
  2. L11
    specialize beta_value_le_code b
  3. L12
    specialize beta_value_le_code c
  4. L13
    specialize beta_value_le_code i
  5. L14
    specialize beta_value_le_code x
  6. L15
    apply beta_value_le_code
  7. L16
    exact hat
03Establish hbsL17–20

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

  1. L17
    have hbs : exists h. h + b = b + s
  2. L18
    specialize le_add_right b
  3. L19
    specialize le_add_right s
  4. L20
    exact le_add_right
04Establish hxsL21–27

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

  1. L21
    have hxs : exists h. h + x = b + s
  2. L22
    specialize le_trans x
  3. L23
    specialize le_trans b
  4. L24
    specialize le_trans (b + s)
  5. L25
    apply le_trans
  6. L26
    exact hxb
  7. L27
    exact hbs
05Establish hsxL28–32

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

  1. L28
    have hsx : exists h. h + S x = S (b + s)
  2. L29
    specialize succ_le_succ x
  3. L30
    specialize succ_le_succ (b + s)
  4. L31
    apply succ_le_succ
  5. L32
    exact hxs
06Establish hscaleL33–37

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

  1. L33
    have hscale : exists h. h + S (b + s) = C * S (b + s)
  2. L34
    specialize le_scaled_nonzero C
  3. L35
    specialize le_scaled_nonzero (S (b + s))
  4. L36
    apply le_scaled_nonzero
  5. L37
    exact hC
07Establish hxbaseL38–44

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

  1. L38
    have hxbase : exists h. h + S x = C * S (b + s)
  2. L39
    specialize le_trans (S x)
  3. L40
    specialize le_trans (S (b + s))
  4. L41
    specialize le_trans (C * S (b + s))
  5. L42
    apply le_trans
  6. L43
    exact hsx
  7. L44
    exact hscale
08Establish hmodL45–54

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

  1. L45
    have hmod : exists h. h + C * S (b + s) = S ((S j) * (C * S (b + s)))
  2. L46
    specialize base_le_beta_modulus (C * S (b + s))
  3. L47
    specialize base_le_beta_modulus j
  4. L48
    exact base_le_beta_modulus
  5. L49
    specialize le_trans (S x)
  6. L50
    specialize le_trans (C * S (b + s))
  7. L51
    specialize le_trans (S ((S j) * (C * S (b + s))))
  8. L52
    apply le_trans
  9. L53
    exact hxbase
  10. L54
    exact hmod

Library-wide reading audit

Original exact command ledger · 54 lines
  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