PA009I · theorem

scaled_inverse_prefix_choose_omitted_orbit

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

Choose an omitted source, decode its actual mate S j, and expose a distinct involutive pair.

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. ∀ b. ∀ c. ∀ l. p = S n → Prime(p) → ¬QRes(p,a) → ScaledInversePrefix(p,a,n,u,v,n) → Lt(l,n) → ∃ x. ∃ y. Lt(x,n) ∧ (¬ContainsPrefix(b,c,l,x) ∧ (Lt(y,n) ∧ (¬x = y ∧ (BetaAt(u,v,x,S y) ∧ BetaAt(u,v,y,S x)))))

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 PD0027 ContainsPrefix PD0039 ScaledInversePrefix

9 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0027 ContainsPrefix PD0038 ScaledInverseIndex

7 occurrences

Exact expanded native-PA statement
forall p a n u v b c l. p = S n -> ((~(p = 1) /\ forall esi_prime_left_espo_choose_prime esi_prime_right_espo_choose_prime. p = esi_prime_left_espo_choose_prime * esi_prime_right_espo_choose_prime -> esi_prime_left_espo_choose_prime = 1 \/ esi_prime_right_espo_choose_prime = 1)) -> ~(exists qr_x_espo_choose_nonresidue. exists qr_u_espo_choose_nonresidue qr_v_espo_choose_nonresidue. qr_x_espo_choose_nonresidue * qr_x_espo_choose_nonresidue + p * qr_u_espo_choose_nonresidue = a + p * qr_v_espo_choose_nonresidue) -> (forall esip_index_espo_choose_prefix. (exists esip_gap_espo_choose_prefix_prefix_bound. esip_gap_espo_choose_prefix_prefix_bound + S (esip_index_espo_choose_prefix) = n) -> exists esip_mate_espo_choose_prefix. ((((exists ff_h_esip_espo_choose_prefix_entry. ff_h_esip_espo_choose_prefix_entry + S (esip_mate_espo_choose_prefix) = S ((S (esip_index_espo_choose_prefix)) * v)) /\ exists ff_q_esip_espo_choose_prefix_entry. u = ff_q_esip_espo_choose_prefix_entry * S ((S (esip_index_espo_choose_prefix)) * v) + (esip_mate_espo_choose_prefix))) /\ ((exists esip_gap_espo_choose_prefix_relation_index_bound. esip_gap_espo_choose_prefix_relation_index_bound + S (esip_index_espo_choose_prefix) = n) /\ ((((~((S esip_index_espo_choose_prefix) = 0) /\ (exists esip_gap_espo_choose_prefix_relation_scaled_left_bound. esip_gap_espo_choose_prefix_relation_scaled_left_bound + S (S esip_index_espo_choose_prefix) = p))) /\ (((~(esip_mate_espo_choose_prefix = 0) /\ (exists esip_gap_espo_choose_prefix_relation_scaled_right_bound. esip_gap_espo_choose_prefix_relation_scaled_right_bound + S (esip_mate_espo_choose_prefix) = p))) /\ (exists esi_mod_left_espo_choose_prefix_relation_scaled_mod esi_mod_right_espo_choose_prefix_relation_scaled_mod. ((S esip_index_espo_choose_prefix) * esip_mate_espo_choose_prefix) + p * esi_mod_left_espo_choose_prefix_relation_scaled_mod = (a) + p * esi_mod_right_espo_choose_prefix_relation_scaled_mod))))))) -> (exists wpo_gap_choose_short. wpo_gap_choose_short + S (l) = n) -> (exists i j. ((exists wpo_gap_chosen_i_bound. wpo_gap_chosen_i_bound + S (i) = n) /\ (((~(exists wpo_index_chosen_i_omit_contains. ((exists wpo_gap_chosen_i_omit_contains_bound. wpo_gap_chosen_i_omit_contains_bound + S (wpo_index_chosen_i_omit_contains) = l) /\ (((exists wpo_beta_height_chosen_i_omit_contains_entry. wpo_beta_height_chosen_i_omit_contains_entry + S (i) = S ((S (wpo_index_chosen_i_omit_contains)) * c)) /\ exists wpo_beta_quotient_chosen_i_omit_contains_entry. b = wpo_beta_quotient_chosen_i_omit_contains_entry * S ((S (wpo_index_chosen_i_omit_contains)) * c) + (i)))))) /\ (((exists wpo_gap_chosen_j_bound. wpo_gap_chosen_j_bound + S (j) = n) /\ (((~(i = j)) /\ (((((exists wpo_beta_height_chosen_forward. wpo_beta_height_chosen_forward + S (S j) = S ((S (i)) * v)) /\ exists wpo_beta_quotient_chosen_forward. u = wpo_beta_quotient_chosen_forward * S ((S (i)) * v) + (S j))) /\ (((exists wpo_beta_height_chosen_back. wpo_beta_height_chosen_back + S (S i) = S ((S (j)) * v)) /\ exists wpo_beta_quotient_chosen_back. u = wpo_beta_quotient_chosen_back * S ((S (j)) * v) + (S i)))))))))))))

