PA009W · theorem

scaled_inverse_pair_order_terminal_package

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

At n=h+h, package a complete adjacent scaled-orbit order of length n.

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.

Statement with defined notation

∀ p. ∀ a. ∀ n. ∀ u. ∀ v. ∀ h. p = S n → Prime(p) → ¬QRes(p,a) → ScaledInversePrefix(p,a,n,u,v,n) → n = h + h → ∃ x. ∃ y. (∀ z. ∀ m. ∀ k. Lt(z,h + h) → BetaAt(x,y,z,m) → BetaAt(u,v,m,S k) → ContainsPrefix(x,y,h + h,k)) ∧ ((∀ z. Lt(z,h + h) → ∃ m. BetaAt(x,y,z,m) ∧ Lt(m,n)) ∧ InjectivePrefix(x,y,h + h)) ∧ (∀ z. Lt(z,h) → ∃ m. ∃ k. BetaAt(x,y,z + z,m) ∧ (BetaAt(x,y,S (z + z),k) ∧ BetaAt(u,v,m,S k)))

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0004 Prime PD0013 BetaAt PD0021 QRes PD0025 InjectivePrefix PD0027 ContainsPrefix PD0039 ScaledInversePrefix

15 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0025 InjectivePrefix PD0027 ContainsPrefix

12 occurrences

