PA008R · theorem

prime_scaled_inverse_prefix_extend

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

Append one actual scaled-inverse value to a zero-based source prefix.

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. ∀ b. ∀ c. ∀ l. ∀ sl. p = S n → Prime(p) → ¬a = 0 → Lt(a,p) → Lt(l,n) → sl = S l → ScaledInversePrefix(p,a,n,b,c,l) → ∃ x. ∃ y. ScaledInversePrefix(p,a,n,x,y,sl)

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

5 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0033 ScaledInverse PD0038 ScaledInverseIndex

5 occurrences

Exact expanded native-PA statement
forall p a n b c l sl. p = S n -> ((~(p = 1) /\ forall esi_prime_left_esip_extend_prime esi_prime_right_esip_extend_prime. p = esi_prime_left_esip_extend_prime * esi_prime_right_esip_extend_prime -> esi_prime_left_esip_extend_prime = 1 \/ esi_prime_right_esip_extend_prime = 1)) -> ~(a = 0) -> (exists esip_gap_extend_target_bound. esip_gap_extend_target_bound + S (a) = p) -> (exists esip_gap_extend_length_bound. esip_gap_extend_length_bound + S (l) = n) -> sl = S l -> (forall esip_index_extend_before. (exists esip_gap_extend_before_prefix_bound. esip_gap_extend_before_prefix_bound + S (esip_index_extend_before) = l) -> exists esip_mate_extend_before. ((((exists ff_h_esip_extend_before_entry. ff_h_esip_extend_before_entry + S (esip_mate_extend_before) = S ((S (esip_index_extend_before)) * c)) /\ exists ff_q_esip_extend_before_entry. b = ff_q_esip_extend_before_entry * S ((S (esip_index_extend_before)) * c) + (esip_mate_extend_before))) /\ ((exists esip_gap_extend_before_relation_index_bound. esip_gap_extend_before_relation_index_bound + S (esip_index_extend_before) = n) /\ ((((~((S esip_index_extend_before) = 0) /\ (exists esip_gap_extend_before_relation_scaled_left_bound. esip_gap_extend_before_relation_scaled_left_bound + S (S esip_index_extend_before) = p))) /\ (((~(esip_mate_extend_before = 0) /\ (exists esip_gap_extend_before_relation_scaled_right_bound. esip_gap_extend_before_relation_scaled_right_bound + S (esip_mate_extend_before) = p))) /\ (exists esi_mod_left_extend_before_relation_scaled_mod esi_mod_right_extend_before_relation_scaled_mod. ((S esip_index_extend_before) * esip_mate_extend_before) + p * esi_mod_left_extend_before_relation_scaled_mod = (a) + p * esi_mod_right_extend_before_relation_scaled_mod))))))) -> exists z d. (forall esip_index_extend_after. (exists esip_gap_extend_after_prefix_bound. esip_gap_extend_after_prefix_bound + S (esip_index_extend_after) = sl) -> exists esip_mate_extend_after. ((((exists ff_h_esip_extend_after_entry. ff_h_esip_extend_after_entry + S (esip_mate_extend_after) = S ((S (esip_index_extend_after)) * d)) /\ exists ff_q_esip_extend_after_entry. z = ff_q_esip_extend_after_entry * S ((S (esip_index_extend_after)) * d) + (esip_mate_extend_after))) /\ ((exists esip_gap_extend_after_relation_index_bound. esip_gap_extend_after_relation_index_bound + S (esip_index_extend_after) = n) /\ ((((~((S esip_index_extend_after) = 0) /\ (exists esip_gap_extend_after_relation_scaled_left_bound. esip_gap_extend_after_relation_scaled_left_bound + S (S esip_index_extend_after) = p))) /\ (((~(esip_mate_extend_after = 0) /\ (exists esip_gap_extend_after_relation_scaled_right_bound. esip_gap_extend_after_relation_scaled_right_bound + S (esip_mate_extend_after) = p))) /\ (exists esi_mod_left_extend_after_relation_scaled_mod esi_mod_right_extend_after_relation_scaled_mod. ((S esip_index_extend_after) * esip_mate_extend_after) + p * esi_mod_left_extend_after_relation_scaled_mod = (a) + p * esi_mod_right_extend_after_relation_scaled_mod)))))))

Proof neighborhood

Direct theorem prerequisites

PA0005 succ_ne_zero PA002K succ_le_succ PA008Q prime_scaled_inverse_exists PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt

Direct theorem dependents

PA008S prime_scaled_inverse_prefix_exists_bounded

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

76 script commands · 27 reading checkpoints · 4 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 (5)
succ ne zerosucc le succprime scaled inverse existsbeta prefix extendfinite lt succ eq or lt
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 b
  5. L5
    intro c
  6. L6
    intro l
  7. L7
    intro sl
  8. L8
    intro hpn
  9. L9
    intro hp
  10. L10
    intro ha0
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hap
  2. L12
    intro hln
  3. L13
    intro hsl
  4. L14
    intro hprefix
