PA00AO

inverse_prefix_zero_fixed

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

The zero index, representing residue one, is fixed by the full inverse prefix.

Exact expanded PA statement

forall p n k b c. p = S n -> n = S k -> (forall wip_index_zero_prefix. (exists wip_gap_zero_prefix_prefix_bound. wip_gap_zero_prefix_prefix_bound + S wip_index_zero_prefix = n) -> exists wip_mate_zero_prefix. ((((exists wip_beta_height_zero_prefix_decoded. wip_beta_height_zero_prefix_decoded + S (wip_mate_zero_prefix) = S ((S (wip_index_zero_prefix)) * c)) /\ exists wip_beta_quotient_zero_prefix_decoded. b = wip_beta_quotient_zero_prefix_decoded * S ((S (wip_index_zero_prefix)) * c) + (wip_mate_zero_prefix))) /\ ((exists wip_gap_zero_prefix_inverse_index_bound. wip_gap_zero_prefix_inverse_index_bound + S wip_index_zero_prefix = n) /\ ((exists wip_gap_zero_prefix_inverse_mate_bound. wip_gap_zero_prefix_inverse_mate_bound + S wip_mate_zero_prefix = n) /\ (exists wip_mod_left_zero_prefix_inverse_mod wip_mod_right_zero_prefix_inverse_mod. ((S wip_index_zero_prefix) * S wip_mate_zero_prefix) + p * wip_mod_left_zero_prefix_inverse_mod = 1 + p * wip_mod_right_zero_prefix_inverse_mod))))) -> (((exists wie_beta_height_zero_result. wie_beta_height_zero_result + S (0) = S ((S (0)) * c)) /\ exists wie_beta_quotient_zero_result. b = wie_beta_quotient_zero_result * S ((S (0)) * c) + (0)))

Structural proof guide

Generated structural guide

The zero index, representing residue one, is fixed by the full inverse prefix.

Use the direct prerequisites mod_eq_refl, one_mul, inverse_prefix_extensional as previously established PA formulas.

The proof proceeds by intermediate claims (4), equality transport (4).

Referenced ingredients

PA0023 mod_eq_refl PA000M one_mul PA00AM inverse_prefix_extensional

Proof neighborhood

Direct dependencies

PA0023 mod_eq_refl PA000M one_mul PA00AM inverse_prefix_extensional

Direct dependents

PA00AQ prime_inverse_prefix_nonendpoint_mate

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 k
  4. 0004intro b
  5. 0005intro c
  6. 0006intro hpn
  7. 0007intro hnk
  8. 0008intro hprefix
  9. 0009have hzero_bound : exists wie_strict_gap_zero_bound. wie_strict_gap_zero_bound + S 0 = n
  10. 0010rewrite hnk
  11. 0011exists k
  12. 0012rewrite PA4
  13. 0013rewrite PA3
  14. 0014refl
  15. 0015have hzero_refl : exists wie_mod_left_zero_refl wie_mod_right_zero_refl. (1) + p * wie_mod_left_zero_refl = (1) + p * wie_mod_right_zero_refl
  16. 0016specialize mod_eq_refl p
  17. 0017specialize mod_eq_refl 1
  18. 0018exact mod_eq_refl
  19. 0019have hzero_mod : exists wie_mod_left_zero wie_mod_right_zero. ((S 0) * S 0) + p * wie_mod_left_zero = (1) + p * wie_mod_right_zero
  20. 0020specialize one_mul 1
  21. 0021rewrite one_mul
  22. 0022exact hzero_refl
  23. 0023have hzero_relation : (exists wie_strict_gap_zero_relation_index_bound. wie_strict_gap_zero_relation_index_bound + S 0 = n) /\ ((exists wie_strict_gap_zero_relation_mate_bound. wie_strict_gap_zero_relation_mate_bound + S 0 = n) /\ (exists wie_mod_left_zero_relation_mod wie_mod_right_zero_relation_mod. ((S 0) * S 0) + p * wie_mod_left_zero_relation_mod = (1) + p * wie_mod_right_zero_relation_mod))
  24. 0024split
  25. 0025exact hzero_bound
  26. 0026split
  27. 0027exact hzero_bound
  28. 0028exact hzero_mod
  29. 0029specialize inverse_prefix_extensional p
  30. 0030specialize inverse_prefix_extensional n
  31. 0031specialize inverse_prefix_extensional b
  32. 0032specialize inverse_prefix_extensional c
  33. 0033specialize inverse_prefix_extensional n
  34. 0034specialize inverse_prefix_extensional 0
  35. 0035specialize inverse_prefix_extensional 0
  36. 0036apply inverse_prefix_extensional
  37. 0037exact hpn
  38. 0038exact hprefix
  39. 0039exact hzero_bound
  40. 0040exact hzero_relation