PA007E · theorem

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.

Statement with defined notation

∀ p. ∀ h. ∀ a. ∀ b. ∀ c. ∀ mb. ∀ mc. ∀ sb. ∀ sc. (∀ x. Lt(x,h) → ∃ y. ∃ z. ∃ n. BetaAt(b,c,x,y) ∧ (BetaAt(mb,mc,x,z) ∧ (BetaAt(sb,sc,x,n) ∧ (Lt(0,z) ∧ (Le(z,h) ∧ ((n = 0 ∨ n = 1) ∧ (n = 0 ∧ ModEq(p,a · y,z) ∨ n = 1 ∧ ModEq(p,a · y,2 · h · z)))))))) → ∃ x. ∃ y. ∀ z. ∀ n. Lt(z,h) → BetaAt(mb,mc,z,S n) → BetaAt(x,y,z,n)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0001 Le PD0002 Lt PD0008 ModEq PD0013 BetaAt

11 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0013 BetaAt

4 occurrences

Exact expanded native-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)))))

Proof neighborhood

Direct theorem prerequisites

PA0078 gauss_signed_half_magnitude_range PA007D beta_magnitude_predecessor_recode_exists

Direct theorem dependents

PA0085 gauss_lemma_power_congruence_exists PA00D0 gauss_signed_half_magnitude_sum_equals_half_sum

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
gauss signed half magnitude rangebeta magnitude predecessor recode exists
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: Lt(gmp_index_signed_predecessor_recode_range,h)BetaAt(mb,mc,gmp_index_signed_predecessor_recode_range,x)Lt(0,x)Le(x,h)Original native command in the exact edition
  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 defined 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 : ∀ 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))
    Exact native replay linehave 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