PA008Y

adjacent_scaled_orbit_history_zero

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

The explicit adjacent scaled-orbit history is empty at zero pairs.

Exact expanded PA statement

forall u v b c. (forall espi_pair_zero_history. (exists wpo_gap_zero_history_pair_bound. wpo_gap_zero_history_pair_bound + S (espi_pair_zero_history) = 0) -> exists espi_left_zero_history espi_right_zero_history. (((((exists wpo_beta_height_zero_history_left_entry. wpo_beta_height_zero_history_left_entry + S (espi_left_zero_history) = S ((S (espi_pair_zero_history + espi_pair_zero_history)) * c)) /\ exists wpo_beta_quotient_zero_history_left_entry. b = wpo_beta_quotient_zero_history_left_entry * S ((S (espi_pair_zero_history + espi_pair_zero_history)) * c) + (espi_left_zero_history))) /\ (((((exists wpo_beta_height_zero_history_right_entry. wpo_beta_height_zero_history_right_entry + S (espi_right_zero_history) = S ((S (S (espi_pair_zero_history + espi_pair_zero_history))) * c)) /\ exists wpo_beta_quotient_zero_history_right_entry. b = wpo_beta_quotient_zero_history_right_entry * S ((S (S (espi_pair_zero_history + espi_pair_zero_history))) * c) + (espi_right_zero_history))) /\ (((exists wpo_beta_height_zero_history_scaled_edge. wpo_beta_height_zero_history_scaled_edge + S (S espi_right_zero_history) = S ((S (espi_left_zero_history)) * v)) /\ exists wpo_beta_quotient_zero_history_scaled_edge. u = wpo_beta_quotient_zero_history_scaled_edge * S ((S (espi_left_zero_history)) * v) + (S espi_right_zero_history))))))))

Structural proof guide

Generated structural guide

The explicit adjacent scaled-orbit history is empty at zero pairs.

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

PA009V scaled_inverse_pair_order_paired_iteration

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 u
  2. 0002intro v
  3. 0003intro b
  4. 0004intro c
  5. 0005intro t
  6. 0006intro ht
  7. 0007exfalso
  8. 0008cases ht
  9. 0009have hst : S t = 0
  10. 0010specialize add_eq_zero_right x
  11. 0011specialize add_eq_zero_right (S t)
  12. 0012apply add_eq_zero_right
  13. 0013exact ht_witness
  14. 0014specialize succ_ne_zero t
  15. 0015apply succ_ne_zero
  16. 0016exact hst