PA009E · theorem

scaled_inverse_prefix_involutive

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

Decoding a scaled-inverse mate and decoding its predecessor returns the source residue.

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

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

6 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0033 ScaledInverse PD0038 ScaledInverseIndex

6 occurrences

Exact expanded native-PA statement
forall p a n b c i y. p = S n -> ((~(p = 1) /\ forall esi_prime_left_esipe_involutive_prime esi_prime_right_esipe_involutive_prime. p = esi_prime_left_esipe_involutive_prime * esi_prime_right_esipe_involutive_prime -> esi_prime_left_esipe_involutive_prime = 1 \/ esi_prime_right_esipe_involutive_prime = 1)) -> (forall esip_index_involutive_prefix. (exists esip_gap_involutive_prefix_prefix_bound. esip_gap_involutive_prefix_prefix_bound + S (esip_index_involutive_prefix) = n) -> exists esip_mate_involutive_prefix. ((((exists ff_h_esip_involutive_prefix_entry. ff_h_esip_involutive_prefix_entry + S (esip_mate_involutive_prefix) = S ((S (esip_index_involutive_prefix)) * c)) /\ exists ff_q_esip_involutive_prefix_entry. b = ff_q_esip_involutive_prefix_entry * S ((S (esip_index_involutive_prefix)) * c) + (esip_mate_involutive_prefix))) /\ ((exists esip_gap_involutive_prefix_relation_index_bound. esip_gap_involutive_prefix_relation_index_bound + S (esip_index_involutive_prefix) = n) /\ ((((~((S esip_index_involutive_prefix) = 0) /\ (exists esip_gap_involutive_prefix_relation_scaled_left_bound. esip_gap_involutive_prefix_relation_scaled_left_bound + S (S esip_index_involutive_prefix) = p))) /\ (((~(esip_mate_involutive_prefix = 0) /\ (exists esip_gap_involutive_prefix_relation_scaled_right_bound. esip_gap_involutive_prefix_relation_scaled_right_bound + S (esip_mate_involutive_prefix) = p))) /\ (exists esi_mod_left_involutive_prefix_relation_scaled_mod esi_mod_right_involutive_prefix_relation_scaled_mod. ((S esip_index_involutive_prefix) * esip_mate_involutive_prefix) + p * esi_mod_left_involutive_prefix_relation_scaled_mod = (a) + p * esi_mod_right_involutive_prefix_relation_scaled_mod))))))) -> (exists esip_gap_involutive_bound. esip_gap_involutive_bound + S (i) = n) -> (((exists ff_h_esipe_involutive_at. ff_h_esipe_involutive_at + S (y) = S ((S (i)) * c)) /\ exists ff_q_esipe_involutive_at. b = ff_q_esipe_involutive_at * S ((S (i)) * c) + (y))) -> exists j. y = S j /\ ((exists esip_gap_involutive_mate_bound. esip_gap_involutive_mate_bound + S (j) = n) /\ (((exists ff_h_esipe_involutive_back. ff_h_esipe_involutive_back + S (S i) = S ((S (j)) * c)) /\ exists ff_q_esipe_involutive_back. b = ff_q_esipe_involutive_back * S ((S (j)) * c) + (S i))))

Proof neighborhood

Direct theorem prerequisites

PA009A scaled_inverse_prefix_mate_predecessor PA0099 scaled_inverse_prefix_entry_sound PA009B scaled_inverse_symmetric PA009D scaled_inverse_prefix_extensional

Direct theorem dependents

PA009I scaled_inverse_prefix_choose_omitted_orbit

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

77 script commands · 20 reading checkpoints · 6 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)
scaled inverse prefix mate predecessorscaled inverse prefix entry soundscaled inverse symmetricscaled inverse prefix extensional
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 i
  7. L7
    intro y
  8. L8
    intro hpn
  9. L9
    intro hp
  10. L10
    intro hprefix
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hi
  2. L12
    intro hat
