PA00A6 · theorem

prime_inverse_prefix_exists_bounded

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

Every length bounded by p-1 has a beta-coded 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.

Statement with defined notation

∀ p. ∀ n. ∀ l. p = S n → Prime(p) → Le(l,n) → ∃ x. ∃ y. InversePrefix(p,n,x,y,l)

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

PD0001 Le PD0004 Prime PD0037 InversePrefix

3 occurrences

In local proof propositions

PD0001 Le PD0037 InversePrefix

3 occurrences

Exact expanded native-PA statement
forall p n l. p = S n -> ((~(p = 1) /\ forall wip_prime_left_bounded_prime wip_prime_right_bounded_prime. p = wip_prime_left_bounded_prime * wip_prime_right_bounded_prime -> wip_prime_left_bounded_prime = 1 \/ wip_prime_right_bounded_prime = 1)) -> (exists wip_weak_gap_bounded_length. wip_weak_gap_bounded_length + l = n) -> exists b c. (forall wip_index_bounded_result. (exists wip_gap_bounded_result_prefix_bound. wip_gap_bounded_result_prefix_bound + S wip_index_bounded_result = l) -> exists wip_mate_bounded_result. ((((exists wip_beta_height_bounded_result_decoded. wip_beta_height_bounded_result_decoded + S (wip_mate_bounded_result) = S ((S (wip_index_bounded_result)) * c)) /\ exists wip_beta_quotient_bounded_result_decoded. b = wip_beta_quotient_bounded_result_decoded * S ((S (wip_index_bounded_result)) * c) + (wip_mate_bounded_result))) /\ ((exists wip_gap_bounded_result_inverse_index_bound. wip_gap_bounded_result_inverse_index_bound + S wip_index_bounded_result = n) /\ ((exists wip_gap_bounded_result_inverse_mate_bound. wip_gap_bounded_result_inverse_mate_bound + S wip_mate_bounded_result = n) /\ (exists wip_mod_left_bounded_result_inverse_mod wip_mod_right_bounded_result_inverse_mod. ((S wip_index_bounded_result) * S wip_mate_bounded_result) + p * wip_mod_left_bounded_result_inverse_mod = 1 + p * wip_mod_right_bounded_result_inverse_mod)))))

Proof neighborhood

Direct theorem prerequisites

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA000X lt_to_le PA00A5 prime_inverse_prefix_extend

Direct theorem dependents

PA00A7 prime_inverse_prefix_exists

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

51 script commands · 15 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 (4)
add eq zero rightsucc ne zerolt to leprime inverse prefix extend
01Fix variables and assumptionsL1–2

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

  1. L1
    intro p
  2. L2
    intro n
02Induction on lL3–6

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

  1. L3
    induction l
  2. L4
    intro hpn
  3. L5
    intro hp
  4. L6
    intro hln
03Construct an explicit witnessL7–8

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

  1. L7
    exists 0
  2. L8
    exists 0
04Fix variables and assumptionsL9–10

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

  1. L9
    intro i
  2. L10
    intro hi
05Separate the logical casesL11–12

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

  1. L11
    exfalso
  2. L12
    cases hi
06Establish hsiL13–22

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

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

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

  1. L23
    intro hln
08Establish hprev_boundL24–28

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

  1. L24
    have hprev_bound : Le(l,n)Definitions: Le(l,n)Original native command in the exact edition
  2. L25
    specialize lt_to_le l
  3. L26
    specialize lt_to_le n
  4. L27
    apply lt_to_le
  5. L28
    exact hln
09Establish hprevL29–33

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

  1. L29
    have hprev : ∃ b. ∃ c. InversePrefix(p,n,b,c,l)Definitions: InversePrefix(p,n,b,c,l)Original native command in the exact edition
  2. L30
    apply IH
  3. L31
    exact hpn
  4. L32
    exact hp
  5. L33
    exact hprev_bound
10Separate the logical casesL34–35

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

  1. L34
    cases hprev
  2. L35
    cases hprev_witness
11Establish hnextL36–45

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

  1. L36
    have hnext : ∃ z. ∃ d. InversePrefix(p,n,z,d,S l)Definitions: InversePrefix(p,n,z,d,S l)Original native command in the exact edition
  2. L37
    specialize prime_inverse_prefix_extend p
  3. L38
    specialize prime_inverse_prefix_extend n
  4. L39
    specialize prime_inverse_prefix_extend x
  5. L40
    specialize prime_inverse_prefix_extend x1
  6. L41
    specialize prime_inverse_prefix_extend l
  7. L42
    apply prime_inverse_prefix_extend
  8. L43
    exact hpn
  9. L44
    exact hp
  10. L45
    exact hln
12Use earlier factsL46–46

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

  1. L46
    exact hprev_witness_witness
13Separate the logical casesL47–48

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

  1. L47
    cases hnext
  2. L48
    cases hnext_witness
14Construct an explicit witnessL49–50

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

  1. L49
    exists x2
  2. L50
    exists x3
