PA008X — scaled_pair_order_state

Exact expanded PA statement

forall u v n. exists b c. (((forall espo_position_zero_state_closed espo_source_zero_state_closed espo_mate_zero_state_closed. (exists wpo_gap_zero_state_closed_position_bound. wpo_gap_zero_state_closed_position_bound + S (espo_position_zero_state_closed) = 0) -> (((exists wpo_beta_height_zero_state_closed_source_entry. wpo_beta_height_zero_state_closed_source_entry + S (espo_source_zero_state_closed) = S ((S (espo_position_zero_state_closed)) * c)) /\ exists wpo_beta_quotient_zero_state_closed_source_entry. b = wpo_beta_quotient_zero_state_closed_source_entry * S ((S (espo_position_zero_state_closed)) * c) + (espo_source_zero_state_closed))) -> (((exists wpo_beta_height_zero_state_closed_scaled_entry. wpo_beta_height_zero_state_closed_scaled_entry + S (S espo_mate_zero_state_closed) = S ((S (espo_source_zero_state_closed)) * v)) /\ exists wpo_beta_quotient_zero_state_closed_scaled_entry. u = wpo_beta_quotient_zero_state_closed_scaled_entry * S ((S (espo_source_zero_state_closed)) * v) + (S espo_mate_zero_state_closed))) -> exists espo_mate_position_zero_state_closed. ((exists wpo_gap_zero_state_closed_mate_bound. wpo_gap_zero_state_closed_mate_bound + S (espo_mate_position_zero_state_closed) = 0) /\ (((exists wpo_beta_height_zero_state_closed_mate_entry. wpo_beta_height_zero_state_closed_mate_entry + S (espo_mate_zero_state_closed) = S ((S (espo_mate_position_zero_state_closed)) * c)) /\ exists wpo_beta_quotient_zero_state_closed_mate_entry. b = wpo_beta_quotient_zero_state_closed_mate_entry * S ((S (espo_mate_position_zero_state_closed)) * c) + (espo_mate_zero_state_closed))))) /\ (((forall fom_index_zero_state_bounded. (exists fom_gap_zero_state_bounded_index_bound. fom_gap_zero_state_bounded_index_bound + S (fom_index_zero_state_bounded) = 0) -> exists fom_value_zero_state_bounded. ((((exists fom_beta_height_zero_state_bounded_entry. fom_beta_height_zero_state_bounded_entry + S (fom_value_zero_state_bounded) = S ((S (fom_index_zero_state_bounded)) * c)) /\ exists fom_beta_quotient_zero_state_bounded_entry. b = fom_beta_quotient_zero_state_bounded_entry * S ((S (fom_index_zero_state_bounded)) * c) + (fom_value_zero_state_bounded))) /\ (exists fom_gap_zero_state_bounded_value_bound. fom_gap_zero_state_bounded_value_bound + S (fom_value_zero_state_bounded) = n))) /\ (forall wpo_injective_left_zero_state_injective wpo_injective_right_zero_state_injective wpo_injective_value_zero_state_injective. (exists wpo_gap_zero_state_injective_left_bound. wpo_gap_zero_state_injective_left_bound + S (wpo_injective_left_zero_state_injective) = 0) -> (exists wpo_gap_zero_state_injective_right_bound. wpo_gap_zero_state_injective_right_bound + S (wpo_injective_right_zero_state_injective) = 0) -> (((exists wpo_beta_height_zero_state_injective_left_entry. wpo_beta_height_zero_state_injective_left_entry + S (wpo_injective_value_zero_state_injective) = S ((S (wpo_injective_left_zero_state_injective)) * c)) /\ exists wpo_beta_quotient_zero_state_injective_left_entry. b = wpo_beta_quotient_zero_state_injective_left_entry * S ((S (wpo_injective_left_zero_state_injective)) * c) + (wpo_injective_value_zero_state_injective))) -> (((exists wpo_beta_height_zero_state_injective_right_entry. wpo_beta_height_zero_state_injective_right_entry + S (wpo_injective_value_zero_state_injective) = S ((S (wpo_injective_right_zero_state_injective)) * c)) /\ exists wpo_beta_quotient_zero_state_injective_right_entry. b = wpo_beta_quotient_zero_state_injective_right_entry * S ((S (wpo_injective_right_zero_state_injective)) * c) + (wpo_injective_value_zero_state_injective))) -> wpo_injective_left_zero_state_injective = wpo_injective_right_zero_state_injective)))))

Structural proof guide

Generated structural guide

Zero codes witness the empty shifted, bounded, injective state.

Use the direct prerequisites scaled_orbit_closed_prefix_zero, bounded_into_zero, injective_prefix_zero as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA008U scaled_orbit_closed_prefix_zero PA008V bounded_into_zero PA008W injective_prefix_zero

Proof neighborhood

Direct dependencies

PA008U scaled_orbit_closed_prefix_zero PA008V bounded_into_zero PA008W injective_prefix_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.