PA0075

gauss_half_range_signed_prefix_exists

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

The full prime odd half-range has beta-coded positive magnitudes and explicit reflection bits.

Exact expanded PA statement

forall p h a b c. p = 2 * h + 1 -> ((~(p = 1) /\ forall gsp_prime_left_half_range_prime gsp_prime_right_half_range_prime. p = gsp_prime_left_half_range_prime * gsp_prime_right_half_range_prime -> gsp_prime_left_half_range_prime = 1 \/ gsp_prime_right_half_range_prime = 1)) -> (~(exists gsp_divisor_factor_half_range_multiplier. a = p * gsp_divisor_factor_half_range_multiplier)) -> (forall gsp_range_index_half_range_source. (exists gsp_lt_gap_half_range_source_range_bound. gsp_lt_gap_half_range_source_range_bound + S gsp_range_index_half_range_source = h) -> (((exists gsp_beta_height_half_range_source_range_entry. gsp_beta_height_half_range_source_range_entry + S (1 + gsp_range_index_half_range_source) = S ((S (gsp_range_index_half_range_source)) * c)) /\ exists gsp_beta_quotient_half_range_source_range_entry. b = gsp_beta_quotient_half_range_source_range_entry * S ((S (gsp_range_index_half_range_source)) * c) + (1 + gsp_range_index_half_range_source)))) -> (exists mb mc sb sc. (forall gsp_index_full_half_range_result. (exists gsp_lt_gap_full_half_range_result_index_bound. gsp_lt_gap_full_half_range_result_index_bound + S gsp_index_full_half_range_result = h) -> (exists gsp_value_full_half_range_result_entry gsp_magnitude_full_half_range_result_entry gsp_sign_full_half_range_result_entry. (((exists ff_h_gsp_full_half_range_result_entry_source. ff_h_gsp_full_half_range_result_entry_source + S (gsp_value_full_half_range_result_entry) = S ((S (gsp_index_full_half_range_result)) * c)) /\ exists ff_q_gsp_full_half_range_result_entry_source. b = ff_q_gsp_full_half_range_result_entry_source * S ((S (gsp_index_full_half_range_result)) * c) + (gsp_value_full_half_range_result_entry))) /\ ((((exists ff_h_gsp_full_half_range_result_entry_magnitude. ff_h_gsp_full_half_range_result_entry_magnitude + S (gsp_magnitude_full_half_range_result_entry) = S ((S (gsp_index_full_half_range_result)) * mc)) /\ exists ff_q_gsp_full_half_range_result_entry_magnitude. mb = ff_q_gsp_full_half_range_result_entry_magnitude * S ((S (gsp_index_full_half_range_result)) * mc) + (gsp_magnitude_full_half_range_result_entry))) /\ ((((exists ff_h_gsp_full_half_range_result_entry_sign. ff_h_gsp_full_half_range_result_entry_sign + S (gsp_sign_full_half_range_result_entry) = S ((S (gsp_index_full_half_range_result)) * sc)) /\ exists ff_q_gsp_full_half_range_result_entry_sign. sb = ff_q_gsp_full_half_range_result_entry_sign * S ((S (gsp_index_full_half_range_result)) * sc) + (gsp_sign_full_half_range_result_entry))) /\ ((exists gsp_lt_gap_full_half_range_result_entry_positive. gsp_lt_gap_full_half_range_result_entry_positive + S 0 = gsp_magnitude_full_half_range_result_entry) /\ ((exists gsp_le_gap_full_half_range_result_entry_bounded. gsp_le_gap_full_half_range_result_entry_bounded + gsp_magnitude_full_half_range_result_entry = h) /\ ((gsp_sign_full_half_range_result_entry = 0 \/ gsp_sign_full_half_range_result_entry = 1) /\ (((gsp_sign_full_half_range_result_entry = 0 /\ (exists gsp_mod_left_full_half_range_result_entry_lower gsp_mod_right_full_half_range_result_entry_lower. (a * gsp_value_full_half_range_result_entry) + p * gsp_mod_left_full_half_range_result_entry_lower = (gsp_magnitude_full_half_range_result_entry) + p * gsp_mod_right_full_half_range_result_entry_lower)) \/ (gsp_sign_full_half_range_result_entry = 1 /\ (exists gsp_mod_left_full_half_range_result_entry_reflected gsp_mod_right_full_half_range_result_entry_reflected. (a * gsp_value_full_half_range_result_entry) + p * gsp_mod_left_full_half_range_result_entry_reflected = ((2 * h) * gsp_magnitude_full_half_range_result_entry) + p * gsp_mod_right_full_half_range_result_entry_reflected))))))))))))

