PA007E

gauss_signed_half_predecessor_recode_exists

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

The signed-half magnitude prefix admits a beta code of its 0,...,h-1 predecessors.

Exact expanded PA statement

forall p h a b c mb mc sb sc. (forall gsp_index_injective_signed_source. (exists gsp_lt_gap_injective_signed_source_index_bound. gsp_lt_gap_injective_signed_source_index_bound + S gsp_index_injective_signed_source = h) -> (exists gsp_value_injective_signed_source_entry gsp_magnitude_injective_signed_source_entry gsp_sign_injective_signed_source_entry. (((exists ff_h_gsp_injective_signed_source_entry_source. ff_h_gsp_injective_signed_source_entry_source + S (gsp_value_injective_signed_source_entry) = S ((S (gsp_index_injective_signed_source)) * c)) /\ exists ff_q_gsp_injective_signed_source_entry_source. b = ff_q_gsp_injective_signed_source_entry_source * S ((S (gsp_index_injective_signed_source)) * c) + (gsp_value_injective_signed_source_entry))) /\ ((((exists ff_h_gsp_injective_signed_source_entry_magnitude. ff_h_gsp_injective_signed_source_entry_magnitude + S (gsp_magnitude_injective_signed_source_entry) = S ((S (gsp_index_injective_signed_source)) * mc)) /\ exists ff_q_gsp_injective_signed_source_entry_magnitude. mb = ff_q_gsp_injective_signed_source_entry_magnitude * S ((S (gsp_index_injective_signed_source)) * mc) + (gsp_magnitude_injective_signed_source_entry))) /\ ((((exists ff_h_gsp_injective_signed_source_entry_sign. ff_h_gsp_injective_signed_source_entry_sign + S (gsp_sign_injective_signed_source_entry) = S ((S (gsp_index_injective_signed_source)) * sc)) /\ exists ff_q_gsp_injective_signed_source_entry_sign. sb = ff_q_gsp_injective_signed_source_entry_sign * S ((S (gsp_index_injective_signed_source)) * sc) + (gsp_sign_injective_signed_source_entry))) /\ ((exists gsp_lt_gap_injective_signed_source_entry_positive. gsp_lt_gap_injective_signed_source_entry_positive + S 0 = gsp_magnitude_injective_signed_source_entry) /\ ((exists gsp_le_gap_injective_signed_source_entry_bounded. gsp_le_gap_injective_signed_source_entry_bounded + gsp_magnitude_injective_signed_source_entry = h) /\ ((gsp_sign_injective_signed_source_entry = 0 \/ gsp_sign_injective_signed_source_entry = 1) /\ (((gsp_sign_injective_signed_source_entry = 0 /\ (exists gsp_mod_left_injective_signed_source_entry_lower gsp_mod_right_injective_signed_source_entry_lower. (a * gsp_value_injective_signed_source_entry) + p * gsp_mod_left_injective_signed_source_entry_lower = (gsp_magnitude_injective_signed_source_entry) + p * gsp_mod_right_injective_signed_source_entry_lower)) \/ (gsp_sign_injective_signed_source_entry = 1 /\ (exists gsp_mod_left_injective_signed_source_entry_reflected gsp_mod_right_injective_signed_source_entry_reflected. (a * gsp_value_injective_signed_source_entry) + p * gsp_mod_left_injective_signed_source_entry_reflected = ((2 * h) * gsp_magnitude_injective_signed_source_entry) + p * gsp_mod_right_injective_signed_source_entry_reflected))))))))))) -> (exists rb rc. (forall gmp_index_signed_predecessor_recode_result gmp_predecessor_signed_predecessor_recode_result. (exists gsp_lt_gap_signed_predecessor_recode_result_index_bound. gsp_lt_gap_signed_predecessor_recode_result_index_bound + S gmp_index_signed_predecessor_recode_result = h) -> (((exists gsp_beta_height_gmp_signed_predecessor_recode_result_source. gsp_beta_height_gmp_signed_predecessor_recode_result_source + S (S gmp_predecessor_signed_predecessor_recode_result) = S ((S (gmp_index_signed_predecessor_recode_result)) * mc)) /\ exists gsp_beta_quotient_gmp_signed_predecessor_recode_result_source. mb = gsp_beta_quotient_gmp_signed_predecessor_recode_result_source * S ((S (gmp_index_signed_predecessor_recode_result)) * mc) + (S gmp_predecessor_signed_predecessor_recode_result))) -> (((exists ff_h_gmp_signed_predecessor_recode_result_target. ff_h_gmp_signed_predecessor_recode_result_target + S (gmp_predecessor_signed_predecessor_recode_result) = S ((S (gmp_index_signed_predecessor_recode_result)) * rc)) /\ exists ff_q_gmp_signed_predecessor_recode_result_target. rb = ff_q_gmp_signed_predecessor_recode_result_target * S ((S (gmp_index_signed_predecessor_recode_result)) * rc) + (gmp_predecessor_signed_predecessor_recode_result)))))