03Establish hpredecessorL13–22

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

  1. L13
    have hpredecessor : ∃ j. y = S j ∧ Lt(j,n)Definitions: Lt(j,n)Original native command in the exact edition
  2. L14
    specialize scaled_inverse_prefix_mate_predecessor p
  3. L15
    specialize scaled_inverse_prefix_mate_predecessor a
  4. L16
    specialize scaled_inverse_prefix_mate_predecessor n
  5. L17
    specialize scaled_inverse_prefix_mate_predecessor b
  6. L18
    specialize scaled_inverse_prefix_mate_predecessor c
  7. L19
    specialize scaled_inverse_prefix_mate_predecessor i
  8. L20
    specialize scaled_inverse_prefix_mate_predecessor y
  9. L21
    apply scaled_inverse_prefix_mate_predecessor
  10. L22
    exact hpn
04Use earlier factsL23–25

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

  1. L23
    exact hprefix
  2. L24
    exact hi
  3. L25
    exact hat
05Separate the logical casesL26–27

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

  1. L26
    cases hpredecessor
  2. L27
    cases hpredecessor_witness
06Establish hforward_relationL28–37

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

  1. L28
    have hforward_relation : ScaledInverseIndex(p,a,n,i,y)Definitions: ScaledInverseIndex(p,a,n,i,y)Original native command in the exact edition
  2. L29
    specialize scaled_inverse_prefix_entry_sound p
  3. L30
    specialize scaled_inverse_prefix_entry_sound a
  4. L31
    specialize scaled_inverse_prefix_entry_sound n
  5. L32
    specialize scaled_inverse_prefix_entry_sound b
  6. L33
    specialize scaled_inverse_prefix_entry_sound c
  7. L34
    specialize scaled_inverse_prefix_entry_sound n
  8. L35
    specialize scaled_inverse_prefix_entry_sound i
  9. L36
    specialize scaled_inverse_prefix_entry_sound y
  10. L37
    apply scaled_inverse_prefix_entry_sound
07Use earlier factsL38–40

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

  1. L38
    exact hprefix
  2. L39
    exact hi
  3. L40
    exact hat
08Separate the logical casesL41–41

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

  1. L41
    cases hforward_relation
09Establish hforwardL42–46

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

  1. L42
    have hforward : ScaledInverse(p,a,S i,S x)Definitions: ScaledInverse(p,a,S i,S x)Original native command in the exact edition
  2. L43
    rewrite hpredecessor_witness_left at hforward_relation_right
  3. L44
    rewrite hpredecessor_witness_left at hforward_relation_right
  4. L45
    rewrite hpredecessor_witness_left at hforward_relation_right
  5. L46
    exact hforward_relation_right
10Establish hreverseL47–53

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

  1. L47
    have hreverse : ScaledInverse(p,a,S x,S i)Definitions: ScaledInverse(p,a,S x,S i)Original native command in the exact edition
  2. L48
    specialize scaled_inverse_symmetric p
  3. L49
    specialize scaled_inverse_symmetric a
  4. L50
    specialize scaled_inverse_symmetric (S i)
  5. L51
    specialize scaled_inverse_symmetric (S x)
  6. L52
    apply scaled_inverse_symmetric
  7. L53
    exact hforward
11Establish hreverse_relationL54–54

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

  1. L54
    have hreverse_relation : ScaledInverseIndex(p,a,n,x,S i)Definitions: ScaledInverseIndex(p,a,n,x,S i)Original native command in the exact edition
12Separate the logical casesL55–55

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

  1. L55
    split
13Use earlier factsL56–57

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

  1. L56
    exact hpredecessor_witness_right
  2. L57
    exact hreverse
14Establish hbackL58–67

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

  1. L58
    have hback : BetaAt(b,c,x,S i)Definitions: BetaAt(b,c,x,S i)Original native command in the exact edition
  2. L59
    specialize scaled_inverse_prefix_extensional p
  3. L60
    specialize scaled_inverse_prefix_extensional a
  4. L61
    specialize scaled_inverse_prefix_extensional n
  5. L62
    specialize scaled_inverse_prefix_extensional b
  6. L63
    specialize scaled_inverse_prefix_extensional c
  7. L64
    specialize scaled_inverse_prefix_extensional n
  8. L65
    specialize scaled_inverse_prefix_extensional x
  9. L66
    specialize scaled_inverse_prefix_extensional (S i)
  10. L67
    apply scaled_inverse_prefix_extensional
