PA00B2

prime_pair_order_paired_terminal_state_exists

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

Specialize the paired iteration to a terminal n-2 prefix with full adjacency history.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded PA statement

forall p n u v r m. p = S n -> ((~(p = 1) /\ forall wip_prime_left_wpopi_prime wip_prime_right_wpopi_prime. p = wip_prime_left_wpopi_prime * wip_prime_right_wpopi_prime -> wip_prime_left_wpopi_prime = 1 \/ wip_prime_right_wpopi_prime = 1)) -> (forall wip_index_wpopi_inverse. (exists wip_gap_wpopi_inverse_prefix_bound. wip_gap_wpopi_inverse_prefix_bound + S wip_index_wpopi_inverse = n) -> exists wip_mate_wpopi_inverse. ((((exists wip_beta_height_wpopi_inverse_decoded. wip_beta_height_wpopi_inverse_decoded + S (wip_mate_wpopi_inverse) = S ((S (wip_index_wpopi_inverse)) * v)) /\ exists wip_beta_quotient_wpopi_inverse_decoded. u = wip_beta_quotient_wpopi_inverse_decoded * S ((S (wip_index_wpopi_inverse)) * v) + (wip_mate_wpopi_inverse))) /\ ((exists wip_gap_wpopi_inverse_inverse_index_bound. wip_gap_wpopi_inverse_inverse_index_bound + S wip_index_wpopi_inverse = n) /\ ((exists wip_gap_wpopi_inverse_inverse_mate_bound. wip_gap_wpopi_inverse_inverse_mate_bound + S wip_mate_wpopi_inverse = n) /\ (exists wip_mod_left_wpopi_inverse_inverse_mod wip_mod_right_wpopi_inverse_inverse_mod. ((S wip_index_wpopi_inverse) * S wip_mate_wpopi_inverse) + p * wip_mod_left_wpopi_inverse_inverse_mod = 1 + p * wip_mod_right_wpopi_inverse_inverse_mod))))) -> n = S r -> n = S (S (m + m)) -> (exists b c. ((((forall wpo_position_wpopi_iteration_state_closed wpo_source_wpopi_iteration_state_closed wpo_mate_wpopi_iteration_state_closed. (exists wpo_gap_wpopi_iteration_state_closed_position_bound. wpo_gap_wpopi_iteration_state_closed_position_bound + S (wpo_position_wpopi_iteration_state_closed) = m + m) -> (((exists wpo_beta_height_wpopi_iteration_state_closed_source_entry. wpo_beta_height_wpopi_iteration_state_closed_source_entry + S (wpo_source_wpopi_iteration_state_closed) = S ((S (wpo_position_wpopi_iteration_state_closed)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_closed_source_entry. b = wpo_beta_quotient_wpopi_iteration_state_closed_source_entry * S ((S (wpo_position_wpopi_iteration_state_closed)) * c) + (wpo_source_wpopi_iteration_state_closed))) -> (((exists wpo_beta_height_wpopi_iteration_state_closed_inverse_entry. wpo_beta_height_wpopi_iteration_state_closed_inverse_entry + S (wpo_mate_wpopi_iteration_state_closed) = S ((S (wpo_source_wpopi_iteration_state_closed)) * v)) /\ exists wpo_beta_quotient_wpopi_iteration_state_closed_inverse_entry. u = wpo_beta_quotient_wpopi_iteration_state_closed_inverse_entry * S ((S (wpo_source_wpopi_iteration_state_closed)) * v) + (wpo_mate_wpopi_iteration_state_closed))) -> exists wpo_mate_position_wpopi_iteration_state_closed. ((exists wpo_gap_wpopi_iteration_state_closed_mate_bound. wpo_gap_wpopi_iteration_state_closed_mate_bound + S (wpo_mate_position_wpopi_iteration_state_closed) = m + m) /\ (((exists wpo_beta_height_wpopi_iteration_state_closed_mate_entry. wpo_beta_height_wpopi_iteration_state_closed_mate_entry + S (wpo_mate_wpopi_iteration_state_closed) = S ((S (wpo_mate_position_wpopi_iteration_state_closed)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_closed_mate_entry. b = wpo_beta_quotient_wpopi_iteration_state_closed_mate_entry * S ((S (wpo_mate_position_wpopi_iteration_state_closed)) * c) + (wpo_mate_wpopi_iteration_state_closed))))) /\ ((forall fom_index_wpopi_iteration_state_bounded. (exists fom_gap_wpopi_iteration_state_bounded_index_bound. fom_gap_wpopi_iteration_state_bounded_index_bound + S (fom_index_wpopi_iteration_state_bounded) = m + m) -> exists fom_value_wpopi_iteration_state_bounded. ((((exists fom_beta_height_wpopi_iteration_state_bounded_entry. fom_beta_height_wpopi_iteration_state_bounded_entry + S (fom_value_wpopi_iteration_state_bounded) = S ((S (fom_index_wpopi_iteration_state_bounded)) * c)) /\ exists fom_beta_quotient_wpopi_iteration_state_bounded_entry. b = fom_beta_quotient_wpopi_iteration_state_bounded_entry * S ((S (fom_index_wpopi_iteration_state_bounded)) * c) + (fom_value_wpopi_iteration_state_bounded))) /\ (exists fom_gap_wpopi_iteration_state_bounded_value_bound. fom_gap_wpopi_iteration_state_bounded_value_bound + S (fom_value_wpopi_iteration_state_bounded) = n))) /\ ((forall wpo_position_wpopi_iteration_state_nonendpoint wpo_value_wpopi_iteration_state_nonendpoint. (exists wpo_gap_wpopi_iteration_state_nonendpoint_position_bound. wpo_gap_wpopi_iteration_state_nonendpoint_position_bound + S (wpo_position_wpopi_iteration_state_nonendpoint) = m + m) -> (((exists wpo_beta_height_wpopi_iteration_state_nonendpoint_entry. wpo_beta_height_wpopi_iteration_state_nonendpoint_entry + S (wpo_value_wpopi_iteration_state_nonendpoint) = S ((S (wpo_position_wpopi_iteration_state_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_nonendpoint_entry. b = wpo_beta_quotient_wpopi_iteration_state_nonendpoint_entry * S ((S (wpo_position_wpopi_iteration_state_nonendpoint)) * c) + (wpo_value_wpopi_iteration_state_nonendpoint))) -> (~(wpo_value_wpopi_iteration_state_nonendpoint = 0) /\ ~((S wpo_value_wpopi_iteration_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wpopi_iteration_state_injective wpo_injective_right_wpopi_iteration_state_injective wpo_injective_value_wpopi_iteration_state_injective. (exists wpo_gap_wpopi_iteration_state_injective_left_bound. wpo_gap_wpopi_iteration_state_injective_left_bound + S (wpo_injective_left_wpopi_iteration_state_injective) = m + m) -> (exists wpo_gap_wpopi_iteration_state_injective_right_bound. wpo_gap_wpopi_iteration_state_injective_right_bound + S (wpo_injective_right_wpopi_iteration_state_injective) = m + m) -> (((exists wpo_beta_height_wpopi_iteration_state_injective_left_entry. wpo_beta_height_wpopi_iteration_state_injective_left_entry + S (wpo_injective_value_wpopi_iteration_state_injective) = S ((S (wpo_injective_left_wpopi_iteration_state_injective)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_injective_left_entry. b = wpo_beta_quotient_wpopi_iteration_state_injective_left_entry * S ((S (wpo_injective_left_wpopi_iteration_state_injective)) * c) + (wpo_injective_value_wpopi_iteration_state_injective))) -> (((exists wpo_beta_height_wpopi_iteration_state_injective_right_entry. wpo_beta_height_wpopi_iteration_state_injective_right_entry + S (wpo_injective_value_wpopi_iteration_state_injective) = S ((S (wpo_injective_right_wpopi_iteration_state_injective)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_injective_right_entry. b = wpo_beta_quotient_wpopi_iteration_state_injective_right_entry * S ((S (wpo_injective_right_wpopi_iteration_state_injective)) * c) + (wpo_injective_value_wpopi_iteration_state_injective))) -> wpo_injective_left_wpopi_iteration_state_injective = wpo_injective_right_wpopi_iteration_state_injective))))) /\ (forall wpop_pair_wpopi_iteration_history. (exists wpo_gap_wpopi_iteration_history_pair_bound. wpo_gap_wpopi_iteration_history_pair_bound + S (wpop_pair_wpopi_iteration_history) = m) -> exists wpop_left_wpopi_iteration_history wpop_right_wpopi_iteration_history. ((((exists wpo_beta_height_wpopi_iteration_history_left_entry. wpo_beta_height_wpopi_iteration_history_left_entry + S (wpop_left_wpopi_iteration_history) = S ((S (wpop_pair_wpopi_iteration_history + wpop_pair_wpopi_iteration_history)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_history_left_entry. b = wpo_beta_quotient_wpopi_iteration_history_left_entry * S ((S (wpop_pair_wpopi_iteration_history + wpop_pair_wpopi_iteration_history)) * c) + (wpop_left_wpopi_iteration_history))) /\ ((((exists wpo_beta_height_wpopi_iteration_history_right_entry. wpo_beta_height_wpopi_iteration_history_right_entry + S (wpop_right_wpopi_iteration_history) = S ((S (S (wpop_pair_wpopi_iteration_history + wpop_pair_wpopi_iteration_history))) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_history_right_entry. b = wpo_beta_quotient_wpopi_iteration_history_right_entry * S ((S (S (wpop_pair_wpopi_iteration_history + wpop_pair_wpopi_iteration_history))) * c) + (wpop_right_wpopi_iteration_history))) /\ (((exists wpo_beta_height_wpopi_iteration_history_inverse_entry. wpo_beta_height_wpopi_iteration_history_inverse_entry + S (wpop_right_wpopi_iteration_history) = S ((S (wpop_left_wpopi_iteration_history)) * v)) /\ exists wpo_beta_quotient_wpopi_iteration_history_inverse_entry. u = wpo_beta_quotient_wpopi_iteration_history_inverse_entry * S ((S (wpop_left_wpopi_iteration_history)) * v) + (wpop_right_wpopi_iteration_history))))))))

Structural proof guide

Generated structural guide

Specialize the paired iteration to a terminal n-2 prefix with full adjacency history.

Use the direct prerequisites prime_pair_order_paired_iteration, zero_add as previously established PA formulas.

The proof proceeds by intermediate claims (2), equality transport (1), certified simplification (1).

Referenced ingredients

PA00B1 prime_pair_order_paired_iteration PA0001 zero_add

Proof neighborhood

Direct dependencies

PA00B1 prime_pair_order_paired_iteration PA0001 zero_add

Direct dependents

PA00BE prime_wilson_terminal_product_package_exists

Formal native tactic body

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

Read the argument

Proof checkpoints

29 script commands · 5 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (1)
prime pair order paired iteration

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro u
  4. L4
    intro v
  5. L5
    intro r
  6. L6
    intro m
  7. L7
    intro hpn
  8. L8
    intro hp
  9. L9
    intro hprefix
  10. L10
    intro hnr
02Fix variables and assumptionsL11–11

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro hterminal
03Establish hbalanceL12–14

Establish this local claim before using it. It is not an additional assumption.

  1. L12
    have hbalance : (0 + 0) + S (S (m + m)) = n
  2. L13
    rewrite hterminal
  3. L14
    simp [zero_add]
04Establish hiterationL15–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime pair order paired iteration.

  1. L15
    have hiteration : ∀ t. ∀ q. q + q + S S (t + t) = n → ∃ x. ∃ y. (∀ z. ∀ m. ∀ k. Lt(z,t + t) → BetaAt(x,y,z,m) → BetaAt(u,v,m,k) → ContainsPrefix(x,y,t + t,k)) ∧ ((∀ z. Lt(z,t + t) → ∃ m. BetaAt(x,y,z,m) ∧ Lt(m,n)) ∧ ((∀ z. ∀ m. Lt(z,t + t) → BetaAt(x,y,z,m) → ¬m = 0 ∧ ¬S m = n) ∧ InjectivePrefix(x,y,t + t))) ∧ (∀ z. Lt(z,t) → ∃ m. ∃ k. BetaAt(x,y,z + z,m) ∧ (BetaAt(x,y,S (z + z),k) ∧ BetaAt(u,v,m,k)))Definitions: LtBetaAtInjectivePrefixContainsPrefix
  2. L16
    specialize prime_pair_order_paired_iteration p
  3. L17
    specialize prime_pair_order_paired_iteration n
  4. L18
    specialize prime_pair_order_paired_iteration u
  5. L19
    specialize prime_pair_order_paired_iteration v
  6. L20
    specialize prime_pair_order_paired_iteration r
  7. L21
    apply prime_pair_order_paired_iteration
  8. L22
    exact hpn
  9. L23
    exact hp
  10. L24
    exact hprefix
05Use earlier factsL25–29

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L25
    exact hnr
  2. L26
    specialize hiteration m
  3. L27
    specialize hiteration 0
  4. L28
    apply hiteration
  5. L29
    exact hbalance

Library-wide reading audit

Original exact command ledger · 29 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro u
  4. 0004intro v
  5. 0005intro r
  6. 0006intro m
  7. 0007intro hpn
  8. 0008intro hp
  9. 0009intro hprefix
  10. 0010intro hnr
  11. 0011intro hterminal
  12. 0012have hbalance : (0 + 0) + S (S (m + m)) = n
  13. 0013rewrite hterminal
  14. 0014simp [zero_add]
  15. 0015have hiteration : forall t q. (q + q) + S (S (t + t)) = n -> exists b c. ((((forall wpo_position_wpopi_family_state_closed wpo_source_wpopi_family_state_closed wpo_mate_wpopi_family_state_closed. (exists wpo_gap_wpopi_family_state_closed_position_bound. wpo_gap_wpopi_family_state_closed_position_bound + S (wpo_position_wpopi_family_state_closed) = t + t) -> (((exists wpo_beta_height_wpopi_family_state_closed_source_entry. wpo_beta_height_wpopi_family_state_closed_source_entry + S (wpo_source_wpopi_family_state_closed) = S ((S (wpo_position_wpopi_family_state_closed)) * c)) /\ exists wpo_beta_quotient_wpopi_family_state_closed_source_entry. b = wpo_beta_quotient_wpopi_family_state_closed_source_entry * S ((S (wpo_position_wpopi_family_state_closed)) * c) + (wpo_source_wpopi_family_state_closed))) -> (((exists wpo_beta_height_wpopi_family_state_closed_inverse_entry. wpo_beta_height_wpopi_family_state_closed_inverse_entry + S (wpo_mate_wpopi_family_state_closed) = S ((S (wpo_source_wpopi_family_state_closed)) * v)) /\ exists wpo_beta_quotient_wpopi_family_state_closed_inverse_entry. u = wpo_beta_quotient_wpopi_family_state_closed_inverse_entry * S ((S (wpo_source_wpopi_family_state_closed)) * v) + (wpo_mate_wpopi_family_state_closed))) -> exists wpo_mate_position_wpopi_family_state_closed. ((exists wpo_gap_wpopi_family_state_closed_mate_bound. wpo_gap_wpopi_family_state_closed_mate_bound + S (wpo_mate_position_wpopi_family_state_closed) = t + t) /\ (((exists wpo_beta_height_wpopi_family_state_closed_mate_entry. wpo_beta_height_wpopi_family_state_closed_mate_entry + S (wpo_mate_wpopi_family_state_closed) = S ((S (wpo_mate_position_wpopi_family_state_closed)) * c)) /\ exists wpo_beta_quotient_wpopi_family_state_closed_mate_entry. b = wpo_beta_quotient_wpopi_family_state_closed_mate_entry * S ((S (wpo_mate_position_wpopi_family_state_closed)) * c) + (wpo_mate_wpopi_family_state_closed))))) /\ ((forall fom_index_wpopi_family_state_bounded. (exists fom_gap_wpopi_family_state_bounded_index_bound. fom_gap_wpopi_family_state_bounded_index_bound + S (fom_index_wpopi_family_state_bounded) = t + t) -> exists fom_value_wpopi_family_state_bounded. ((((exists fom_beta_height_wpopi_family_state_bounded_entry. fom_beta_height_wpopi_family_state_bounded_entry + S (fom_value_wpopi_family_state_bounded) = S ((S (fom_index_wpopi_family_state_bounded)) * c)) /\ exists fom_beta_quotient_wpopi_family_state_bounded_entry. b = fom_beta_quotient_wpopi_family_state_bounded_entry * S ((S (fom_index_wpopi_family_state_bounded)) * c) + (fom_value_wpopi_family_state_bounded))) /\ (exists fom_gap_wpopi_family_state_bounded_value_bound. fom_gap_wpopi_family_state_bounded_value_bound + S (fom_value_wpopi_family_state_bounded) = n))) /\ ((forall wpo_position_wpopi_family_state_nonendpoint wpo_value_wpopi_family_state_nonendpoint. (exists wpo_gap_wpopi_family_state_nonendpoint_position_bound. wpo_gap_wpopi_family_state_nonendpoint_position_bound + S (wpo_position_wpopi_family_state_nonendpoint) = t + t) -> (((exists wpo_beta_height_wpopi_family_state_nonendpoint_entry. wpo_beta_height_wpopi_family_state_nonendpoint_entry + S (wpo_value_wpopi_family_state_nonendpoint) = S ((S (wpo_position_wpopi_family_state_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wpopi_family_state_nonendpoint_entry. b = wpo_beta_quotient_wpopi_family_state_nonendpoint_entry * S ((S (wpo_position_wpopi_family_state_nonendpoint)) * c) + (wpo_value_wpopi_family_state_nonendpoint))) -> (~(wpo_value_wpopi_family_state_nonendpoint = 0) /\ ~((S wpo_value_wpopi_family_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wpopi_family_state_injective wpo_injective_right_wpopi_family_state_injective wpo_injective_value_wpopi_family_state_injective. (exists wpo_gap_wpopi_family_state_injective_left_bound. wpo_gap_wpopi_family_state_injective_left_bound + S (wpo_injective_left_wpopi_family_state_injective) = t + t) -> (exists wpo_gap_wpopi_family_state_injective_right_bound. wpo_gap_wpopi_family_state_injective_right_bound + S (wpo_injective_right_wpopi_family_state_injective) = t + t) -> (((exists wpo_beta_height_wpopi_family_state_injective_left_entry. wpo_beta_height_wpopi_family_state_injective_left_entry + S (wpo_injective_value_wpopi_family_state_injective) = S ((S (wpo_injective_left_wpopi_family_state_injective)) * c)) /\ exists wpo_beta_quotient_wpopi_family_state_injective_left_entry. b = wpo_beta_quotient_wpopi_family_state_injective_left_entry * S ((S (wpo_injective_left_wpopi_family_state_injective)) * c) + (wpo_injective_value_wpopi_family_state_injective))) -> (((exists wpo_beta_height_wpopi_family_state_injective_right_entry. wpo_beta_height_wpopi_family_state_injective_right_entry + S (wpo_injective_value_wpopi_family_state_injective) = S ((S (wpo_injective_right_wpopi_family_state_injective)) * c)) /\ exists wpo_beta_quotient_wpopi_family_state_injective_right_entry. b = wpo_beta_quotient_wpopi_family_state_injective_right_entry * S ((S (wpo_injective_right_wpopi_family_state_injective)) * c) + (wpo_injective_value_wpopi_family_state_injective))) -> wpo_injective_left_wpopi_family_state_injective = wpo_injective_right_wpopi_family_state_injective))))) /\ (forall wpop_pair_wpopi_family_history. (exists wpo_gap_wpopi_family_history_pair_bound. wpo_gap_wpopi_family_history_pair_bound + S (wpop_pair_wpopi_family_history) = t) -> exists wpop_left_wpopi_family_history wpop_right_wpopi_family_history. ((((exists wpo_beta_height_wpopi_family_history_left_entry. wpo_beta_height_wpopi_family_history_left_entry + S (wpop_left_wpopi_family_history) = S ((S (wpop_pair_wpopi_family_history + wpop_pair_wpopi_family_history)) * c)) /\ exists wpo_beta_quotient_wpopi_family_history_left_entry. b = wpo_beta_quotient_wpopi_family_history_left_entry * S ((S (wpop_pair_wpopi_family_history + wpop_pair_wpopi_family_history)) * c) + (wpop_left_wpopi_family_history))) /\ ((((exists wpo_beta_height_wpopi_family_history_right_entry. wpo_beta_height_wpopi_family_history_right_entry + S (wpop_right_wpopi_family_history) = S ((S (S (wpop_pair_wpopi_family_history + wpop_pair_wpopi_family_history))) * c)) /\ exists wpo_beta_quotient_wpopi_family_history_right_entry. b = wpo_beta_quotient_wpopi_family_history_right_entry * S ((S (S (wpop_pair_wpopi_family_history + wpop_pair_wpopi_family_history))) * c) + (wpop_right_wpopi_family_history))) /\ (((exists wpo_beta_height_wpopi_family_history_inverse_entry. wpo_beta_height_wpopi_family_history_inverse_entry + S (wpop_right_wpopi_family_history) = S ((S (wpop_left_wpopi_family_history)) * v)) /\ exists wpo_beta_quotient_wpopi_family_history_inverse_entry. u = wpo_beta_quotient_wpopi_family_history_inverse_entry * S ((S (wpop_left_wpopi_family_history)) * v) + (wpop_right_wpopi_family_history)))))))
  16. 0016specialize prime_pair_order_paired_iteration p
  17. 0017specialize prime_pair_order_paired_iteration n
  18. 0018specialize prime_pair_order_paired_iteration u
  19. 0019specialize prime_pair_order_paired_iteration v
  20. 0020specialize prime_pair_order_paired_iteration r
  21. 0021apply prime_pair_order_paired_iteration
  22. 0022exact hpn
  23. 0023exact hp
  24. 0024exact hprefix
  25. 0025exact hnr
  26. 0026specialize hiteration m
  27. 0027specialize hiteration 0
  28. 0028apply hiteration
  29. 0029exact hbalance