PA008S

prime_scaled_inverse_prefix_exists_bounded

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

Every bounded predecessor length has a beta-coded scaled-inverse 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.

Exact expanded PA statement

forall p a n l. p = S n -> ((~(p = 1) /\ forall esi_prime_left_esip_bounded_prime esi_prime_right_esip_bounded_prime. p = esi_prime_left_esip_bounded_prime * esi_prime_right_esip_bounded_prime -> esi_prime_left_esip_bounded_prime = 1 \/ esi_prime_right_esip_bounded_prime = 1)) -> ~(a = 0) -> (exists esip_gap_bounded_target_bound. esip_gap_bounded_target_bound + S (a) = p) -> (exists esip_weak_gap_bounded. esip_weak_gap_bounded + l = n) -> exists b c. (forall esip_index_bounded_result. (exists esip_gap_bounded_result_prefix_bound. esip_gap_bounded_result_prefix_bound + S (esip_index_bounded_result) = l) -> exists esip_mate_bounded_result. ((((exists ff_h_esip_bounded_result_entry. ff_h_esip_bounded_result_entry + S (esip_mate_bounded_result) = S ((S (esip_index_bounded_result)) * c)) /\ exists ff_q_esip_bounded_result_entry. b = ff_q_esip_bounded_result_entry * S ((S (esip_index_bounded_result)) * c) + (esip_mate_bounded_result))) /\ ((exists esip_gap_bounded_result_relation_index_bound. esip_gap_bounded_result_relation_index_bound + S (esip_index_bounded_result) = n) /\ ((((~((S esip_index_bounded_result) = 0) /\ (exists esip_gap_bounded_result_relation_scaled_left_bound. esip_gap_bounded_result_relation_scaled_left_bound + S (S esip_index_bounded_result) = p))) /\ (((~(esip_mate_bounded_result = 0) /\ (exists esip_gap_bounded_result_relation_scaled_right_bound. esip_gap_bounded_result_relation_scaled_right_bound + S (esip_mate_bounded_result) = p))) /\ (exists esi_mod_left_bounded_result_relation_scaled_mod esi_mod_right_bounded_result_relation_scaled_mod. ((S esip_index_bounded_result) * esip_mate_bounded_result) + p * esi_mod_left_bounded_result_relation_scaled_mod = (a) + p * esi_mod_right_bounded_result_relation_scaled_mod)))))))

Structural proof guide

Generated structural guide

Every bounded predecessor length has a beta-coded scaled-inverse prefix.

Use the direct prerequisites add_eq_zero_right, succ_ne_zero, lt_to_le, prime_scaled_inverse_prefix_extend as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (5), intermediate claims (4).

Referenced ingredients

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA000X lt_to_le PA008R prime_scaled_inverse_prefix_extend

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA000X lt_to_le PA008R prime_scaled_inverse_prefix_extend

Direct dependents

PA008T prime_scaled_inverse_prefix_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

63 script commands · 17 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.

Named ingredients (4)
add eq zero rightsucc ne zerolt to leprime scaled inverse prefix extend

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–3

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro n
02Induction on lL4–9

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L4
    induction l
  2. L5
    intro hpn
  3. L6
    intro hp
  4. L7
    intro ha0
  5. L8
    intro hap
  6. L9
    intro hln
03Construct an explicit witnessL10–11

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

  1. L10
    exists 0
  2. L11
    exists 0
04Fix variables and assumptionsL12–13

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

  1. L12
    intro i
  2. L13
    intro hi
05Separate the logical casesL14–15

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

  1. L14
    exfalso
  2. L15
    cases hi
06Establish hsiL16–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.

  1. L16
    have hsi : S i = 0
  2. L17
    specialize add_eq_zero_right x
  3. L18
    specialize add_eq_zero_right (S i)
  4. L19
    apply add_eq_zero_right
  5. L20
    exact hi_witness
  6. L21
    specialize succ_ne_zero i
  7. L22
    apply succ_ne_zero
  8. L23
    exact hsi
  9. L24
    intro hpn
  10. L25
    intro hp
