PA0076

gauss_signed_half_prefix_all_bits

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

The sign projection of every encoded signed-half prefix is an AllBits prefix.

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 l. (forall gsp_index_bits_source. (exists gsp_lt_gap_bits_source_index_bound. gsp_lt_gap_bits_source_index_bound + S gsp_index_bits_source = l) -> (exists gsp_value_bits_source_entry gsp_magnitude_bits_source_entry gsp_sign_bits_source_entry. (((exists ff_h_gsp_bits_source_entry_source. ff_h_gsp_bits_source_entry_source + S (gsp_value_bits_source_entry) = S ((S (gsp_index_bits_source)) * c)) /\ exists ff_q_gsp_bits_source_entry_source. b = ff_q_gsp_bits_source_entry_source * S ((S (gsp_index_bits_source)) * c) + (gsp_value_bits_source_entry))) /\ ((((exists ff_h_gsp_bits_source_entry_magnitude. ff_h_gsp_bits_source_entry_magnitude + S (gsp_magnitude_bits_source_entry) = S ((S (gsp_index_bits_source)) * mc)) /\ exists ff_q_gsp_bits_source_entry_magnitude. mb = ff_q_gsp_bits_source_entry_magnitude * S ((S (gsp_index_bits_source)) * mc) + (gsp_magnitude_bits_source_entry))) /\ ((((exists ff_h_gsp_bits_source_entry_sign. ff_h_gsp_bits_source_entry_sign + S (gsp_sign_bits_source_entry) = S ((S (gsp_index_bits_source)) * sc)) /\ exists ff_q_gsp_bits_source_entry_sign. sb = ff_q_gsp_bits_source_entry_sign * S ((S (gsp_index_bits_source)) * sc) + (gsp_sign_bits_source_entry))) /\ ((exists gsp_lt_gap_bits_source_entry_positive. gsp_lt_gap_bits_source_entry_positive + S 0 = gsp_magnitude_bits_source_entry) /\ ((exists gsp_le_gap_bits_source_entry_bounded. gsp_le_gap_bits_source_entry_bounded + gsp_magnitude_bits_source_entry = h) /\ ((gsp_sign_bits_source_entry = 0 \/ gsp_sign_bits_source_entry = 1) /\ (((gsp_sign_bits_source_entry = 0 /\ (exists gsp_mod_left_bits_source_entry_lower gsp_mod_right_bits_source_entry_lower. (a * gsp_value_bits_source_entry) + p * gsp_mod_left_bits_source_entry_lower = (gsp_magnitude_bits_source_entry) + p * gsp_mod_right_bits_source_entry_lower)) \/ (gsp_sign_bits_source_entry = 1 /\ (exists gsp_mod_left_bits_source_entry_reflected gsp_mod_right_bits_source_entry_reflected. (a * gsp_value_bits_source_entry) + p * gsp_mod_left_bits_source_entry_reflected = ((2 * h) * gsp_magnitude_bits_source_entry) + p * gsp_mod_right_bits_source_entry_reflected))))))))))) -> (forall ff_i_gsp_signs. (exists ff_lt_gsp_signs_bound. ff_lt_gsp_signs_bound + S ff_i_gsp_signs = l) -> exists ff_bit_gsp_signs. ((((exists ff_h_gsp_signs_decoded. ff_h_gsp_signs_decoded + S (ff_bit_gsp_signs) = S ((S (ff_i_gsp_signs)) * sc)) /\ exists ff_q_gsp_signs_decoded. sb = ff_q_gsp_signs_decoded * S ((S (ff_i_gsp_signs)) * sc) + (ff_bit_gsp_signs))) /\ (ff_bit_gsp_signs = 0 \/ ff_bit_gsp_signs = 1)))

Structural proof guide

Generated structural guide

The sign projection of every encoded signed-half prefix is an AllBits prefix.

This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.