03Establish hsource_boundL15–20

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

  1. L15
    have hsource_bound : Lt(S l,p)Definitions: Lt(S l,p)Original native command in the exact edition
  2. L16
    rewrite hpn
  3. L17
    specialize succ_le_succ (S l)
  4. L18
    specialize succ_le_succ n
  5. L19
    apply succ_le_succ
  6. L20
    exact hln
04Establish hnewL21–30

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

  1. L21
    have hnew : ∃ j. ScaledInverse(p,a,S l,j)Definitions: ScaledInverse(p,a,S l,j)Original native command in the exact edition
  2. L22
    specialize prime_scaled_inverse_exists p
  3. L23
    specialize prime_scaled_inverse_exists a
  4. L24
    specialize prime_scaled_inverse_exists (S l)
  5. L25
    apply prime_scaled_inverse_exists
  6. L26
    exact hp
  7. L27
    exact ha0
  8. L28
    exact hap
  9. L29
    specialize succ_ne_zero l
  10. L30
    exact succ_ne_zero
05Use earlier factsL31–31

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

  1. L31
    exact hsource_bound
06Separate the logical casesL32–32

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

  1. L32
    cases hnew
07Use earlier factsL33–36

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

  1. L33
    specialize beta_prefix_extend l
  2. L34
    specialize beta_prefix_extend b
  3. L35
    specialize beta_prefix_extend c
  4. L36
    specialize beta_prefix_extend x
08Separate the logical casesL37–39

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

  1. L37
    cases beta_prefix_extend
  2. L38
    cases beta_prefix_extend_witness
  3. L39
    cases beta_prefix_extend_witness_witness
09Construct an explicit witnessL40–41

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

  1. L40
    exists x1
  2. L41
    exists x2
10Fix variables and assumptionsL42–43

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

  1. L42
    intro i
  2. L43
    intro hi
11Calculate and transport equalitiesL44–44

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L44
    rewrite hsl at hi
12Establish hsplitL45–49

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L45
    have hsplit : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L46
    specialize finite_lt_succ_eq_or_lt l
  3. L47
    specialize finite_lt_succ_eq_or_lt i
  4. L48
    apply finite_lt_succ_eq_or_lt
  5. L49
    exact hi
13Separate the logical casesL50–50

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

  1. L50
    cases hsplit
14Construct an explicit witnessL51–51

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

  1. L51
    exists x
15Separate the logical casesL52–52

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

  1. L52
    split
16Calculate and transport equalitiesL53–54

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L53
    rewrite hsplit_left
  2. L54
    rewrite hsplit_left
17Use earlier factsL55–55

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

  1. L55
    exact beta_prefix_extend_witness_witness_left
18Separate the logical casesL56–56

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

  1. L56
    split
19Calculate and transport equalitiesL57–57

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L57
    rewrite hsplit_left
20Use earlier factsL58–58

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

  1. L58
    exact hln
21Calculate and transport equalitiesL59–61

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L59
    rewrite hsplit_left
  2. L60
    rewrite hsplit_left
  3. L61
    rewrite hsplit_left
22Use earlier factsL62–62

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

  1. L62
    exact hnew_witness
23Establish holdL63–66

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

  1. L63
    have hold : ∃ j. BetaAt(b,c,i,j) ∧ ScaledInverseIndex(p,a,n,i,j)Definitions: BetaAt(b,c,i,j)ScaledInverseIndex(p,a,n,i,j)Original native command in the exact edition
  2. L64
    specialize hprefix i
  3. L65
    apply hprefix
  4. L66
    exact hsplit_right
24Separate the logical casesL67–68

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

  1. L67
    cases hold
  2. L68
    cases hold_witness
25Construct an explicit witnessL69–69

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

  1. L69
    exists x3
26Separate the logical casesL70–70

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

  1. L70
    split
27Use earlier factsL71–76

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

  1. L71
    specialize beta_prefix_extend_witness_witness_right i
  2. L72
    specialize beta_prefix_extend_witness_witness_right x3
  3. L73
    apply beta_prefix_extend_witness_witness_right
  4. L74
    exact hsplit_right
  5. L75
    exact hold_witness_left
  6. L76
    exact hold_witness_right

Library-wide reading audit

