PA008V

bounded_into_zero

Alpha v16 checked-use theorem · independently closed; not Stable

Every empty beta prefix is bounded into every codomain.

Exact expanded PA statement

forall b c n. (forall fom_index_wpoi_zero_bounded. (exists fom_gap_wpoi_zero_bounded_index_bound. fom_gap_wpoi_zero_bounded_index_bound + S (fom_index_wpoi_zero_bounded) = 0) -> exists fom_value_wpoi_zero_bounded. ((((exists fom_beta_height_wpoi_zero_bounded_entry. fom_beta_height_wpoi_zero_bounded_entry + S (fom_value_wpoi_zero_bounded) = S ((S (fom_index_wpoi_zero_bounded)) * c)) /\ exists fom_beta_quotient_wpoi_zero_bounded_entry. b = fom_beta_quotient_wpoi_zero_bounded_entry * S ((S (fom_index_wpoi_zero_bounded)) * c) + (fom_value_wpoi_zero_bounded))) /\ (exists fom_gap_wpoi_zero_bounded_value_bound. fom_gap_wpoi_zero_bounded_value_bound + S (fom_value_wpoi_zero_bounded) = n)))

Structural proof guide

Generated structural guide

Every empty beta prefix is bounded into every codomain.

Use the direct prerequisites add_eq_zero_right, succ_ne_zero as previously established PA formulas.

The proof proceeds by case analysis (1), intermediate claims (1).

Referenced ingredients

PA0004 add_eq_zero_right PA0005 succ_ne_zero

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero

Direct dependents

PA008X scaled_pair_order_state_zero PA00AA pair_order_state_zero

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro b
  2. 0002intro c
  3. 0003intro n
  4. 0004intro q
  5. 0005intro hq
  6. 0006exfalso
  7. 0007cases hq
  8. 0008have hsq : S q = 0
  9. 0009specialize add_eq_zero_right x
  10. 0010specialize add_eq_zero_right (S q)
  11. 0011apply add_eq_zero_right
  12. 0012exact hq_witness
  13. 0013specialize succ_ne_zero q
  14. 0014apply succ_ne_zero
  15. 0015exact hsq