Structural proof guide

Generated structural guide

The full prime odd half-range has beta-coded positive magnitudes and explicit reflection bits.

Use the direct prerequisites gauss_half_range_signed_choices, gauss_signed_half_prefix_exists as previously established PA formulas.

The proof proceeds by intermediate claims (1).

Referenced ingredients

PA0072 gauss_half_range_signed_choices PA0074 gauss_signed_half_prefix_exists

Proof neighborhood

Direct dependencies

PA0072 gauss_half_range_signed_choices PA0074 gauss_signed_half_prefix_exists

Direct dependents

PA0085 gauss_lemma_power_congruence_exists

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 hp
  7. 0007intro hprime
  8. 0008intro hnotdiv
  9. 0009intro hrange
  10. 0010have hchoices : forall gsp_choice_index_half_range_choices. (exists gsp_lt_gap_half_range_choices_choice_bound. gsp_lt_gap_half_range_choices_choice_bound + S gsp_choice_index_half_range_choices = h) -> (exists gsp_value_half_range_choices_choice gsp_magnitude_half_range_choices_choice gsp_sign_half_range_choices_choice. (((exists ff_h_gsp_half_range_choices_choice_source. ff_h_gsp_half_range_choices_choice_source + S (gsp_value_half_range_choices_choice) = S ((S (gsp_choice_index_half_range_choices)) * c)) /\ exists ff_q_gsp_half_range_choices_choice_source. b = ff_q_gsp_half_range_choices_choice_source * S ((S (gsp_choice_index_half_range_choices)) * c) + (gsp_value_half_range_choices_choice))) /\ ((exists gsp_lt_gap_half_range_choices_choice_positive. gsp_lt_gap_half_range_choices_choice_positive + S 0 = gsp_magnitude_half_range_choices_choice) /\ ((exists gsp_le_gap_half_range_choices_choice_bounded. gsp_le_gap_half_range_choices_choice_bounded + gsp_magnitude_half_range_choices_choice = h) /\ ((gsp_sign_half_range_choices_choice = 0 \/ gsp_sign_half_range_choices_choice = 1) /\ (((gsp_sign_half_range_choices_choice = 0 /\ (exists gsp_mod_left_half_range_choices_choice_lower gsp_mod_right_half_range_choices_choice_lower. (a * gsp_value_half_range_choices_choice) + p * gsp_mod_left_half_range_choices_choice_lower = (gsp_magnitude_half_range_choices_choice) + p * gsp_mod_right_half_range_choices_choice_lower)) \/ (gsp_sign_half_range_choices_choice = 1 /\ (exists gsp_mod_left_half_range_choices_choice_reflected gsp_mod_right_half_range_choices_choice_reflected. (a * gsp_value_half_range_choices_choice) + p * gsp_mod_left_half_range_choices_choice_reflected = ((2 * h) * gsp_magnitude_half_range_choices_choice) + p * gsp_mod_right_half_range_choices_choice_reflected))))))))
  11. 0011specialize gauss_half_range_signed_choices p
  12. 0012specialize gauss_half_range_signed_choices h
  13. 0013specialize gauss_half_range_signed_choices a
  14. 0014specialize gauss_half_range_signed_choices b
  15. 0015specialize gauss_half_range_signed_choices c
  16. 0016apply gauss_half_range_signed_choices
  17. 0017exact hp
  18. 0018exact hprime
  19. 0019exact hnotdiv
  20. 0020exact hrange
  21. 0021specialize gauss_signed_half_prefix_exists p
  22. 0022specialize gauss_signed_half_prefix_exists h
  23. 0023specialize gauss_signed_half_prefix_exists a
  24. 0024specialize gauss_signed_half_prefix_exists b
  25. 0025specialize gauss_signed_half_prefix_exists c
  26. 0026specialize gauss_signed_half_prefix_exists h
  27. 0027apply gauss_signed_half_prefix_exists
  28. 0028exact hchoices