The proof proceeds by case analysis (9), intermediate claims (1).

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA0077 gauss_signed_half_bit_count_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

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

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 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 : ∃ gsp_value_bits_entry. ∃ gsp_magnitude_bits_entry. ∃ gsp_sign_bits_entry. BetaAt(b,c,i,gsp_value_bits_entry) ∧ (BetaAt(mb,mc,i,gsp_magnitude_bits_entry) ∧ (BetaAt(sb,sc,i,gsp_sign_bits_entry) ∧ (Lt(0,gsp_magnitude_bits_entry) ∧ (Le(gsp_magnitude_bits_entry,h) ∧ ((gsp_sign_bits_entry = 0 ∨ gsp_sign_bits_entry = 1) ∧ (gsp_sign_bits_entry = 0 ∧ ModEq(p,a · gsp_value_bits_entry,gsp_magnitude_bits_entry) ∨ gsp_sign_bits_entry = 1 ∧ ModEq(p,a · gsp_value_bits_entry,2 · h · gsp_magnitude_bits_entry)))))))Definitions: LeLtModEqBetaAt
  2. L15
    specialize hprefix i
  3. L16
    apply hprefix
  4. L17
    exact hi
04Separate the logical casesL18–26

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
  9. L26
    cases hentry_witness_witness_witness_right_right_right_right_right
05Construct an explicit witnessL27–27

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

  1. L27
    exists x2
06Separate the logical casesL28–28

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

  1. L28
    split
07Use earlier factsL29–30

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

  1. L29
    exact hentry_witness_witness_witness_right_right_left
  2. L30
    exact hentry_witness_witness_witness_right_right_right_right_right_left

Library-wide reading audit

Original exact command ledger · 30 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 : exists gsp_value_bits_entry gsp_magnitude_bits_entry gsp_sign_bits_entry. (((exists ff_h_gsp_bits_entry_source. ff_h_gsp_bits_entry_source + S (gsp_value_bits_entry) = S ((S (i)) * c)) /\ exists ff_q_gsp_bits_entry_source. b = ff_q_gsp_bits_entry_source * S ((S (i)) * c) + (gsp_value_bits_entry))) /\ ((((exists ff_h_gsp_bits_entry_magnitude. ff_h_gsp_bits_entry_magnitude + S (gsp_magnitude_bits_entry) = S ((S (i)) * mc)) /\ exists ff_q_gsp_bits_entry_magnitude. mb = ff_q_gsp_bits_entry_magnitude * S ((S (i)) * mc) + (gsp_magnitude_bits_entry))) /\ ((((exists ff_h_gsp_bits_entry_sign. ff_h_gsp_bits_entry_sign + S (gsp_sign_bits_entry) = S ((S (i)) * sc)) /\ exists ff_q_gsp_bits_entry_sign. sb = ff_q_gsp_bits_entry_sign * S ((S (i)) * sc) + (gsp_sign_bits_entry))) /\ ((exists gsp_lt_gap_bits_entry_positive. gsp_lt_gap_bits_entry_positive + S 0 = gsp_magnitude_bits_entry) /\ ((exists gsp_le_gap_bits_entry_bounded. gsp_le_gap_bits_entry_bounded + gsp_magnitude_bits_entry = h) /\ ((gsp_sign_bits_entry = 0 \/ gsp_sign_bits_entry = 1) /\ (((gsp_sign_bits_entry = 0 /\ (exists gsp_mod_left_bits_entry_lower gsp_mod_right_bits_entry_lower. (a * gsp_value_bits_entry) + p * gsp_mod_left_bits_entry_lower = (gsp_magnitude_bits_entry) + p * gsp_mod_right_bits_entry_lower)) \/ (gsp_sign_bits_entry = 1 /\ (exists gsp_mod_left_bits_entry_reflected gsp_mod_right_bits_entry_reflected. (a * gsp_value_bits_entry) + p * gsp_mod_left_bits_entry_reflected = ((2 * h) * gsp_magnitude_bits_entry) + p * gsp_mod_right_bits_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. 0026cases hentry_witness_witness_witness_right_right_right_right_right
  27. 0027exists x2
  28. 0028split
  29. 0029exact hentry_witness_witness_witness_right_right_left
  30. 0030exact hentry_witness_witness_witness_right_right_right_right_right_left