PA00AF

inverse_prefix_entry_sound

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

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

Exact expanded PA statement

forall p n b c l i j. (forall wip_index_entry_prefix. (exists wip_gap_entry_prefix_prefix_bound. wip_gap_entry_prefix_prefix_bound + S wip_index_entry_prefix = l) -> exists wip_mate_entry_prefix. ((((exists wip_beta_height_entry_prefix_decoded. wip_beta_height_entry_prefix_decoded + S (wip_mate_entry_prefix) = S ((S (wip_index_entry_prefix)) * c)) /\ exists wip_beta_quotient_entry_prefix_decoded. b = wip_beta_quotient_entry_prefix_decoded * S ((S (wip_index_entry_prefix)) * c) + (wip_mate_entry_prefix))) /\ ((exists wip_gap_entry_prefix_inverse_index_bound. wip_gap_entry_prefix_inverse_index_bound + S wip_index_entry_prefix = n) /\ ((exists wip_gap_entry_prefix_inverse_mate_bound. wip_gap_entry_prefix_inverse_mate_bound + S wip_mate_entry_prefix = n) /\ (exists wip_mod_left_entry_prefix_inverse_mod wip_mod_right_entry_prefix_inverse_mod. ((S wip_index_entry_prefix) * S wip_mate_entry_prefix) + p * wip_mod_left_entry_prefix_inverse_mod = 1 + p * wip_mod_right_entry_prefix_inverse_mod))))) -> (exists wip_gap_entry_index_bound. wip_gap_entry_index_bound + S i = l) -> (((exists wip_beta_height_entry_source. wip_beta_height_entry_source + S (j) = S ((S (i)) * c)) /\ exists wip_beta_quotient_entry_source. b = wip_beta_quotient_entry_source * S ((S (i)) * c) + (j))) -> ((exists wip_gap_entry_result_index_bound. wip_gap_entry_result_index_bound + S i = n) /\ ((exists wip_gap_entry_result_mate_bound. wip_gap_entry_result_mate_bound + S j = n) /\ (exists wip_mod_left_entry_result_mod wip_mod_right_entry_result_mod. ((S i) * S j) + p * wip_mod_left_entry_result_mod = 1 + p * wip_mod_right_entry_result_mod)))

Structural proof guide

Generated structural guide

Every decoded inverse-prefix entry satisfies its stored inverse 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 (2).

Referenced ingredients

PA002F beta_at_unique

Proof neighborhood

Direct dependencies

PA002F beta_at_unique

Direct dependents

PA00AH prime_inverse_prefix_fixed_cases PA00AN inverse_prefix_involutive

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 n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro i
  7. 0007intro j
  8. 0008intro hprefix
  9. 0009intro hi
  10. 0010intro hat
  11. 0011have hstored : exists k. ((((exists wip_beta_height_entry_stored_at. wip_beta_height_entry_stored_at + S (k) = S ((S (i)) * c)) /\ exists wip_beta_quotient_entry_stored_at. b = wip_beta_quotient_entry_stored_at * S ((S (i)) * c) + (k))) /\ ((exists wip_gap_entry_stored_inverse_index_bound. wip_gap_entry_stored_inverse_index_bound + S i = n) /\ ((exists wip_gap_entry_stored_inverse_mate_bound. wip_gap_entry_stored_inverse_mate_bound + S k = n) /\ (exists wip_mod_left_entry_stored_inverse_mod wip_mod_right_entry_stored_inverse_mod. ((S i) * S k) + p * wip_mod_left_entry_stored_inverse_mod = 1 + p * wip_mod_right_entry_stored_inverse_mod))))
  12. 0012specialize hprefix i
  13. 0013apply hprefix
  14. 0014exact hi
  15. 0015cases hstored
  16. 0016cases hstored_witness
  17. 0017have heq : j = x
  18. 0018specialize beta_at_unique b
  19. 0019specialize beta_at_unique c
  20. 0020specialize beta_at_unique i
  21. 0021specialize beta_at_unique j
  22. 0022specialize beta_at_unique x
  23. 0023apply beta_at_unique
  24. 0024exact hat
  25. 0025exact hstored_witness_left
  26. 0026rewrite heq
  27. 0027rewrite heq
  28. 0028exact hstored_witness_right