Proof neighborhood

Direct theorem prerequisites

PA0098 finite_short_prefix_omits PA009E scaled_inverse_prefix_involutive PA009H scaled_inverse_prefix_no_fixed_of_not_qres

Direct theorem dependents

PA009O scaled_inverse_pair_order_choose_append

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

78 script commands · 23 reading checkpoints · 5 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 (3)
finite short prefix omitsscaled inverse prefix involutivescaled inverse prefix no fixed of not qres
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 b
  7. L7
    intro c
  8. L8
    intro l
  9. L9
    intro hpn
  10. L10
    intro hp
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hnotqres
  2. L12
    intro hprefix
  3. L13
    intro hshort
03Establish homittedL14–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite short prefix omits.

  1. L14
    have homitted : ∃ wpo_value_choose_omitted. Lt(wpo_value_choose_omitted,n) ∧ ¬ContainsPrefix(b,c,l,wpo_value_choose_omitted)Definitions: Lt(wpo_value_choose_omitted,n)ContainsPrefix(b,c,l,wpo_value_choose_omitted)Original native command in the exact edition
  2. L15
    specialize finite_short_prefix_omits b
  3. L16
    specialize finite_short_prefix_omits c
  4. L17
    specialize finite_short_prefix_omits l
  5. L18
    specialize finite_short_prefix_omits n
  6. L19
    apply finite_short_prefix_omits
  7. L20
    exact hshort
04Separate the logical casesL21–22

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L21
    cases homitted
  2. L22
    cases homitted_witness
05Establish hstoredL23–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hprefix.

  1. L23
    have hstored : ∃ y. BetaAt(u,v,x,y) ∧ ScaledInverseIndex(p,a,n,x,y)Definitions: BetaAt(u,v,x,y)ScaledInverseIndex(p,a,n,x,y)Original native command in the exact edition
  2. L24
    specialize hprefix x
  3. L25
    apply hprefix
  4. L26
    exact homitted_witness_left
06Separate the logical casesL27–28

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L27
    cases hstored
  2. L28
    cases hstored_witness
07Establish hinvolutiveL29–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply scaled inverse prefix involutive.

  1. L29
    have hinvolutive : ∃ j. x1 = S j ∧ (Lt(j,n) ∧ BetaAt(u,v,j,S x))Definitions: Lt(j,n)BetaAt(u,v,j,S x)Original native command in the exact edition
  2. L30
    specialize scaled_inverse_prefix_involutive p
  3. L31
    specialize scaled_inverse_prefix_involutive a
  4. L32
    specialize scaled_inverse_prefix_involutive n
  5. L33
    specialize scaled_inverse_prefix_involutive u
  6. L34
    specialize scaled_inverse_prefix_involutive v
  7. L35
    specialize scaled_inverse_prefix_involutive x
  8. L36
    specialize scaled_inverse_prefix_involutive x1
  9. L37
    apply scaled_inverse_prefix_involutive
  10. L38
    exact hpn
08Use earlier factsL39–42

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

  1. L39
    exact hp
  2. L40
    exact hprefix
  3. L41
    exact homitted_witness_left
  4. L42
    exact hstored_witness_left
09Separate the logical casesL43–45

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L43
    cases hinvolutive
  2. L44
    cases hinvolutive_witness
  3. L45
    cases hinvolutive_witness_right
10Establish hforwardL46–49

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

  1. L46
    have hforward : BetaAt(u,v,x,S x2)Definitions: BetaAt(u,v,x,S x2)Original native command in the exact edition
  2. L47
    rewrite <- hinvolutive_witness_left
  3. L48
    rewrite <- hinvolutive_witness_left
  4. L49
    exact hstored_witness_left