07Fix variables and assumptionsL26–28

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

  1. L26
    intro ha0
  2. L27
    intro hap
  3. L28
    intro hln
08Establish hprev_boundL29–33

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

  1. L29
    have hprev_bound : exists h. h + l = n
  2. L30
    specialize lt_to_le l
  3. L31
    specialize lt_to_le n
  4. L32
    apply lt_to_le
  5. L33
    exact hln
09Establish hprevL34–40

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

  1. L34
    have hprev : ∃ b. ∃ c. ScaledInversePrefix(p,a,n,b,c,l)Definitions: ScaledInversePrefix
  2. L35
    apply IH
  3. L36
    exact hpn
  4. L37
    exact hp
  5. L38
    exact ha0
  6. L39
    exact hap
  7. L40
    exact hprev_bound
10Separate the logical casesL41–42

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

  1. L41
    cases hprev
  2. L42
    cases hprev_witness
11Establish hnextL43–52

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

  1. L43
    have hnext : ∃ z. ∃ d. ScaledInversePrefix(p,a,n,z,d,S l)Definitions: ScaledInversePrefix
  2. L44
    specialize prime_scaled_inverse_prefix_extend p
  3. L45
    specialize prime_scaled_inverse_prefix_extend a
  4. L46
    specialize prime_scaled_inverse_prefix_extend n
  5. L47
    specialize prime_scaled_inverse_prefix_extend x
  6. L48
    specialize prime_scaled_inverse_prefix_extend x1
  7. L49
    specialize prime_scaled_inverse_prefix_extend l
  8. L50
    specialize prime_scaled_inverse_prefix_extend (S l)
  9. L51
    apply prime_scaled_inverse_prefix_extend
  10. L52
    exact hpn
12Use earlier factsL53–56

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

  1. L53
    exact hp
  2. L54
    exact ha0
  3. L55
    exact hap
  4. L56
    exact hln
13Calculate and transport equalitiesL57–57

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

  1. L57
    refl
14Use earlier factsL58–58

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

  1. L58
    exact hprev_witness_witness
15Separate the logical casesL59–60

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

  1. L59
    cases hnext
  2. L60
    cases hnext_witness
16Construct an explicit witnessL61–62

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

  1. L61
    exists x2
  2. L62
    exists x3
17Use earlier factsL63–63

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

  1. L63
    exact hnext_witness_witness

Library-wide reading audit