Exact expanded native-PA statement
forall p a n u v h. p = S n -> ((~(p = 1) /\ forall esi_prime_left_iteration_prime esi_prime_right_iteration_prime. p = esi_prime_left_iteration_prime * esi_prime_right_iteration_prime -> esi_prime_left_iteration_prime = 1 \/ esi_prime_right_iteration_prime = 1)) -> ~(exists qr_x_iteration_nonresidue. exists qr_u_iteration_nonresidue qr_v_iteration_nonresidue. qr_x_iteration_nonresidue * qr_x_iteration_nonresidue + p * qr_u_iteration_nonresidue = a + p * qr_v_iteration_nonresidue) -> (forall esip_index_iteration_prefix. (exists esip_gap_iteration_prefix_prefix_bound. esip_gap_iteration_prefix_prefix_bound + S (esip_index_iteration_prefix) = n) -> exists esip_mate_iteration_prefix. ((((exists ff_h_esip_iteration_prefix_entry. ff_h_esip_iteration_prefix_entry + S (esip_mate_iteration_prefix) = S ((S (esip_index_iteration_prefix)) * v)) /\ exists ff_q_esip_iteration_prefix_entry. u = ff_q_esip_iteration_prefix_entry * S ((S (esip_index_iteration_prefix)) * v) + (esip_mate_iteration_prefix))) /\ ((exists esip_gap_iteration_prefix_relation_index_bound. esip_gap_iteration_prefix_relation_index_bound + S (esip_index_iteration_prefix) = n) /\ ((((~((S esip_index_iteration_prefix) = 0) /\ (exists esip_gap_iteration_prefix_relation_scaled_left_bound. esip_gap_iteration_prefix_relation_scaled_left_bound + S (S esip_index_iteration_prefix) = p))) /\ (((~(esip_mate_iteration_prefix = 0) /\ (exists esip_gap_iteration_prefix_relation_scaled_right_bound. esip_gap_iteration_prefix_relation_scaled_right_bound + S (esip_mate_iteration_prefix) = p))) /\ (exists esi_mod_left_iteration_prefix_relation_scaled_mod esi_mod_right_iteration_prefix_relation_scaled_mod. ((S esip_index_iteration_prefix) * esip_mate_iteration_prefix) + p * esi_mod_left_iteration_prefix_relation_scaled_mod = (a) + p * esi_mod_right_iteration_prefix_relation_scaled_mod))))))) -> n = h + h -> (exists b c. (((((forall espo_position_terminal_state_closed espo_source_terminal_state_closed espo_mate_terminal_state_closed. (exists wpo_gap_terminal_state_closed_position_bound. wpo_gap_terminal_state_closed_position_bound + S (espo_position_terminal_state_closed) = h + h) -> (((exists wpo_beta_height_terminal_state_closed_source_entry. wpo_beta_height_terminal_state_closed_source_entry + S (espo_source_terminal_state_closed) = S ((S (espo_position_terminal_state_closed)) * c)) /\ exists wpo_beta_quotient_terminal_state_closed_source_entry. b = wpo_beta_quotient_terminal_state_closed_source_entry * S ((S (espo_position_terminal_state_closed)) * c) + (espo_source_terminal_state_closed))) -> (((exists wpo_beta_height_terminal_state_closed_scaled_entry. wpo_beta_height_terminal_state_closed_scaled_entry + S (S espo_mate_terminal_state_closed) = S ((S (espo_source_terminal_state_closed)) * v)) /\ exists wpo_beta_quotient_terminal_state_closed_scaled_entry. u = wpo_beta_quotient_terminal_state_closed_scaled_entry * S ((S (espo_source_terminal_state_closed)) * v) + (S espo_mate_terminal_state_closed))) -> exists espo_mate_position_terminal_state_closed. ((exists wpo_gap_terminal_state_closed_mate_bound. wpo_gap_terminal_state_closed_mate_bound + S (espo_mate_position_terminal_state_closed) = h + h) /\ (((exists wpo_beta_height_terminal_state_closed_mate_entry. wpo_beta_height_terminal_state_closed_mate_entry + S (espo_mate_terminal_state_closed) = S ((S (espo_mate_position_terminal_state_closed)) * c)) /\ exists wpo_beta_quotient_terminal_state_closed_mate_entry. b = wpo_beta_quotient_terminal_state_closed_mate_entry * S ((S (espo_mate_position_terminal_state_closed)) * c) + (espo_mate_terminal_state_closed))))) /\ (((forall fom_index_terminal_state_bounded. (exists fom_gap_terminal_state_bounded_index_bound. fom_gap_terminal_state_bounded_index_bound + S (fom_index_terminal_state_bounded) = h + h) -> exists fom_value_terminal_state_bounded. ((((exists fom_beta_height_terminal_state_bounded_entry. fom_beta_height_terminal_state_bounded_entry + S (fom_value_terminal_state_bounded) = S ((S (fom_index_terminal_state_bounded)) * c)) /\ exists fom_beta_quotient_terminal_state_bounded_entry. b = fom_beta_quotient_terminal_state_bounded_entry * S ((S (fom_index_terminal_state_bounded)) * c) + (fom_value_terminal_state_bounded))) /\ (exists fom_gap_terminal_state_bounded_value_bound. fom_gap_terminal_state_bounded_value_bound + S (fom_value_terminal_state_bounded) = n))) /\ (forall wpo_injective_left_terminal_state_injective wpo_injective_right_terminal_state_injective wpo_injective_value_terminal_state_injective. (exists wpo_gap_terminal_state_injective_left_bound. wpo_gap_terminal_state_injective_left_bound + S (wpo_injective_left_terminal_state_injective) = h + h) -> (exists wpo_gap_terminal_state_injective_right_bound. wpo_gap_terminal_state_injective_right_bound + S (wpo_injective_right_terminal_state_injective) = h + h) -> (((exists wpo_beta_height_terminal_state_injective_left_entry. wpo_beta_height_terminal_state_injective_left_entry + S (wpo_injective_value_terminal_state_injective) = S ((S (wpo_injective_left_terminal_state_injective)) * c)) /\ exists wpo_beta_quotient_terminal_state_injective_left_entry. b = wpo_beta_quotient_terminal_state_injective_left_entry * S ((S (wpo_injective_left_terminal_state_injective)) * c) + (wpo_injective_value_terminal_state_injective))) -> (((exists wpo_beta_height_terminal_state_injective_right_entry. wpo_beta_height_terminal_state_injective_right_entry + S (wpo_injective_value_terminal_state_injective) = S ((S (wpo_injective_right_terminal_state_injective)) * c)) /\ exists wpo_beta_quotient_terminal_state_injective_right_entry. b = wpo_beta_quotient_terminal_state_injective_right_entry * S ((S (wpo_injective_right_terminal_state_injective)) * c) + (wpo_injective_value_terminal_state_injective))) -> wpo_injective_left_terminal_state_injective = wpo_injective_right_terminal_state_injective))))) /\ (forall espi_pair_terminal_history. (exists wpo_gap_terminal_history_pair_bound. wpo_gap_terminal_history_pair_bound + S (espi_pair_terminal_history) = h) -> exists espi_left_terminal_history espi_right_terminal_history. (((((exists wpo_beta_height_terminal_history_left_entry. wpo_beta_height_terminal_history_left_entry + S (espi_left_terminal_history) = S ((S (espi_pair_terminal_history + espi_pair_terminal_history)) * c)) /\ exists wpo_beta_quotient_terminal_history_left_entry. b = wpo_beta_quotient_terminal_history_left_entry * S ((S (espi_pair_terminal_history + espi_pair_terminal_history)) * c) + (espi_left_terminal_history))) /\ (((((exists wpo_beta_height_terminal_history_right_entry. wpo_beta_height_terminal_history_right_entry + S (espi_right_terminal_history) = S ((S (S (espi_pair_terminal_history + espi_pair_terminal_history))) * c)) /\ exists wpo_beta_quotient_terminal_history_right_entry. b = wpo_beta_quotient_terminal_history_right_entry * S ((S (S (espi_pair_terminal_history + espi_pair_terminal_history))) * c) + (espi_right_terminal_history))) /\ (((exists wpo_beta_height_terminal_history_scaled_edge. wpo_beta_height_terminal_history_scaled_edge + S (S espi_right_terminal_history) = S ((S (espi_left_terminal_history)) * v)) /\ exists wpo_beta_quotient_terminal_history_scaled_edge. u = wpo_beta_quotient_terminal_history_scaled_edge * S ((S (espi_left_terminal_history)) * v) + (S espi_right_terminal_history)))))))))))

