PA007E

gauss_signed_half_predecessor_recode_exists

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

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

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

Read the argument

Proof checkpoints

29 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 signed half magnitude rangebeta magnitude predecessor recode 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–10

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 mb
  7. L7
    intro mc
  8. L8
    intro sb
  9. L9
    intro sc
  10. L10
    intro hprefix
02Establish hrangeL11–20

Establish this local claim before using it. It is not an additional assumption.

  1. L11
    have hrange : ∀ gmp_index_signed_predecessor_recode_range. Lt(gmp_index_signed_predecessor_recode_range,h) → ∃ x. BetaAt(mb,mc,gmp_index_signed_predecessor_recode_range,x) ∧ (Lt(0,x) ∧ Le(x,h))Definitions: LeLtBetaAt
  2. L12
    specialize gauss_signed_half_magnitude_range p
  3. L13
    specialize gauss_signed_half_magnitude_range h
  4. L14
    specialize gauss_signed_half_magnitude_range a
  5. L15
    specialize gauss_signed_half_magnitude_range b
  6. L16
    specialize gauss_signed_half_magnitude_range c
  7. L17
    specialize gauss_signed_half_magnitude_range mb
  8. L18
    specialize gauss_signed_half_magnitude_range mc
  9. L19
    specialize gauss_signed_half_magnitude_range sb
  10. L20
    specialize gauss_signed_half_magnitude_range sc
03Use earlier factsL21–29

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

  1. L21
    specialize gauss_signed_half_magnitude_range h
  2. L22
    apply gauss_signed_half_magnitude_range
  3. L23
    exact hprefix
  4. L24
    specialize beta_magnitude_predecessor_recode_exists mb
  5. L25
    specialize beta_magnitude_predecessor_recode_exists mc
  6. L26
    specialize beta_magnitude_predecessor_recode_exists h
  7. L27
    specialize beta_magnitude_predecessor_recode_exists h
  8. L28
    apply beta_magnitude_predecessor_recode_exists
  9. L29
    exact hrange

Library-wide reading audit

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