PA0078 · theorem

gauss_signed_half_magnitude_range

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

Every decoded signed-prefix magnitude lies constructively in 1,...,h.

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. ∀ l. (∀ x. Lt(x,l) → ∃ 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. Lt(x,l) → ∃ y. BetaAt(mb,mc,x,y) ∧ (Lt(0,y) ∧ Le(y,h))

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

12 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0008 ModEq PD0013 BetaAt

7 occurrences

Exact expanded native-PA statement
forall p h a b c mb mc sb sc l. (forall gsp_index_magnitude_range_source. (exists gsp_lt_gap_magnitude_range_source_index_bound. gsp_lt_gap_magnitude_range_source_index_bound + S gsp_index_magnitude_range_source = l) -> (exists gsp_value_magnitude_range_source_entry gsp_magnitude_magnitude_range_source_entry gsp_sign_magnitude_range_source_entry. (((exists ff_h_gsp_magnitude_range_source_entry_source. ff_h_gsp_magnitude_range_source_entry_source + S (gsp_value_magnitude_range_source_entry) = S ((S (gsp_index_magnitude_range_source)) * c)) /\ exists ff_q_gsp_magnitude_range_source_entry_source. b = ff_q_gsp_magnitude_range_source_entry_source * S ((S (gsp_index_magnitude_range_source)) * c) + (gsp_value_magnitude_range_source_entry))) /\ ((((exists ff_h_gsp_magnitude_range_source_entry_magnitude. ff_h_gsp_magnitude_range_source_entry_magnitude + S (gsp_magnitude_magnitude_range_source_entry) = S ((S (gsp_index_magnitude_range_source)) * mc)) /\ exists ff_q_gsp_magnitude_range_source_entry_magnitude. mb = ff_q_gsp_magnitude_range_source_entry_magnitude * S ((S (gsp_index_magnitude_range_source)) * mc) + (gsp_magnitude_magnitude_range_source_entry))) /\ ((((exists ff_h_gsp_magnitude_range_source_entry_sign. ff_h_gsp_magnitude_range_source_entry_sign + S (gsp_sign_magnitude_range_source_entry) = S ((S (gsp_index_magnitude_range_source)) * sc)) /\ exists ff_q_gsp_magnitude_range_source_entry_sign. sb = ff_q_gsp_magnitude_range_source_entry_sign * S ((S (gsp_index_magnitude_range_source)) * sc) + (gsp_sign_magnitude_range_source_entry))) /\ ((exists gsp_lt_gap_magnitude_range_source_entry_positive. gsp_lt_gap_magnitude_range_source_entry_positive + S 0 = gsp_magnitude_magnitude_range_source_entry) /\ ((exists gsp_le_gap_magnitude_range_source_entry_bounded. gsp_le_gap_magnitude_range_source_entry_bounded + gsp_magnitude_magnitude_range_source_entry = h) /\ ((gsp_sign_magnitude_range_source_entry = 0 \/ gsp_sign_magnitude_range_source_entry = 1) /\ (((gsp_sign_magnitude_range_source_entry = 0 /\ (exists gsp_mod_left_magnitude_range_source_entry_lower gsp_mod_right_magnitude_range_source_entry_lower. (a * gsp_value_magnitude_range_source_entry) + p * gsp_mod_left_magnitude_range_source_entry_lower = (gsp_magnitude_magnitude_range_source_entry) + p * gsp_mod_right_magnitude_range_source_entry_lower)) \/ (gsp_sign_magnitude_range_source_entry = 1 /\ (exists gsp_mod_left_magnitude_range_source_entry_reflected gsp_mod_right_magnitude_range_source_entry_reflected. (a * gsp_value_magnitude_range_source_entry) + p * gsp_mod_left_magnitude_range_source_entry_reflected = ((2 * h) * gsp_magnitude_magnitude_range_source_entry) + p * gsp_mod_right_magnitude_range_source_entry_reflected))))))))))) -> (forall gmp_index_magnitude_range_result. (exists gsp_lt_gap_magnitude_range_result_index_bound. gsp_lt_gap_magnitude_range_result_index_bound + S gmp_index_magnitude_range_result = l) -> exists gmp_magnitude_magnitude_range_result. ((((exists ff_h_gmp_magnitude_range_result_decoded. ff_h_gmp_magnitude_range_result_decoded + S (gmp_magnitude_magnitude_range_result) = S ((S (gmp_index_magnitude_range_result)) * mc)) /\ exists ff_q_gmp_magnitude_range_result_decoded. mb = ff_q_gmp_magnitude_range_result_decoded * S ((S (gmp_index_magnitude_range_result)) * mc) + (gmp_magnitude_magnitude_range_result))) /\ ((exists gsp_lt_gap_magnitude_range_result_positive. gsp_lt_gap_magnitude_range_result_positive + S 0 = gmp_magnitude_magnitude_range_result) /\ (exists gsp_le_gap_magnitude_range_result_bounded. gsp_le_gap_magnitude_range_result_bounded + gmp_magnitude_magnitude_range_result = h))))

Proof neighborhood

Direct theorem prerequisites

none

Direct theorem dependents

PA007E gauss_signed_half_predecessor_recode_exists 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

31 script commands · 9 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.

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 l
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hprefix
  2. L12
    intro i
  3. L13
    intro hi
03Establish hentryL14–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hprefix.

  1. L14
    have hentry · expand full local formula (694 characters)have hentry : ∃ gsp_value_magnitude_range_entry. ∃ gsp_magnitude_magnitude_range_entry. ∃ gsp_sign_magnitude_range_entry. BetaAt(b,c,i,gsp_value_magnitude_range_entry) ∧ (BetaAt(mb,mc,i,gsp_magnitude_magnitude_range_entry) ∧ (BetaAt(sb,sc,i,gsp_sign_magnitude_range_entry) ∧ (Lt(0,gsp_magnitude_magnitude_range_entry) ∧ (Le(gsp_magnitude_magnitude_range_entry,h) ∧ ((gsp_sign_magnitude_range_entry = 0 ∨ gsp_sign_magnitude_range_entry = 1) ∧ (gsp_sign_magnitude_range_entry = 0 ∧ ModEq(p,a · gsp_value_magnitude_range_entry,gsp_magnitude_magnitude_range_entry) ∨ gsp_sign_magnitude_range_entry = 1 ∧ ModEq(p,a · gsp_value_magnitude_range_entry,2 · h · gsp_magnitude_magnitude_range_entry)))))))
    Definitions: BetaAt(b,c,i,gsp_value_magnitude_range_entry)BetaAt(mb,mc,i,gsp_magnitude_magnitude_range_entry)BetaAt(sb,sc,i,gsp_sign_magnitude_range_entry)Lt(0,gsp_magnitude_magnitude_range_entry)Le(gsp_magnitude_magnitude_range_entry,h)ModEq(p,a · gsp_value_magnitude_range_entry,gsp_magnitude_magnitude_range_entry)ModEq(p,a · gsp_value_magnitude_range_entry,2 · h · gsp_magnitude_magnitude_range_entry)Original native command in the exact edition
  2. L15
    specialize hprefix i
  3. L16
    apply hprefix
  4. L17
    exact hi
04Separate the logical casesL18–25

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L18
    cases hentry
  2. L19
    cases hentry_witness
  3. L20
    cases hentry_witness_witness
  4. L21
    cases hentry_witness_witness_witness
  5. L22
    cases hentry_witness_witness_witness_right
  6. L23
    cases hentry_witness_witness_witness_right_right
  7. L24
    cases hentry_witness_witness_witness_right_right_right
  8. L25
    cases hentry_witness_witness_witness_right_right_right_right
05Construct an explicit witnessL26–26

Supply the displayed value, then prove that it has the required property.

  1. L26
    exists x1
06Separate the logical casesL27–27

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L27
    split
07Use earlier factsL28–28

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

  1. L28
    exact hentry_witness_witness_witness_right_left
08Separate the logical casesL29–29

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L29
    split
09Use earlier factsL30–31

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

  1. L30
    exact hentry_witness_witness_witness_right_right_right_left
  2. L31
    exact hentry_witness_witness_witness_right_right_right_right_left

Library-wide reading audit

Original defined command ledger · 31 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 l
  11. 0011intro hprefix
  12. 0012intro i
  13. 0013intro hi
  14. 0014have hentry : ∃ gsp_value_magnitude_range_entry. ∃ gsp_magnitude_magnitude_range_entry. ∃ gsp_sign_magnitude_range_entry. BetaAt(b,c,i,gsp_value_magnitude_range_entry) ∧ (BetaAt(mb,mc,i,gsp_magnitude_magnitude_range_entry) ∧ (BetaAt(sb,sc,i,gsp_sign_magnitude_range_entry) ∧ (Lt(0,gsp_magnitude_magnitude_range_entry) ∧ (Le(gsp_magnitude_magnitude_range_entry,h) ∧ ((gsp_sign_magnitude_range_entry = 0 ∨ gsp_sign_magnitude_range_entry = 1) ∧ (gsp_sign_magnitude_range_entry = 0 ∧ ModEq(p,a · gsp_value_magnitude_range_entry,gsp_magnitude_magnitude_range_entry) ∨ gsp_sign_magnitude_range_entry = 1 ∧ ModEq(p,a · gsp_value_magnitude_range_entry,2 · h · gsp_magnitude_magnitude_range_entry)))))))
    Exact native replay linehave hentry : exists gsp_value_magnitude_range_entry gsp_magnitude_magnitude_range_entry gsp_sign_magnitude_range_entry. (((exists ff_h_gsp_magnitude_range_entry_source. ff_h_gsp_magnitude_range_entry_source + S (gsp_value_magnitude_range_entry) = S ((S (i)) * c)) /\ exists ff_q_gsp_magnitude_range_entry_source. b = ff_q_gsp_magnitude_range_entry_source * S ((S (i)) * c) + (gsp_value_magnitude_range_entry))) /\ ((((exists ff_h_gsp_magnitude_range_entry_magnitude. ff_h_gsp_magnitude_range_entry_magnitude + S (gsp_magnitude_magnitude_range_entry) = S ((S (i)) * mc)) /\ exists ff_q_gsp_magnitude_range_entry_magnitude. mb = ff_q_gsp_magnitude_range_entry_magnitude * S ((S (i)) * mc) + (gsp_magnitude_magnitude_range_entry))) /\ ((((exists ff_h_gsp_magnitude_range_entry_sign. ff_h_gsp_magnitude_range_entry_sign + S (gsp_sign_magnitude_range_entry) = S ((S (i)) * sc)) /\ exists ff_q_gsp_magnitude_range_entry_sign. sb = ff_q_gsp_magnitude_range_entry_sign * S ((S (i)) * sc) + (gsp_sign_magnitude_range_entry))) /\ ((exists gsp_lt_gap_magnitude_range_entry_positive. gsp_lt_gap_magnitude_range_entry_positive + S 0 = gsp_magnitude_magnitude_range_entry) /\ ((exists gsp_le_gap_magnitude_range_entry_bounded. gsp_le_gap_magnitude_range_entry_bounded + gsp_magnitude_magnitude_range_entry = h) /\ ((gsp_sign_magnitude_range_entry = 0 \/ gsp_sign_magnitude_range_entry = 1) /\ (((gsp_sign_magnitude_range_entry = 0 /\ (exists gsp_mod_left_magnitude_range_entry_lower gsp_mod_right_magnitude_range_entry_lower. (a * gsp_value_magnitude_range_entry) + p * gsp_mod_left_magnitude_range_entry_lower = (gsp_magnitude_magnitude_range_entry) + p * gsp_mod_right_magnitude_range_entry_lower)) \/ (gsp_sign_magnitude_range_entry = 1 /\ (exists gsp_mod_left_magnitude_range_entry_reflected gsp_mod_right_magnitude_range_entry_reflected. (a * gsp_value_magnitude_range_entry) + p * gsp_mod_left_magnitude_range_entry_reflected = ((2 * h) * gsp_magnitude_magnitude_range_entry) + p * gsp_mod_right_magnitude_range_entry_reflected)))))))))
  15. 0015specialize hprefix i
  16. 0016apply hprefix
  17. 0017exact hi
  18. 0018cases hentry
  19. 0019cases hentry_witness
  20. 0020cases hentry_witness_witness
  21. 0021cases hentry_witness_witness_witness
  22. 0022cases hentry_witness_witness_witness_right
  23. 0023cases hentry_witness_witness_witness_right_right
  24. 0024cases hentry_witness_witness_witness_right_right_right
  25. 0025cases hentry_witness_witness_witness_right_right_right_right
  26. 0026exists x1
  27. 0027split
  28. 0028exact hentry_witness_witness_witness_right_left
  29. 0029split
  30. 0030exact hentry_witness_witness_witness_right_right_right_left
  31. 0031exact hentry_witness_witness_witness_right_right_right_right_left