BT0040

beta_at_self_of_bound

Stable · empty-context checked

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

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

Direct prerequisites: mul_zero_left, zero_add. The authored body proceeds by equality transport (2).

Proof neighborhood

Direct dependencies

BT0004 mul_zero_left BT0000 zero_add

Direct dependents

BT005E beta_prefix_product_trace_exists BT0089 beta_prefix_sum_trace_exists

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  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