Structural proof guide

Generated structural guide

The signed-half magnitude prefix admits a beta code of its 0,...,h-1 predecessors.

Use the direct prerequisites gauss_signed_half_magnitude_range, beta_magnitude_predecessor_recode_exists as previously established PA formulas.

The proof proceeds by intermediate claims (1).

Referenced ingredients

PA0078 gauss_signed_half_magnitude_range PA007D beta_magnitude_predecessor_recode_exists

Proof neighborhood

Direct dependencies

PA0078 gauss_signed_half_magnitude_range PA007D beta_magnitude_predecessor_recode_exists

Direct dependents

PA0085 gauss_lemma_power_congruence_exists PA00D0 gauss_signed_half_magnitude_sum_equals_half_sum

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 h
  3. 0003intro a
  4. 0004intro b
  5. 0005intro c
  6. 0006intro mb
  7. 0007intro mc
  8. 0008intro sb
  9. 0009intro sc
  10. 0010intro hprefix
  11. 0011have hrange : forall gmp_index_signed_predecessor_recode_range. (exists gsp_lt_gap_signed_predecessor_recode_range_index_bound. gsp_lt_gap_signed_predecessor_recode_range_index_bound + S gmp_index_signed_predecessor_recode_range = h) -> exists gmp_magnitude_signed_predecessor_recode_range. ((((exists ff_h_gmp_signed_predecessor_recode_range_decoded. ff_h_gmp_signed_predecessor_recode_range_decoded + S (gmp_magnitude_signed_predecessor_recode_range) = S ((S (gmp_index_signed_predecessor_recode_range)) * mc)) /\ exists ff_q_gmp_signed_predecessor_recode_range_decoded. mb = ff_q_gmp_signed_predecessor_recode_range_decoded * S ((S (gmp_index_signed_predecessor_recode_range)) * mc) + (gmp_magnitude_signed_predecessor_recode_range))) /\ ((exists gsp_lt_gap_signed_predecessor_recode_range_positive. gsp_lt_gap_signed_predecessor_recode_range_positive + S 0 = gmp_magnitude_signed_predecessor_recode_range) /\ (exists gsp_le_gap_signed_predecessor_recode_range_bounded. gsp_le_gap_signed_predecessor_recode_range_bounded + gmp_magnitude_signed_predecessor_recode_range = h)))
  12. 0012specialize gauss_signed_half_magnitude_range p
  13. 0013specialize gauss_signed_half_magnitude_range h
  14. 0014specialize gauss_signed_half_magnitude_range a
  15. 0015specialize gauss_signed_half_magnitude_range b
  16. 0016specialize gauss_signed_half_magnitude_range c
  17. 0017specialize gauss_signed_half_magnitude_range mb
  18. 0018specialize gauss_signed_half_magnitude_range mc
  19. 0019specialize gauss_signed_half_magnitude_range sb
  20. 0020specialize gauss_signed_half_magnitude_range sc
  21. 0021specialize gauss_signed_half_magnitude_range h
  22. 0022apply gauss_signed_half_magnitude_range
  23. 0023exact hprefix
  24. 0024specialize beta_magnitude_predecessor_recode_exists mb
  25. 0025specialize beta_magnitude_predecessor_recode_exists mc
  26. 0026specialize beta_magnitude_predecessor_recode_exists h
  27. 0027specialize beta_magnitude_predecessor_recode_exists h
  28. 0028apply beta_magnitude_predecessor_recode_exists
  29. 0029exact hrange