PA0075

gauss_half_range_signed_prefix_exists

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

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

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-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

28 script commands · 3 reading checkpoints · 1 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (2)
gauss half range signed choicesgauss signed half prefix exists

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–9

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro a
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro hp
  7. L7
    intro hprime
  8. L8
    intro hnotdiv
  9. L9
    intro hrange
02Establish hchoicesL10–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gauss half range signed choices.

  1. L10
    have hchoices : ∀ gsp_choice_index_half_range_choices. Lt(gsp_choice_index_half_range_choices,h) → ∃ x. ∃ y. ∃ z. BetaAt(b,c,gsp_choice_index_half_range_choices,x) ∧ (Lt(0,y) ∧ (Le(y,h) ∧ ((z = 0 ∨ z = 1) ∧ (z = 0 ∧ ModEq(p,a · x,y) ∨ z = 1 ∧ ModEq(p,a · x,2 · h · y)))))Definitions: LeLtModEqBetaAt
  2. L11
    specialize gauss_half_range_signed_choices p
  3. L12
    specialize gauss_half_range_signed_choices h
  4. L13
    specialize gauss_half_range_signed_choices a
  5. L14
    specialize gauss_half_range_signed_choices b
  6. L15
    specialize gauss_half_range_signed_choices c
  7. L16
    apply gauss_half_range_signed_choices
  8. L17
    exact hp
  9. L18
    exact hprime
  10. L19
    exact hnotdiv
03Use earlier factsL20–28

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L20
    exact hrange
  2. L21
    specialize gauss_signed_half_prefix_exists p
  3. L22
    specialize gauss_signed_half_prefix_exists h
  4. L23
    specialize gauss_signed_half_prefix_exists a
  5. L24
    specialize gauss_signed_half_prefix_exists b
  6. L25
    specialize gauss_signed_half_prefix_exists c
  7. L26
    specialize gauss_signed_half_prefix_exists h
  8. L27
    apply gauss_signed_half_prefix_exists
  9. L28
    exact hchoices

Library-wide reading audit

Original exact command ledger · 28 lines
  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