Original exact command ledger · 63 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro n
  4. 0004induction l
  5. 0005intro hpn
  6. 0006intro hp
  7. 0007intro ha0
  8. 0008intro hap
  9. 0009intro hln
  10. 0010exists 0
  11. 0011exists 0
  12. 0012intro i
  13. 0013intro hi
  14. 0014exfalso
  15. 0015cases hi
  16. 0016have hsi : S i = 0
  17. 0017specialize add_eq_zero_right x
  18. 0018specialize add_eq_zero_right (S i)
  19. 0019apply add_eq_zero_right
  20. 0020exact hi_witness
  21. 0021specialize succ_ne_zero i
  22. 0022apply succ_ne_zero
  23. 0023exact hsi
  24. 0024intro hpn
  25. 0025intro hp
  26. 0026intro ha0
  27. 0027intro hap
  28. 0028intro hln
  29. 0029have hprev_bound : exists h. h + l = n
  30. 0030specialize lt_to_le l
  31. 0031specialize lt_to_le n
  32. 0032apply lt_to_le
  33. 0033exact hln
  34. 0034have hprev : exists b c. (forall esip_index_bounded_previous. (exists esip_gap_bounded_previous_prefix_bound. esip_gap_bounded_previous_prefix_bound + S (esip_index_bounded_previous) = l) -> exists esip_mate_bounded_previous. ((((exists ff_h_esip_bounded_previous_entry. ff_h_esip_bounded_previous_entry + S (esip_mate_bounded_previous) = S ((S (esip_index_bounded_previous)) * c)) /\ exists ff_q_esip_bounded_previous_entry. b = ff_q_esip_bounded_previous_entry * S ((S (esip_index_bounded_previous)) * c) + (esip_mate_bounded_previous))) /\ ((exists esip_gap_bounded_previous_relation_index_bound. esip_gap_bounded_previous_relation_index_bound + S (esip_index_bounded_previous) = n) /\ ((((~((S esip_index_bounded_previous) = 0) /\ (exists esip_gap_bounded_previous_relation_scaled_left_bound. esip_gap_bounded_previous_relation_scaled_left_bound + S (S esip_index_bounded_previous) = p))) /\ (((~(esip_mate_bounded_previous = 0) /\ (exists esip_gap_bounded_previous_relation_scaled_right_bound. esip_gap_bounded_previous_relation_scaled_right_bound + S (esip_mate_bounded_previous) = p))) /\ (exists esi_mod_left_bounded_previous_relation_scaled_mod esi_mod_right_bounded_previous_relation_scaled_mod. ((S esip_index_bounded_previous) * esip_mate_bounded_previous) + p * esi_mod_left_bounded_previous_relation_scaled_mod = (a) + p * esi_mod_right_bounded_previous_relation_scaled_mod)))))))
  35. 0035apply IH
  36. 0036exact hpn
  37. 0037exact hp
  38. 0038exact ha0
  39. 0039exact hap
  40. 0040exact hprev_bound
  41. 0041cases hprev
  42. 0042cases hprev_witness
  43. 0043have hnext : exists z d. (forall esip_index_bounded_successor. (exists esip_gap_bounded_successor_prefix_bound. esip_gap_bounded_successor_prefix_bound + S (esip_index_bounded_successor) = S l) -> exists esip_mate_bounded_successor. ((((exists ff_h_esip_bounded_successor_entry. ff_h_esip_bounded_successor_entry + S (esip_mate_bounded_successor) = S ((S (esip_index_bounded_successor)) * d)) /\ exists ff_q_esip_bounded_successor_entry. z = ff_q_esip_bounded_successor_entry * S ((S (esip_index_bounded_successor)) * d) + (esip_mate_bounded_successor))) /\ ((exists esip_gap_bounded_successor_relation_index_bound. esip_gap_bounded_successor_relation_index_bound + S (esip_index_bounded_successor) = n) /\ ((((~((S esip_index_bounded_successor) = 0) /\ (exists esip_gap_bounded_successor_relation_scaled_left_bound. esip_gap_bounded_successor_relation_scaled_left_bound + S (S esip_index_bounded_successor) = p))) /\ (((~(esip_mate_bounded_successor = 0) /\ (exists esip_gap_bounded_successor_relation_scaled_right_bound. esip_gap_bounded_successor_relation_scaled_right_bound + S (esip_mate_bounded_successor) = p))) /\ (exists esi_mod_left_bounded_successor_relation_scaled_mod esi_mod_right_bounded_successor_relation_scaled_mod. ((S esip_index_bounded_successor) * esip_mate_bounded_successor) + p * esi_mod_left_bounded_successor_relation_scaled_mod = (a) + p * esi_mod_right_bounded_successor_relation_scaled_mod)))))))
  44. 0044specialize prime_scaled_inverse_prefix_extend p
  45. 0045specialize prime_scaled_inverse_prefix_extend a
  46. 0046specialize prime_scaled_inverse_prefix_extend n
  47. 0047specialize prime_scaled_inverse_prefix_extend x
  48. 0048specialize prime_scaled_inverse_prefix_extend x1
  49. 0049specialize prime_scaled_inverse_prefix_extend l
  50. 0050specialize prime_scaled_inverse_prefix_extend (S l)
  51. 0051apply prime_scaled_inverse_prefix_extend
  52. 0052exact hpn
  53. 0053exact hp
  54. 0054exact ha0
  55. 0055exact hap
  56. 0056exact hln
  57. 0057refl
  58. 0058exact hprev_witness_witness
  59. 0059cases hnext
  60. 0060cases hnext_witness
  61. 0061exists x2
  62. 0062exists x3
  63. 0063exact hnext_witness_witness