15Use earlier factsL51–51

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

  1. L51
    exact hnext_witness_witness

Library-wide reading audit

Original defined command ledger · 51 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003induction l
  4. 0004intro hpn
  5. 0005intro hp
  6. 0006intro hln
  7. 0007exists 0
  8. 0008exists 0
  9. 0009intro i
  10. 0010intro hi
  11. 0011exfalso
  12. 0012cases hi
  13. 0013have hsi : S i = 0
  14. 0014specialize add_eq_zero_right x
  15. 0015specialize add_eq_zero_right (S i)
  16. 0016apply add_eq_zero_right
  17. 0017exact hi_witness
  18. 0018specialize succ_ne_zero i
  19. 0019apply succ_ne_zero
  20. 0020exact hsi
  21. 0021intro hpn
  22. 0022intro hp
  23. 0023intro hln
  24. 0024have hprev_bound : Le(l,n)
    Exact native replay linehave hprev_bound : exists h. h + l = n
  25. 0025specialize lt_to_le l
  26. 0026specialize lt_to_le n
  27. 0027apply lt_to_le
  28. 0028exact hln
  29. 0029have hprev : ∃ b. ∃ c. InversePrefix(p,n,b,c,l)
    Exact native replay linehave hprev : exists b c. (forall wip_index_bounded_previous. (exists wip_gap_bounded_previous_prefix_bound. wip_gap_bounded_previous_prefix_bound + S wip_index_bounded_previous = l) -> exists wip_mate_bounded_previous. ((((exists wip_beta_height_bounded_previous_decoded. wip_beta_height_bounded_previous_decoded + S (wip_mate_bounded_previous) = S ((S (wip_index_bounded_previous)) * c)) /\ exists wip_beta_quotient_bounded_previous_decoded. b = wip_beta_quotient_bounded_previous_decoded * S ((S (wip_index_bounded_previous)) * c) + (wip_mate_bounded_previous))) /\ ((exists wip_gap_bounded_previous_inverse_index_bound. wip_gap_bounded_previous_inverse_index_bound + S wip_index_bounded_previous = n) /\ ((exists wip_gap_bounded_previous_inverse_mate_bound. wip_gap_bounded_previous_inverse_mate_bound + S wip_mate_bounded_previous = n) /\ (exists wip_mod_left_bounded_previous_inverse_mod wip_mod_right_bounded_previous_inverse_mod. ((S wip_index_bounded_previous) * S wip_mate_bounded_previous) + p * wip_mod_left_bounded_previous_inverse_mod = 1 + p * wip_mod_right_bounded_previous_inverse_mod)))))
  30. 0030apply IH
  31. 0031exact hpn
  32. 0032exact hp
  33. 0033exact hprev_bound
  34. 0034cases hprev
  35. 0035cases hprev_witness
  36. 0036have hnext : ∃ z. ∃ d. InversePrefix(p,n,z,d,S l)
    Exact native replay linehave hnext : exists z d. (forall wip_index_bounded_successor. (exists wip_gap_bounded_successor_prefix_bound. wip_gap_bounded_successor_prefix_bound + S wip_index_bounded_successor = S l) -> exists wip_mate_bounded_successor. ((((exists wip_beta_height_bounded_successor_decoded. wip_beta_height_bounded_successor_decoded + S (wip_mate_bounded_successor) = S ((S (wip_index_bounded_successor)) * d)) /\ exists wip_beta_quotient_bounded_successor_decoded. z = wip_beta_quotient_bounded_successor_decoded * S ((S (wip_index_bounded_successor)) * d) + (wip_mate_bounded_successor))) /\ ((exists wip_gap_bounded_successor_inverse_index_bound. wip_gap_bounded_successor_inverse_index_bound + S wip_index_bounded_successor = n) /\ ((exists wip_gap_bounded_successor_inverse_mate_bound. wip_gap_bounded_successor_inverse_mate_bound + S wip_mate_bounded_successor = n) /\ (exists wip_mod_left_bounded_successor_inverse_mod wip_mod_right_bounded_successor_inverse_mod. ((S wip_index_bounded_successor) * S wip_mate_bounded_successor) + p * wip_mod_left_bounded_successor_inverse_mod = 1 + p * wip_mod_right_bounded_successor_inverse_mod)))))
  37. 0037specialize prime_inverse_prefix_extend p
  38. 0038specialize prime_inverse_prefix_extend n
  39. 0039specialize prime_inverse_prefix_extend x
  40. 0040specialize prime_inverse_prefix_extend x1
  41. 0041specialize prime_inverse_prefix_extend l
  42. 0042apply prime_inverse_prefix_extend
  43. 0043exact hpn
  44. 0044exact hp
  45. 0045exact hln
  46. 0046exact hprev_witness_witness
  47. 0047cases hnext
  48. 0048cases hnext_witness
  49. 0049exists x2
  50. 0050exists x3
  51. 0051exact hnext_witness_witness