Proof neighborhood

Direct theorem prerequisites

PA009V scaled_inverse_pair_order_paired_iteration

Direct theorem dependents

PA00BL scaled_inverse_nonresidue_half_power_mod_predecessor

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
scaled inverse pair order paired iteration
01Fix variables and assumptionsL1–10

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

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

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

  1. L11
    intro heven
03Establish hbalanceL12–14

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

  1. L12
    have hbalance : (h + h) + (0 + 0) = n
  2. L13
    rewrite heven
  3. L14
    simp
04Establish hallL15–24

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

  1. L15
    have hall : ∀ m. ∀ k. m + m + (k + k) = n → ∃ x. ∃ y. (∀ z. ∀ i. ∀ j. Lt(z,m + m) → BetaAt(x,y,z,i) → BetaAt(u,v,i,S j) → ContainsPrefix(x,y,m + m,j)) ∧ ((∀ z. Lt(z,m + m) → ∃ i. BetaAt(x,y,z,i) ∧ Lt(i,n)) ∧ InjectivePrefix(x,y,m + m)) ∧ (∀ z. Lt(z,m) → ∃ i. ∃ j. BetaAt(x,y,z + z,i) ∧ (BetaAt(x,y,S (z + z),j) ∧ BetaAt(u,v,i,S j)))Definitions: Lt(z,m + m)BetaAt(x,y,z,i)BetaAt(u,v,i,S j)ContainsPrefix(x,y,m + m,j)Lt(i,n)InjectivePrefix(x,y,m + m)Lt(z,m)BetaAt(x,y,z + z,i)BetaAt(x,y,S (z + z),j)Original native command in the exact edition
  2. L16
    specialize scaled_inverse_pair_order_paired_iteration p
  3. L17
    specialize scaled_inverse_pair_order_paired_iteration a
  4. L18
    specialize scaled_inverse_pair_order_paired_iteration n
  5. L19
    specialize scaled_inverse_pair_order_paired_iteration u
  6. L20
    specialize scaled_inverse_pair_order_paired_iteration v
  7. L21
    apply scaled_inverse_pair_order_paired_iteration
  8. L22
    exact hpn
  9. L23
    exact hp
  10. L24
    exact hnotqres
05Use earlier factsL25–29

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

  1. L25
    exact hprefix
  2. L26
    specialize hall h
  3. L27
    specialize hall 0
  4. L28
    apply hall
  5. L29
    exact hbalance

