PA009A · theorem

scaled_inverse_prefix_mate_predecessor

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

Every positive decoded mate has a predecessor inside the source bound.

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

4 occurrences

In local proof propositions

PD0002 Lt PD0038 ScaledInverseIndex

2 occurrences

Exact expanded native-PA statement
forall p a n b c i y. p = S n -> (forall esip_index_predecessor_prefix. (exists esip_gap_predecessor_prefix_prefix_bound. esip_gap_predecessor_prefix_prefix_bound + S (esip_index_predecessor_prefix) = n) -> exists esip_mate_predecessor_prefix. ((((exists ff_h_esip_predecessor_prefix_entry. ff_h_esip_predecessor_prefix_entry + S (esip_mate_predecessor_prefix) = S ((S (esip_index_predecessor_prefix)) * c)) /\ exists ff_q_esip_predecessor_prefix_entry. b = ff_q_esip_predecessor_prefix_entry * S ((S (esip_index_predecessor_prefix)) * c) + (esip_mate_predecessor_prefix))) /\ ((exists esip_gap_predecessor_prefix_relation_index_bound. esip_gap_predecessor_prefix_relation_index_bound + S (esip_index_predecessor_prefix) = n) /\ ((((~((S esip_index_predecessor_prefix) = 0) /\ (exists esip_gap_predecessor_prefix_relation_scaled_left_bound. esip_gap_predecessor_prefix_relation_scaled_left_bound + S (S esip_index_predecessor_prefix) = p))) /\ (((~(esip_mate_predecessor_prefix = 0) /\ (exists esip_gap_predecessor_prefix_relation_scaled_right_bound. esip_gap_predecessor_prefix_relation_scaled_right_bound + S (esip_mate_predecessor_prefix) = p))) /\ (exists esi_mod_left_predecessor_prefix_relation_scaled_mod esi_mod_right_predecessor_prefix_relation_scaled_mod. ((S esip_index_predecessor_prefix) * esip_mate_predecessor_prefix) + p * esi_mod_left_predecessor_prefix_relation_scaled_mod = (a) + p * esi_mod_right_predecessor_prefix_relation_scaled_mod))))))) -> (exists esip_gap_predecessor_source_bound. esip_gap_predecessor_source_bound + S (i) = n) -> (((exists ff_h_esipe_predecessor_at. ff_h_esipe_predecessor_at + S (y) = S ((S (i)) * c)) /\ exists ff_q_esipe_predecessor_at. b = ff_q_esipe_predecessor_at * S ((S (i)) * c) + (y))) -> exists j. y = S j /\ (exists esip_gap_predecessor_result_bound. esip_gap_predecessor_result_bound + S (j) = n)

Proof neighborhood

Direct theorem prerequisites

PA0099 scaled_inverse_prefix_entry_sound PA001V nonzero_is_succ PA000V le_of_succ_le_succ

Direct theorem dependents

PA009E scaled_inverse_prefix_involutive

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

44 script commands · 11 reading checkpoints · 3 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 (3)
scaled inverse prefix entry soundnonzero is succle of succ le succ
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 hprefix
  10. L10
    intro hi
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hat
03Establish hrelationL12–21

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

  1. L12
    have hrelation : ScaledInverseIndex(p,a,n,i,y)Definitions: ScaledInverseIndex(p,a,n,i,y)Original native command in the exact edition
  2. L13
    specialize scaled_inverse_prefix_entry_sound p
  3. L14
    specialize scaled_inverse_prefix_entry_sound a
  4. L15
    specialize scaled_inverse_prefix_entry_sound n
  5. L16
    specialize scaled_inverse_prefix_entry_sound b
  6. L17
    specialize scaled_inverse_prefix_entry_sound c
  7. L18
    specialize scaled_inverse_prefix_entry_sound n
  8. L19
    specialize scaled_inverse_prefix_entry_sound i
  9. L20
    specialize scaled_inverse_prefix_entry_sound y
  10. L21
    apply scaled_inverse_prefix_entry_sound