15Use earlier factsL68–71

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

  1. L68
    exact hp
  2. L69
    exact hprefix
  3. L70
    exact hpredecessor_witness_right
  4. L71
    exact hreverse_relation
16Construct an explicit witnessL72–72

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

  1. L72
    exists x
17Separate the logical casesL73–73

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

  1. L73
    split
18Use earlier factsL74–74

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

  1. L74
    exact hpredecessor_witness_left
19Separate the logical casesL75–75

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

  1. L75
    split
20Use earlier factsL76–77

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

  1. L76
    exact hpredecessor_witness_right
  2. L77
    exact hback

Library-wide reading audit

Original defined command ledger · 77 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro n
  4. 0004intro b
  5. 0005intro c
  6. 0006intro i
  7. 0007intro y
  8. 0008intro hpn
  9. 0009intro hp
  10. 0010intro hprefix
  11. 0011intro hi
  12. 0012intro hat
  13. 0013have hpredecessor : ∃ j. y = S j ∧ Lt(j,n)
    Exact native replay linehave hpredecessor : exists j. y = S j /\ (exists esip_gap_involutive_mate_bound. esip_gap_involutive_mate_bound + S (j) = n)
  14. 0014specialize scaled_inverse_prefix_mate_predecessor p
  15. 0015specialize scaled_inverse_prefix_mate_predecessor a
  16. 0016specialize scaled_inverse_prefix_mate_predecessor n
  17. 0017specialize scaled_inverse_prefix_mate_predecessor b
  18. 0018specialize scaled_inverse_prefix_mate_predecessor c
  19. 0019specialize scaled_inverse_prefix_mate_predecessor i
  20. 0020specialize scaled_inverse_prefix_mate_predecessor y
  21. 0021apply scaled_inverse_prefix_mate_predecessor
  22. 0022exact hpn
  23. 0023exact hprefix
  24. 0024exact hi
  25. 0025exact hat
  26. 0026cases hpredecessor
  27. 0027cases hpredecessor_witness
  28. 0028have hforward_relation : ScaledInverseIndex(p,a,n,i,y)
    Exact native replay linehave hforward_relation : (exists esip_gap_involutive_forward_relation_index_bound. esip_gap_involutive_forward_relation_index_bound + S (i) = n) /\ ((((~((S i) = 0) /\ (exists esip_gap_involutive_forward_relation_scaled_left_bound. esip_gap_involutive_forward_relation_scaled_left_bound + S (S i) = p))) /\ (((~(y = 0) /\ (exists esip_gap_involutive_forward_relation_scaled_right_bound. esip_gap_involutive_forward_relation_scaled_right_bound + S (y) = p))) /\ (exists esi_mod_left_involutive_forward_relation_scaled_mod esi_mod_right_involutive_forward_relation_scaled_mod. ((S i) * y) + p * esi_mod_left_involutive_forward_relation_scaled_mod = (a) + p * esi_mod_right_involutive_forward_relation_scaled_mod))))
  29. 0029specialize scaled_inverse_prefix_entry_sound p
  30. 0030specialize scaled_inverse_prefix_entry_sound a
  31. 0031specialize scaled_inverse_prefix_entry_sound n
  32. 0032specialize scaled_inverse_prefix_entry_sound b
  33. 0033specialize scaled_inverse_prefix_entry_sound c
  34. 0034specialize scaled_inverse_prefix_entry_sound n
  35. 0035specialize scaled_inverse_prefix_entry_sound i
  36. 0036specialize scaled_inverse_prefix_entry_sound y
  37. 0037apply scaled_inverse_prefix_entry_sound
  38. 0038exact hprefix
  39. 0039exact hi
  40. 0040exact hat
  41. 0041cases hforward_relation
  42. 0042have hforward : ScaledInverse(p,a,S i,S x)
    Exact native replay linehave hforward : (((~((S i) = 0) /\ (exists esip_gap_involutive_forward_scaled_left_bound. esip_gap_involutive_forward_scaled_left_bound + S (S i) = p))) /\ (((~(S x = 0) /\ (exists esip_gap_involutive_forward_scaled_right_bound. esip_gap_involutive_forward_scaled_right_bound + S (S x) = p))) /\ (exists esi_mod_left_involutive_forward_scaled_mod esi_mod_right_involutive_forward_scaled_mod. ((S i) * S x) + p * esi_mod_left_involutive_forward_scaled_mod = (a) + p * esi_mod_right_involutive_forward_scaled_mod)))
  43. 0043rewrite hpredecessor_witness_left at hforward_relation_right
  44. 0044rewrite hpredecessor_witness_left at hforward_relation_right
  45. 0045rewrite hpredecessor_witness_left at hforward_relation_right
  46. 0046exact hforward_relation_right
  47. 0047have hreverse : ScaledInverse(p,a,S x,S i)
    Exact native replay linehave hreverse : (((~((S x) = 0) /\ (exists esip_gap_involutive_reverse_scaled_left_bound. esip_gap_involutive_reverse_scaled_left_bound + S (S x) = p))) /\ (((~(S i = 0) /\ (exists esip_gap_involutive_reverse_scaled_right_bound. esip_gap_involutive_reverse_scaled_right_bound + S (S i) = p))) /\ (exists esi_mod_left_involutive_reverse_scaled_mod esi_mod_right_involutive_reverse_scaled_mod. ((S x) * S i) + p * esi_mod_left_involutive_reverse_scaled_mod = (a) + p * esi_mod_right_involutive_reverse_scaled_mod)))
  48. 0048specialize scaled_inverse_symmetric p
  49. 0049specialize scaled_inverse_symmetric a
  50. 0050specialize scaled_inverse_symmetric (S i)
  51. 0051specialize scaled_inverse_symmetric (S x)
  52. 0052apply scaled_inverse_symmetric
  53. 0053exact hforward
  54. 0054have hreverse_relation : ScaledInverseIndex(p,a,n,x,S i)
    Exact native replay linehave hreverse_relation : (exists esip_gap_involutive_reverse_relation_index_bound. esip_gap_involutive_reverse_relation_index_bound + S (x) = n) /\ ((((~((S x) = 0) /\ (exists esip_gap_involutive_reverse_relation_scaled_left_bound. esip_gap_involutive_reverse_relation_scaled_left_bound + S (S x) = p))) /\ (((~(S i = 0) /\ (exists esip_gap_involutive_reverse_relation_scaled_right_bound. esip_gap_involutive_reverse_relation_scaled_right_bound + S (S i) = p))) /\ (exists esi_mod_left_involutive_reverse_relation_scaled_mod esi_mod_right_involutive_reverse_relation_scaled_mod. ((S x) * S i) + p * esi_mod_left_involutive_reverse_relation_scaled_mod = (a) + p * esi_mod_right_involutive_reverse_relation_scaled_mod))))
  55. 0055split
  56. 0056exact hpredecessor_witness_right
  57. 0057exact hreverse
  58. 0058have hback : BetaAt(b,c,x,S i)
    Exact native replay linehave hback : ((exists ff_h_esipe_involutive_back. ff_h_esipe_involutive_back + S (S i) = S ((S (x)) * c)) /\ exists ff_q_esipe_involutive_back. b = ff_q_esipe_involutive_back * S ((S (x)) * c) + (S i))
  59. 0059specialize scaled_inverse_prefix_extensional p
  60. 0060specialize scaled_inverse_prefix_extensional a
  61. 0061specialize scaled_inverse_prefix_extensional n
  62. 0062specialize scaled_inverse_prefix_extensional b
  63. 0063specialize scaled_inverse_prefix_extensional c
  64. 0064specialize scaled_inverse_prefix_extensional n
  65. 0065specialize scaled_inverse_prefix_extensional x
  66. 0066specialize scaled_inverse_prefix_extensional (S i)
  67. 0067apply scaled_inverse_prefix_extensional
  68. 0068exact hp
  69. 0069exact hprefix
  70. 0070exact hpredecessor_witness_right
  71. 0071exact hreverse_relation
  72. 0072exists x
  73. 0073split
  74. 0074exact hpredecessor_witness_left
  75. 0075split
  76. 0076exact hpredecessor_witness_right
  77. 0077exact hback