PA00AH · theorem

prime_inverse_prefix_fixed_cases

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

A fixed zero-based inverse index is zero or the last index.

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. ∀ b. ∀ c. ∀ i. p = S n → Prime(p) → InversePrefix(p,n,b,c,n) → Lt(i,n) → BetaAt(b,c,i,i) → i = 0 ∨ S i = n

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 PD0037 InversePrefix

4 occurrences

In local proof propositions

PD0002 Lt PD0036 InverseIndex

3 occurrences

Exact expanded native-PA statement
forall p n b c i. p = S n -> ((~(p = 1) /\ forall wip_prime_left_fixed_prime wip_prime_right_fixed_prime. p = wip_prime_left_fixed_prime * wip_prime_right_fixed_prime -> wip_prime_left_fixed_prime = 1 \/ wip_prime_right_fixed_prime = 1)) -> (forall wip_index_fixed_prefix. (exists wip_gap_fixed_prefix_prefix_bound. wip_gap_fixed_prefix_prefix_bound + S wip_index_fixed_prefix = n) -> exists wip_mate_fixed_prefix. ((((exists wip_beta_height_fixed_prefix_decoded. wip_beta_height_fixed_prefix_decoded + S (wip_mate_fixed_prefix) = S ((S (wip_index_fixed_prefix)) * c)) /\ exists wip_beta_quotient_fixed_prefix_decoded. b = wip_beta_quotient_fixed_prefix_decoded * S ((S (wip_index_fixed_prefix)) * c) + (wip_mate_fixed_prefix))) /\ ((exists wip_gap_fixed_prefix_inverse_index_bound. wip_gap_fixed_prefix_inverse_index_bound + S wip_index_fixed_prefix = n) /\ ((exists wip_gap_fixed_prefix_inverse_mate_bound. wip_gap_fixed_prefix_inverse_mate_bound + S wip_mate_fixed_prefix = n) /\ (exists wip_mod_left_fixed_prefix_inverse_mod wip_mod_right_fixed_prefix_inverse_mod. ((S wip_index_fixed_prefix) * S wip_mate_fixed_prefix) + p * wip_mod_left_fixed_prefix_inverse_mod = 1 + p * wip_mod_right_fixed_prefix_inverse_mod))))) -> (exists wip_gap_fixed_index_bound. wip_gap_fixed_index_bound + S i = n) -> (((exists wip_beta_height_fixed_entry. wip_beta_height_fixed_entry + S (i) = S ((S (i)) * c)) /\ exists wip_beta_quotient_fixed_entry. b = wip_beta_quotient_fixed_entry * S ((S (i)) * c) + (i))) -> i = 0 \/ S i = n

Proof neighborhood

Direct theorem prerequisites

PA00AF inverse_prefix_entry_sound PA002K succ_le_succ PA00AG prime_bounded_square_one_cases PA003V succ_injective

Direct theorem dependents

PA00AI prime_inverse_prefix_nonendpoint_not_fixed

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

53 script commands · 13 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)
inverse prefix entry soundsucc le succprime bounded square one casessucc injective
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro i
  6. L6
    intro hpn
  7. L7
    intro hp
  8. L8
    intro hprefix
  9. L9
    intro hi
  10. L10
    intro hfixed
02Establish hidxL11–20

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

  1. L11
    have hidx : InverseIndex(p,n,i,i)Definitions: InverseIndex(p,n,i,i)Original native command in the exact edition
  2. L12
    specialize inverse_prefix_entry_sound p
  3. L13
    specialize inverse_prefix_entry_sound n
  4. L14
    specialize inverse_prefix_entry_sound b
  5. L15
    specialize inverse_prefix_entry_sound c
  6. L16
    specialize inverse_prefix_entry_sound n
  7. L17
    specialize inverse_prefix_entry_sound i
  8. L18
    specialize inverse_prefix_entry_sound i
  9. L19
    apply inverse_prefix_entry_sound
  10. L20
    exact hprefix
03Use earlier factsL21–22

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

  1. L21
    exact hi
  2. L22
    exact hfixed
04Separate the logical casesL23–24

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

  1. L23
    cases hidx
  2. L24
    cases hidx_right
05Establish hpositiveL25–25

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

  1. L25
    have hpositive : Lt(0,S i)Definitions: Lt(0,S i)Original native command in the exact edition
06Construct an explicit witnessL26–26

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

  1. L26
    exists i