04Use earlier factsL22–24

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

  1. L22
    exact hprefix
  2. L23
    exact hi
  3. L24
    exact hat
05Separate the logical casesL25–28

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

  1. L25
    cases hrelation
  2. L26
    cases hrelation_right
  3. L27
    cases hrelation_right_right
  4. L28
    cases hrelation_right_right_left
06Establish hshapeL29–32

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

  1. L29
    have hshape : exists j. y = S j
  2. L30
    specialize nonzero_is_succ y
  3. L31
    apply nonzero_is_succ
  4. L32
    exact hrelation_right_right_left_left
07Separate the logical casesL33–33

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

  1. L33
    cases hshape
08Establish hjnL34–40

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

  1. L34
  2. L35
    rewrite hshape_witness at hrelation_right_right_left_right
  3. L36
    rewrite hpn at hrelation_right_right_left_right
  4. L37
    specialize le_of_succ_le_succ (S x)
  5. L38
    specialize le_of_succ_le_succ n
  6. L39
    apply le_of_succ_le_succ
  7. L40
    exact hrelation_right_right_left_right
09Construct an explicit witnessL41–41

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

  1. L41
    exists x
10Separate the logical casesL42–42

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

  1. L42
    split
11Use earlier factsL43–44

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

  1. L43
    exact hshape_witness
  2. L44
    exact hjn

Library-wide reading audit

Original defined command ledger · 44 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 hprefix
  10. 0010intro hi
  11. 0011intro hat
  12. 0012have hrelation : ScaledInverseIndex(p,a,n,i,y)
    Exact native replay linehave hrelation : (exists esip_gap_predecessor_relation_index_bound. esip_gap_predecessor_relation_index_bound + S (i) = n) /\ ((((~((S i) = 0) /\ (exists esip_gap_predecessor_relation_scaled_left_bound. esip_gap_predecessor_relation_scaled_left_bound + S (S i) = p))) /\ (((~(y = 0) /\ (exists esip_gap_predecessor_relation_scaled_right_bound. esip_gap_predecessor_relation_scaled_right_bound + S (y) = p))) /\ (exists esi_mod_left_predecessor_relation_scaled_mod esi_mod_right_predecessor_relation_scaled_mod. ((S i) * y) + p * esi_mod_left_predecessor_relation_scaled_mod = (a) + p * esi_mod_right_predecessor_relation_scaled_mod))))
  13. 0013specialize scaled_inverse_prefix_entry_sound p
  14. 0014specialize scaled_inverse_prefix_entry_sound a
  15. 0015specialize scaled_inverse_prefix_entry_sound n
  16. 0016specialize scaled_inverse_prefix_entry_sound b
  17. 0017specialize scaled_inverse_prefix_entry_sound c
  18. 0018specialize scaled_inverse_prefix_entry_sound n
  19. 0019specialize scaled_inverse_prefix_entry_sound i
  20. 0020specialize scaled_inverse_prefix_entry_sound y
  21. 0021apply scaled_inverse_prefix_entry_sound
  22. 0022exact hprefix
  23. 0023exact hi
  24. 0024exact hat
  25. 0025cases hrelation
  26. 0026cases hrelation_right
  27. 0027cases hrelation_right_right
  28. 0028cases hrelation_right_right_left
  29. 0029have hshape : exists j. y = S j
  30. 0030specialize nonzero_is_succ y
  31. 0031apply nonzero_is_succ
  32. 0032exact hrelation_right_right_left_left
  33. 0033cases hshape
  34. 0034have hjn : Lt(x,n)
    Exact native replay linehave hjn : exists h. h + S x = n
  35. 0035rewrite hshape_witness at hrelation_right_right_left_right
  36. 0036rewrite hpn at hrelation_right_right_left_right
  37. 0037specialize le_of_succ_le_succ (S x)
  38. 0038specialize le_of_succ_le_succ n
  39. 0039apply le_of_succ_le_succ
  40. 0040exact hrelation_right_right_left_right
  41. 0041exists x
  42. 0042split
  43. 0043exact hshape_witness
  44. 0044exact hjn