Library-wide reading audit

Original defined command ledger · 29 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro n
  4. 0004intro u
  5. 0005intro v
  6. 0006intro h
  7. 0007intro hpn
  8. 0008intro hp
  9. 0009intro hnotqres
  10. 0010intro hprefix
  11. 0011intro heven
  12. 0012have hbalance : (h + h) + (0 + 0) = n
  13. 0013rewrite heven
  14. 0014simp
  15. 0015have hall : ∀ m. ∀ k. m + m + (k + k) = n → ∃ x. ∃ y. (∀ z. ∀ i. ∀ j. Lt(z,m + m) → BetaAt(x,y,z,i) → BetaAt(u,v,i,S j) → ContainsPrefix(x,y,m + m,j)) ∧ ((∀ z. Lt(z,m + m) → ∃ i. BetaAt(x,y,z,i) ∧ Lt(i,n)) ∧ InjectivePrefix(x,y,m + m)) ∧ (∀ z. Lt(z,m) → ∃ i. ∃ j. BetaAt(x,y,z + z,i) ∧ (BetaAt(x,y,S (z + z),j) ∧ BetaAt(u,v,i,S j)))
    Exact native replay linehave hall : forall m k. (m + m) + (k + k) = n -> (exists b c. (((((forall espo_position_iteration_state_closed espo_source_iteration_state_closed espo_mate_iteration_state_closed. (exists wpo_gap_iteration_state_closed_position_bound. wpo_gap_iteration_state_closed_position_bound + S (espo_position_iteration_state_closed) = m + m) -> (((exists wpo_beta_height_iteration_state_closed_source_entry. wpo_beta_height_iteration_state_closed_source_entry + S (espo_source_iteration_state_closed) = S ((S (espo_position_iteration_state_closed)) * c)) /\ exists wpo_beta_quotient_iteration_state_closed_source_entry. b = wpo_beta_quotient_iteration_state_closed_source_entry * S ((S (espo_position_iteration_state_closed)) * c) + (espo_source_iteration_state_closed))) -> (((exists wpo_beta_height_iteration_state_closed_scaled_entry. wpo_beta_height_iteration_state_closed_scaled_entry + S (S espo_mate_iteration_state_closed) = S ((S (espo_source_iteration_state_closed)) * v)) /\ exists wpo_beta_quotient_iteration_state_closed_scaled_entry. u = wpo_beta_quotient_iteration_state_closed_scaled_entry * S ((S (espo_source_iteration_state_closed)) * v) + (S espo_mate_iteration_state_closed))) -> exists espo_mate_position_iteration_state_closed. ((exists wpo_gap_iteration_state_closed_mate_bound. wpo_gap_iteration_state_closed_mate_bound + S (espo_mate_position_iteration_state_closed) = m + m) /\ (((exists wpo_beta_height_iteration_state_closed_mate_entry. wpo_beta_height_iteration_state_closed_mate_entry + S (espo_mate_iteration_state_closed) = S ((S (espo_mate_position_iteration_state_closed)) * c)) /\ exists wpo_beta_quotient_iteration_state_closed_mate_entry. b = wpo_beta_quotient_iteration_state_closed_mate_entry * S ((S (espo_mate_position_iteration_state_closed)) * c) + (espo_mate_iteration_state_closed))))) /\ (((forall fom_index_iteration_state_bounded. (exists fom_gap_iteration_state_bounded_index_bound. fom_gap_iteration_state_bounded_index_bound + S (fom_index_iteration_state_bounded) = m + m) -> exists fom_value_iteration_state_bounded. ((((exists fom_beta_height_iteration_state_bounded_entry. fom_beta_height_iteration_state_bounded_entry + S (fom_value_iteration_state_bounded) = S ((S (fom_index_iteration_state_bounded)) * c)) /\ exists fom_beta_quotient_iteration_state_bounded_entry. b = fom_beta_quotient_iteration_state_bounded_entry * S ((S (fom_index_iteration_state_bounded)) * c) + (fom_value_iteration_state_bounded))) /\ (exists fom_gap_iteration_state_bounded_value_bound. fom_gap_iteration_state_bounded_value_bound + S (fom_value_iteration_state_bounded) = n))) /\ (forall wpo_injective_left_iteration_state_injective wpo_injective_right_iteration_state_injective wpo_injective_value_iteration_state_injective. (exists wpo_gap_iteration_state_injective_left_bound. wpo_gap_iteration_state_injective_left_bound + S (wpo_injective_left_iteration_state_injective) = m + m) -> (exists wpo_gap_iteration_state_injective_right_bound. wpo_gap_iteration_state_injective_right_bound + S (wpo_injective_right_iteration_state_injective) = m + m) -> (((exists wpo_beta_height_iteration_state_injective_left_entry. wpo_beta_height_iteration_state_injective_left_entry + S (wpo_injective_value_iteration_state_injective) = S ((S (wpo_injective_left_iteration_state_injective)) * c)) /\ exists wpo_beta_quotient_iteration_state_injective_left_entry. b = wpo_beta_quotient_iteration_state_injective_left_entry * S ((S (wpo_injective_left_iteration_state_injective)) * c) + (wpo_injective_value_iteration_state_injective))) -> (((exists wpo_beta_height_iteration_state_injective_right_entry. wpo_beta_height_iteration_state_injective_right_entry + S (wpo_injective_value_iteration_state_injective) = S ((S (wpo_injective_right_iteration_state_injective)) * c)) /\ exists wpo_beta_quotient_iteration_state_injective_right_entry. b = wpo_beta_quotient_iteration_state_injective_right_entry * S ((S (wpo_injective_right_iteration_state_injective)) * c) + (wpo_injective_value_iteration_state_injective))) -> wpo_injective_left_iteration_state_injective = wpo_injective_right_iteration_state_injective))))) /\ (forall espi_pair_iteration_history. (exists wpo_gap_iteration_history_pair_bound. wpo_gap_iteration_history_pair_bound + S (espi_pair_iteration_history) = m) -> exists espi_left_iteration_history espi_right_iteration_history. (((((exists wpo_beta_height_iteration_history_left_entry. wpo_beta_height_iteration_history_left_entry + S (espi_left_iteration_history) = S ((S (espi_pair_iteration_history + espi_pair_iteration_history)) * c)) /\ exists wpo_beta_quotient_iteration_history_left_entry. b = wpo_beta_quotient_iteration_history_left_entry * S ((S (espi_pair_iteration_history + espi_pair_iteration_history)) * c) + (espi_left_iteration_history))) /\ (((((exists wpo_beta_height_iteration_history_right_entry. wpo_beta_height_iteration_history_right_entry + S (espi_right_iteration_history) = S ((S (S (espi_pair_iteration_history + espi_pair_iteration_history))) * c)) /\ exists wpo_beta_quotient_iteration_history_right_entry. b = wpo_beta_quotient_iteration_history_right_entry * S ((S (S (espi_pair_iteration_history + espi_pair_iteration_history))) * c) + (espi_right_iteration_history))) /\ (((exists wpo_beta_height_iteration_history_scaled_edge. wpo_beta_height_iteration_history_scaled_edge + S (S espi_right_iteration_history) = S ((S (espi_left_iteration_history)) * v)) /\ exists wpo_beta_quotient_iteration_history_scaled_edge. u = wpo_beta_quotient_iteration_history_scaled_edge * S ((S (espi_left_iteration_history)) * v) + (S espi_right_iteration_history)))))))))))
  16. 0016specialize scaled_inverse_pair_order_paired_iteration p
  17. 0017specialize scaled_inverse_pair_order_paired_iteration a
  18. 0018specialize scaled_inverse_pair_order_paired_iteration n
  19. 0019specialize scaled_inverse_pair_order_paired_iteration u
  20. 0020specialize scaled_inverse_pair_order_paired_iteration v
  21. 0021apply scaled_inverse_pair_order_paired_iteration
  22. 0022exact hpn
  23. 0023exact hp
  24. 0024exact hnotqres
  25. 0025exact hprefix
  26. 0026specialize hall h
  27. 0027specialize hall 0
  28. 0028apply hall
  29. 0029exact hbalance