07Calculate and transport equalitiesL27–29

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

  1. L27
    rewrite PA4
  2. L28
    rewrite PA3
  3. L29
    refl
08Establish hboundedL30–35

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

  1. L30
    have hbounded : Lt(S i,p)Definitions: Lt(S i,p)Original native command in the exact edition
  2. L31
    rewrite hpn
  3. L32
    specialize succ_le_succ (S i)
  4. L33
    specialize succ_le_succ n
  5. L34
    apply succ_le_succ
  6. L35
    exact hidx_left
09Establish hcasesL36–45

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime bounded square one cases.

  1. L36
    have hcases : S i = 1 \/ S i = n
  2. L37
    specialize prime_bounded_square_one_cases p
  3. L38
    specialize prime_bounded_square_one_cases n
  4. L39
    specialize prime_bounded_square_one_cases (S i)
  5. L40
    apply prime_bounded_square_one_cases
  6. L41
    exact hpn
  7. L42
    exact hp
  8. L43
    exact hpositive
  9. L44
    exact hbounded
  10. L45
    exact hidx_right_right
10Separate the logical casesL46–47

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

  1. L46
    cases hcases
  2. L47
    left
11Use earlier factsL48–51

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

  1. L48
    specialize succ_injective i
  2. L49
    specialize succ_injective 0
  3. L50
    apply succ_injective
  4. L51
    exact hcases_left
12Separate the logical casesL52–52

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

  1. L52
    right
13Use earlier factsL53–53

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

  1. L53
    exact hcases_right

Library-wide reading audit

Original defined command ledger · 53 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro i
  6. 0006intro hpn
  7. 0007intro hp
  8. 0008intro hprefix
  9. 0009intro hi
  10. 0010intro hfixed
  11. 0011have hidx : InverseIndex(p,n,i,i)
    Exact native replay linehave hidx : (exists wip_gap_fixed_inverse_index_bound. wip_gap_fixed_inverse_index_bound + S i = n) /\ ((exists wip_gap_fixed_inverse_mate_bound. wip_gap_fixed_inverse_mate_bound + S i = n) /\ (exists wip_mod_left_fixed_inverse_mod wip_mod_right_fixed_inverse_mod. ((S i) * S i) + p * wip_mod_left_fixed_inverse_mod = 1 + p * wip_mod_right_fixed_inverse_mod))
  12. 0012specialize inverse_prefix_entry_sound p
  13. 0013specialize inverse_prefix_entry_sound n
  14. 0014specialize inverse_prefix_entry_sound b
  15. 0015specialize inverse_prefix_entry_sound c
  16. 0016specialize inverse_prefix_entry_sound n
  17. 0017specialize inverse_prefix_entry_sound i
  18. 0018specialize inverse_prefix_entry_sound i
  19. 0019apply inverse_prefix_entry_sound
  20. 0020exact hprefix
  21. 0021exact hi
  22. 0022exact hfixed
  23. 0023cases hidx
  24. 0024cases hidx_right
  25. 0025have hpositive : Lt(0,S i)
    Exact native replay linehave hpositive : exists wii_positive_gap_fixed_positive. wii_positive_gap_fixed_positive + 1 = S i
  26. 0026exists i
  27. 0027rewrite PA4
  28. 0028rewrite PA3
  29. 0029refl
  30. 0030have hbounded : Lt(S i,p)
    Exact native replay linehave hbounded : exists wii_successor_gap_fixed_residue_bound. wii_successor_gap_fixed_residue_bound + S (S i) = p
  31. 0031rewrite hpn
  32. 0032specialize succ_le_succ (S i)
  33. 0033specialize succ_le_succ n
  34. 0034apply succ_le_succ
  35. 0035exact hidx_left
  36. 0036have hcases : S i = 1 \/ S i = n
  37. 0037specialize prime_bounded_square_one_cases p
  38. 0038specialize prime_bounded_square_one_cases n
  39. 0039specialize prime_bounded_square_one_cases (S i)
  40. 0040apply prime_bounded_square_one_cases
  41. 0041exact hpn
  42. 0042exact hp
  43. 0043exact hpositive
  44. 0044exact hbounded
  45. 0045exact hidx_right_right
  46. 0046cases hcases
  47. 0047left
  48. 0048specialize succ_injective i
  49. 0049specialize succ_injective 0
  50. 0050apply succ_injective
  51. 0051exact hcases_left
  52. 0052right
  53. 0053exact hcases_right