11Establish hdistinctL50–59

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

  1. L50
    have hdistinct : ~(x = x2)
  2. L51
    intro heq
  3. L52
    rewrite <- heq at hforward
  4. L53
    rewrite <- heq at hforward
  5. L54
    specialize scaled_inverse_prefix_no_fixed_of_not_qres p
  6. L55
    specialize scaled_inverse_prefix_no_fixed_of_not_qres a
  7. L56
    specialize scaled_inverse_prefix_no_fixed_of_not_qres n
  8. L57
    specialize scaled_inverse_prefix_no_fixed_of_not_qres u
  9. L58
    specialize scaled_inverse_prefix_no_fixed_of_not_qres v
  10. L59
    specialize scaled_inverse_prefix_no_fixed_of_not_qres n
12Use earlier factsL60–65

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

  1. L60
    specialize scaled_inverse_prefix_no_fixed_of_not_qres x
  2. L61
    apply scaled_inverse_prefix_no_fixed_of_not_qres
  3. L62
    exact hnotqres
  4. L63
    exact hprefix
  5. L64
    exact homitted_witness_left
  6. L65
    exact hforward
13Construct an explicit witnessL66–67

Supply the displayed value, then prove that it has the required property.

  1. L66
    exists x
  2. L67
    exists x2
14Separate the logical casesL68–68

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L68
    split
15Use earlier factsL69–69

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

  1. L69
    exact homitted_witness_left
16Separate the logical casesL70–70

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L70
    split
17Use earlier factsL71–71

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

  1. L71
    exact homitted_witness_right
18Separate the logical casesL72–72

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L72
    split
19Use earlier factsL73–73

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

  1. L73
    exact hinvolutive_witness_right_left
20Separate the logical casesL74–74

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L74
    split
21Use earlier factsL75–75

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

  1. L75
    exact hdistinct
22Separate the logical casesL76–76

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L76
    split
23Use earlier factsL77–78

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

  1. L77
    exact hforward
  2. L78
    exact hinvolutive_witness_right_right

Library-wide reading audit

