BT0053

beta_value_le_code

Stable · empty-context checked

Every decoded beta value is at most its code.

Exact expanded PA statement

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

Structural proof guide

Every decoded beta value is at most its code.

Direct prerequisites: none. The authored body proceeds by case analysis (2).

Proof neighborhood

Direct dependencies

none

Direct dependents

BT0057 beta_value_lt_scaled_base

Formal native tactic body

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

  1. 0001intro b
  2. 0002intro c
  3. 0003intro i
  4. 0004intro x
  5. 0005intro hat
  6. 0006cases hat
  7. 0007cases hat_right
  8. 0008exists x1 * S ((S i) * c)
  9. 0009symm
  10. 0010exact hat_right_witness