PA009A

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.

Exact expanded 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)

Structural proof guide

Generated structural guide

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

Use the direct prerequisites scaled_inverse_prefix_entry_sound, nonzero_is_succ, le_of_succ_le_succ as previously established PA formulas.

The proof proceeds by case analysis (5), intermediate claims (3), equality transport (2).

Referenced ingredients

PA0099 scaled_inverse_prefix_entry_sound PA001V nonzero_is_succ PA000V le_of_succ_le_succ

Proof neighborhood

Direct dependencies

PA0099 scaled_inverse_prefix_entry_sound PA001V nonzero_is_succ PA000V le_of_succ_le_succ

Direct dependents

PA009E scaled_inverse_prefix_involutive

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

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.

Named ingredients (3)
scaled inverse prefix entry soundnonzero is succle of succ le succ

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–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
  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
    have hjn : exists h. h + S x = n
  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 exact 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 : (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 : 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