PA0099

scaled_inverse_prefix_entry_sound

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

Every decoded scaled-inverse prefix entry satisfies its stored relation.

Exact expanded PA statement

forall p a n b c l i y. (forall esip_index_ext_entry_prefix. (exists esip_gap_ext_entry_prefix_prefix_bound. esip_gap_ext_entry_prefix_prefix_bound + S (esip_index_ext_entry_prefix) = l) -> exists esip_mate_ext_entry_prefix. ((((exists ff_h_esip_ext_entry_prefix_entry. ff_h_esip_ext_entry_prefix_entry + S (esip_mate_ext_entry_prefix) = S ((S (esip_index_ext_entry_prefix)) * c)) /\ exists ff_q_esip_ext_entry_prefix_entry. b = ff_q_esip_ext_entry_prefix_entry * S ((S (esip_index_ext_entry_prefix)) * c) + (esip_mate_ext_entry_prefix))) /\ ((exists esip_gap_ext_entry_prefix_relation_index_bound. esip_gap_ext_entry_prefix_relation_index_bound + S (esip_index_ext_entry_prefix) = n) /\ ((((~((S esip_index_ext_entry_prefix) = 0) /\ (exists esip_gap_ext_entry_prefix_relation_scaled_left_bound. esip_gap_ext_entry_prefix_relation_scaled_left_bound + S (S esip_index_ext_entry_prefix) = p))) /\ (((~(esip_mate_ext_entry_prefix = 0) /\ (exists esip_gap_ext_entry_prefix_relation_scaled_right_bound. esip_gap_ext_entry_prefix_relation_scaled_right_bound + S (esip_mate_ext_entry_prefix) = p))) /\ (exists esi_mod_left_ext_entry_prefix_relation_scaled_mod esi_mod_right_ext_entry_prefix_relation_scaled_mod. ((S esip_index_ext_entry_prefix) * esip_mate_ext_entry_prefix) + p * esi_mod_left_ext_entry_prefix_relation_scaled_mod = (a) + p * esi_mod_right_ext_entry_prefix_relation_scaled_mod))))))) -> (exists esip_gap_ext_entry_bound. esip_gap_ext_entry_bound + S (i) = l) -> (((exists ff_h_esipe_entry_at. ff_h_esipe_entry_at + S (y) = S ((S (i)) * c)) /\ exists ff_q_esipe_entry_at. b = ff_q_esipe_entry_at * S ((S (i)) * c) + (y))) -> ((exists esip_gap_ext_entry_relation_index_bound. esip_gap_ext_entry_relation_index_bound + S (i) = n) /\ ((((~((S i) = 0) /\ (exists esip_gap_ext_entry_relation_scaled_left_bound. esip_gap_ext_entry_relation_scaled_left_bound + S (S i) = p))) /\ (((~(y = 0) /\ (exists esip_gap_ext_entry_relation_scaled_right_bound. esip_gap_ext_entry_relation_scaled_right_bound + S (y) = p))) /\ (exists esi_mod_left_ext_entry_relation_scaled_mod esi_mod_right_ext_entry_relation_scaled_mod. ((S i) * y) + p * esi_mod_left_ext_entry_relation_scaled_mod = (a) + p * esi_mod_right_ext_entry_relation_scaled_mod)))))

Structural proof guide

Generated structural guide

Every decoded scaled-inverse prefix entry satisfies its stored relation.

Use the direct prerequisites beta_at_unique as previously established PA formulas.

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

Referenced ingredients

PA002F beta_at_unique

Proof neighborhood

Direct dependencies

PA002F beta_at_unique

Direct dependents

PA009A scaled_inverse_prefix_mate_predecessor PA009E scaled_inverse_prefix_involutive PA009H scaled_inverse_prefix_no_fixed_of_not_qres

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro p
  2. 0002intro a
  3. 0003intro n
  4. 0004intro b
  5. 0005intro c
  6. 0006intro l
  7. 0007intro i
  8. 0008intro y
  9. 0009intro hprefix
  10. 0010intro hi
  11. 0011intro hat
  12. 0012have hstored : exists z. ((((exists ff_h_esipe_stored_at. ff_h_esipe_stored_at + S (z) = S ((S (i)) * c)) /\ exists ff_q_esipe_stored_at. b = ff_q_esipe_stored_at * S ((S (i)) * c) + (z))) /\ ((exists esip_gap_ext_stored_relation_index_bound. esip_gap_ext_stored_relation_index_bound + S (i) = n) /\ ((((~((S i) = 0) /\ (exists esip_gap_ext_stored_relation_scaled_left_bound. esip_gap_ext_stored_relation_scaled_left_bound + S (S i) = p))) /\ (((~(z = 0) /\ (exists esip_gap_ext_stored_relation_scaled_right_bound. esip_gap_ext_stored_relation_scaled_right_bound + S (z) = p))) /\ (exists esi_mod_left_ext_stored_relation_scaled_mod esi_mod_right_ext_stored_relation_scaled_mod. ((S i) * z) + p * esi_mod_left_ext_stored_relation_scaled_mod = (a) + p * esi_mod_right_ext_stored_relation_scaled_mod))))))
  13. 0013specialize hprefix i
  14. 0014apply hprefix
  15. 0015exact hi
  16. 0016cases hstored
  17. 0017cases hstored_witness
  18. 0018have heq : y = x
  19. 0019specialize beta_at_unique b
  20. 0020specialize beta_at_unique c
  21. 0021specialize beta_at_unique i
  22. 0022specialize beta_at_unique y
  23. 0023specialize beta_at_unique x
  24. 0024apply beta_at_unique
  25. 0025exact hat
  26. 0026exact hstored_witness_left
  27. 0027rewrite heq
  28. 0028rewrite heq
  29. 0029rewrite heq
  30. 0030exact hstored_witness_right