PA002W

beta_at_of_mod_eq_bound

Stable checked-use theorem · independently closed

A bounded value congruent to a code is its expanded Gödel-beta value.

Exact expanded PA statement

forall b c i x. (exists h. h + S x = S ((S i) * c)) -> (exists u v. b + S ((S i) * c) * u = x + S ((S i) * c) * v) -> ((exists h. h + S x = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + x)

Structural proof guide

Generated structural guide

A bounded value congruent to a code is its expanded Gödel-beta value.

Use the direct prerequisites beta_modulus_nonzero, mod_eq_to_remainder_decomposition as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA000U beta_modulus_nonzero PA002V mod_eq_to_remainder_decomposition

Proof neighborhood

Direct dependencies

PA000U beta_modulus_nonzero PA002V mod_eq_to_remainder_decomposition

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 hx
  6. 0006intro hmod
  7. 0007split
  8. 0008exact hx
  9. 0009specialize mod_eq_to_remainder_decomposition (S ((S i) * c))
  10. 0010specialize mod_eq_to_remainder_decomposition b
  11. 0011specialize mod_eq_to_remainder_decomposition x
  12. 0012apply mod_eq_to_remainder_decomposition
  13. 0013specialize beta_modulus_nonzero c
  14. 0014specialize beta_modulus_nonzero i
  15. 0015exact beta_modulus_nonzero
  16. 0016exact hx
  17. 0017exact hmod