PA003E

beta_at_self_of_bound

Stable checked-use theorem · independently closed

A value below a Gödel-beta modulus decodes to itself when used as the code.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

A value below a Gödel-beta modulus decodes to itself when used as the code.

Use the direct prerequisites mul_zero_left, zero_add as previously established PA formulas.

The proof proceeds by equality transport (2).

Referenced ingredients

PA000D mul_zero_left PA0001 zero_add

Proof neighborhood

Direct dependencies

PA000D mul_zero_left PA0001 zero_add

Direct dependents

PA003G beta_prefix_sum_trace_exists PA003W beta_prefix_product_trace_exists

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 c
  2. 0002intro i
  3. 0003intro x
  4. 0004intro hx
  5. 0005split
  6. 0006exact hx
  7. 0007exists 0
  8. 0008specialize mul_zero_left (S ((S i) * c))
  9. 0009rewrite mul_zero_left
  10. 0010specialize zero_add x
  11. 0011rewrite zero_add
  12. 0012refl