Original defined command ledger · 76 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro n
  4. 0004intro b
  5. 0005intro c
  6. 0006intro l
  7. 0007intro sl
  8. 0008intro hpn
  9. 0009intro hp
  10. 0010intro ha0
  11. 0011intro hap
  12. 0012intro hln
  13. 0013intro hsl
  14. 0014intro hprefix
  15. 0015have hsource_bound : Lt(S l,p)
    Exact native replay linehave hsource_bound : exists esip_gap_extend_source_bound. esip_gap_extend_source_bound + S (S l) = p
  16. 0016rewrite hpn
  17. 0017specialize succ_le_succ (S l)
  18. 0018specialize succ_le_succ n
  19. 0019apply succ_le_succ
  20. 0020exact hln
  21. 0021have hnew : ∃ j. ScaledInverse(p,a,S l,j)
    Exact native replay linehave hnew : exists j. ((((~((S l) = 0) /\ (exists esip_gap_extend_new_scaled_left_bound. esip_gap_extend_new_scaled_left_bound + S (S l) = p))) /\ (((~(j = 0) /\ (exists esip_gap_extend_new_scaled_right_bound. esip_gap_extend_new_scaled_right_bound + S (j) = p))) /\ (exists esi_mod_left_extend_new_scaled_mod esi_mod_right_extend_new_scaled_mod. ((S l) * j) + p * esi_mod_left_extend_new_scaled_mod = (a) + p * esi_mod_right_extend_new_scaled_mod))))
  22. 0022specialize prime_scaled_inverse_exists p
  23. 0023specialize prime_scaled_inverse_exists a
  24. 0024specialize prime_scaled_inverse_exists (S l)
  25. 0025apply prime_scaled_inverse_exists
  26. 0026exact hp
  27. 0027exact ha0
  28. 0028exact hap
  29. 0029specialize succ_ne_zero l
  30. 0030exact succ_ne_zero
  31. 0031exact hsource_bound
  32. 0032cases hnew
  33. 0033specialize beta_prefix_extend l
  34. 0034specialize beta_prefix_extend b
  35. 0035specialize beta_prefix_extend c
  36. 0036specialize beta_prefix_extend x
  37. 0037cases beta_prefix_extend
  38. 0038cases beta_prefix_extend_witness
  39. 0039cases beta_prefix_extend_witness_witness
  40. 0040exists x1
  41. 0041exists x2
  42. 0042intro i
  43. 0043intro hi
  44. 0044rewrite hsl at hi
  45. 0045have hsplit : i = l ∨ Lt(i,l)
    Exact native replay linehave hsplit : i = l \/ exists h. h + S i = l
  46. 0046specialize finite_lt_succ_eq_or_lt l
  47. 0047specialize finite_lt_succ_eq_or_lt i
  48. 0048apply finite_lt_succ_eq_or_lt
  49. 0049exact hi
  50. 0050cases hsplit
  51. 0051exists x
  52. 0052split
  53. 0053rewrite hsplit_left
  54. 0054rewrite hsplit_left
  55. 0055exact beta_prefix_extend_witness_witness_left
  56. 0056split
  57. 0057rewrite hsplit_left
  58. 0058exact hln
  59. 0059rewrite hsplit_left
  60. 0060rewrite hsplit_left
  61. 0061rewrite hsplit_left
  62. 0062exact hnew_witness
  63. 0063have hold : ∃ j. BetaAt(b,c,i,j) ∧ ScaledInverseIndex(p,a,n,i,j)
    Exact native replay linehave hold : exists j. ((((exists ff_h_esip_extend_old_entry. ff_h_esip_extend_old_entry + S (j) = S ((S (i)) * c)) /\ exists ff_q_esip_extend_old_entry. b = ff_q_esip_extend_old_entry * S ((S (i)) * c) + (j))) /\ ((exists esip_gap_extend_old_relation_index_bound. esip_gap_extend_old_relation_index_bound + S (i) = n) /\ ((((~((S i) = 0) /\ (exists esip_gap_extend_old_relation_scaled_left_bound. esip_gap_extend_old_relation_scaled_left_bound + S (S i) = p))) /\ (((~(j = 0) /\ (exists esip_gap_extend_old_relation_scaled_right_bound. esip_gap_extend_old_relation_scaled_right_bound + S (j) = p))) /\ (exists esi_mod_left_extend_old_relation_scaled_mod esi_mod_right_extend_old_relation_scaled_mod. ((S i) * j) + p * esi_mod_left_extend_old_relation_scaled_mod = (a) + p * esi_mod_right_extend_old_relation_scaled_mod))))))
  64. 0064specialize hprefix i
  65. 0065apply hprefix
  66. 0066exact hsplit_right
  67. 0067cases hold
  68. 0068cases hold_witness
  69. 0069exists x3
  70. 0070split
  71. 0071specialize beta_prefix_extend_witness_witness_right i
  72. 0072specialize beta_prefix_extend_witness_witness_right x3
  73. 0073apply beta_prefix_extend_witness_witness_right
  74. 0074exact hsplit_right
  75. 0075exact hold_witness_left
  76. 0076exact hold_witness_right