BT003Y

beta_modulus_nonzero

Stable · empty-context checked

Every Gödel-beta decoding modulus is nonzero.

Exact expanded PA statement

forall c i. ~(S ((S i) * c) = 0)

Structural proof guide

Every Gödel-beta decoding modulus is nonzero.

Direct prerequisites: succ_ne_zero. The authored body proceeds by direct introduction and elimination.

Proof neighborhood

Direct dependencies

BT000C succ_ne_zero

Direct dependents

BT0041 beta_at_exists BT0045 beta_at_of_mod_eq_bound BT0059 beta_exclusive_accumulated_product_step BT005A beta_exclusive_recode_congruence_step BT005D beta_prefix_extend

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. 0003specialize succ_ne_zero ((S i) * c)
  4. 0004exact succ_ne_zero