Original defined command ledger · 78 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro n
  4. 0004intro u
  5. 0005intro v
  6. 0006intro b
  7. 0007intro c
  8. 0008intro l
  9. 0009intro hpn
  10. 0010intro hp
  11. 0011intro hnotqres
  12. 0012intro hprefix
  13. 0013intro hshort
  14. 0014have homitted : ∃ wpo_value_choose_omitted. Lt(wpo_value_choose_omitted,n) ∧ ¬ContainsPrefix(b,c,l,wpo_value_choose_omitted)
    Exact native replay linehave homitted : exists wpo_value_choose_omitted. ((exists wpo_gap_choose_omitted_value_bound. wpo_gap_choose_omitted_value_bound + S (wpo_value_choose_omitted) = n) /\ (~(exists wpo_index_choose_omitted_omitted_contains. ((exists wpo_gap_choose_omitted_omitted_contains_bound. wpo_gap_choose_omitted_omitted_contains_bound + S (wpo_index_choose_omitted_omitted_contains) = l) /\ (((exists wpo_beta_height_choose_omitted_omitted_contains_entry. wpo_beta_height_choose_omitted_omitted_contains_entry + S (wpo_value_choose_omitted) = S ((S (wpo_index_choose_omitted_omitted_contains)) * c)) /\ exists wpo_beta_quotient_choose_omitted_omitted_contains_entry. b = wpo_beta_quotient_choose_omitted_omitted_contains_entry * S ((S (wpo_index_choose_omitted_omitted_contains)) * c) + (wpo_value_choose_omitted)))))))
  15. 0015specialize finite_short_prefix_omits b
  16. 0016specialize finite_short_prefix_omits c
  17. 0017specialize finite_short_prefix_omits l
  18. 0018specialize finite_short_prefix_omits n
  19. 0019apply finite_short_prefix_omits
  20. 0020exact hshort
  21. 0021cases homitted
  22. 0022cases homitted_witness
  23. 0023have hstored : ∃ y. BetaAt(u,v,x,y) ∧ ScaledInverseIndex(p,a,n,x,y)
    Exact native replay linehave hstored : exists y. ((((exists wpo_beta_height_chosen_stored_x_entry. wpo_beta_height_chosen_stored_x_entry + S (y) = S ((S (x)) * v)) /\ exists wpo_beta_quotient_chosen_stored_x_entry. u = wpo_beta_quotient_chosen_stored_x_entry * S ((S (x)) * v) + (y))) /\ ((exists esip_gap_chosen_stored_x_relation_index_bound. esip_gap_chosen_stored_x_relation_index_bound + S (x) = n) /\ ((((~((S x) = 0) /\ (exists esip_gap_chosen_stored_x_relation_scaled_left_bound. esip_gap_chosen_stored_x_relation_scaled_left_bound + S (S x) = p))) /\ (((~(y = 0) /\ (exists esip_gap_chosen_stored_x_relation_scaled_right_bound. esip_gap_chosen_stored_x_relation_scaled_right_bound + S (y) = p))) /\ (exists esi_mod_left_chosen_stored_x_relation_scaled_mod esi_mod_right_chosen_stored_x_relation_scaled_mod. ((S x) * y) + p * esi_mod_left_chosen_stored_x_relation_scaled_mod = (a) + p * esi_mod_right_chosen_stored_x_relation_scaled_mod))))))
  24. 0024specialize hprefix x
  25. 0025apply hprefix
  26. 0026exact homitted_witness_left
  27. 0027cases hstored
  28. 0028cases hstored_witness
  29. 0029have hinvolutive : ∃ j. x1 = S j ∧ (Lt(j,n) ∧ BetaAt(u,v,j,S x))
    Exact native replay linehave hinvolutive : exists j. ((x1 = S j) /\ (((exists wpo_gap_chosen_involutive_j_bound. wpo_gap_chosen_involutive_j_bound + S (j) = n) /\ (((exists wpo_beta_height_chosen_involutive_back. wpo_beta_height_chosen_involutive_back + S (S x) = S ((S (j)) * v)) /\ exists wpo_beta_quotient_chosen_involutive_back. u = wpo_beta_quotient_chosen_involutive_back * S ((S (j)) * v) + (S x))))))
  30. 0030specialize scaled_inverse_prefix_involutive p
  31. 0031specialize scaled_inverse_prefix_involutive a
  32. 0032specialize scaled_inverse_prefix_involutive n
  33. 0033specialize scaled_inverse_prefix_involutive u
  34. 0034specialize scaled_inverse_prefix_involutive v
  35. 0035specialize scaled_inverse_prefix_involutive x
  36. 0036specialize scaled_inverse_prefix_involutive x1
  37. 0037apply scaled_inverse_prefix_involutive
  38. 0038exact hpn
  39. 0039exact hp
  40. 0040exact hprefix
  41. 0041exact homitted_witness_left
  42. 0042exact hstored_witness_left
  43. 0043cases hinvolutive
  44. 0044cases hinvolutive_witness
  45. 0045cases hinvolutive_witness_right
  46. 0046have hforward : BetaAt(u,v,x,S x2)
    Exact native replay linehave hforward : ((exists wpo_beta_height_chosen_forward_x2. wpo_beta_height_chosen_forward_x2 + S (S x2) = S ((S (x)) * v)) /\ exists wpo_beta_quotient_chosen_forward_x2. u = wpo_beta_quotient_chosen_forward_x2 * S ((S (x)) * v) + (S x2))
  47. 0047rewrite <- hinvolutive_witness_left
  48. 0048rewrite <- hinvolutive_witness_left
  49. 0049exact hstored_witness_left
  50. 0050have hdistinct : ~(x = x2)
  51. 0051intro heq
  52. 0052rewrite <- heq at hforward
  53. 0053rewrite <- heq at hforward
  54. 0054specialize scaled_inverse_prefix_no_fixed_of_not_qres p
  55. 0055specialize scaled_inverse_prefix_no_fixed_of_not_qres a
  56. 0056specialize scaled_inverse_prefix_no_fixed_of_not_qres n
  57. 0057specialize scaled_inverse_prefix_no_fixed_of_not_qres u
  58. 0058specialize scaled_inverse_prefix_no_fixed_of_not_qres v
  59. 0059specialize scaled_inverse_prefix_no_fixed_of_not_qres n
  60. 0060specialize scaled_inverse_prefix_no_fixed_of_not_qres x
  61. 0061apply scaled_inverse_prefix_no_fixed_of_not_qres
  62. 0062exact hnotqres
  63. 0063exact hprefix
  64. 0064exact homitted_witness_left
  65. 0065exact hforward
  66. 0066exists x
  67. 0067exists x2
  68. 0068split
  69. 0069exact homitted_witness_left
  70. 0070split
  71. 0071exact homitted_witness_right
  72. 0072split
  73. 0073exact hinvolutive_witness_right_left
  74. 0074split
  75. 0075exact hdistinct
  76. 0076split
  77. 0077exact hforward
  78. 0078exact hinvolutive_witness_right_right