PA0077

gauss_signed_half_bit_count_exists

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

The encoded reflection bits have a native relational count of their ones.

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_count_source. (exists gsp_lt_gap_count_source_index_bound. gsp_lt_gap_count_source_index_bound + S gsp_index_count_source = l) -> (exists gsp_value_count_source_entry gsp_magnitude_count_source_entry gsp_sign_count_source_entry. (((exists ff_h_gsp_count_source_entry_source. ff_h_gsp_count_source_entry_source + S (gsp_value_count_source_entry) = S ((S (gsp_index_count_source)) * c)) /\ exists ff_q_gsp_count_source_entry_source. b = ff_q_gsp_count_source_entry_source * S ((S (gsp_index_count_source)) * c) + (gsp_value_count_source_entry))) /\ ((((exists ff_h_gsp_count_source_entry_magnitude. ff_h_gsp_count_source_entry_magnitude + S (gsp_magnitude_count_source_entry) = S ((S (gsp_index_count_source)) * mc)) /\ exists ff_q_gsp_count_source_entry_magnitude. mb = ff_q_gsp_count_source_entry_magnitude * S ((S (gsp_index_count_source)) * mc) + (gsp_magnitude_count_source_entry))) /\ ((((exists ff_h_gsp_count_source_entry_sign. ff_h_gsp_count_source_entry_sign + S (gsp_sign_count_source_entry) = S ((S (gsp_index_count_source)) * sc)) /\ exists ff_q_gsp_count_source_entry_sign. sb = ff_q_gsp_count_source_entry_sign * S ((S (gsp_index_count_source)) * sc) + (gsp_sign_count_source_entry))) /\ ((exists gsp_lt_gap_count_source_entry_positive. gsp_lt_gap_count_source_entry_positive + S 0 = gsp_magnitude_count_source_entry) /\ ((exists gsp_le_gap_count_source_entry_bounded. gsp_le_gap_count_source_entry_bounded + gsp_magnitude_count_source_entry = h) /\ ((gsp_sign_count_source_entry = 0 \/ gsp_sign_count_source_entry = 1) /\ (((gsp_sign_count_source_entry = 0 /\ (exists gsp_mod_left_count_source_entry_lower gsp_mod_right_count_source_entry_lower. (a * gsp_value_count_source_entry) + p * gsp_mod_left_count_source_entry_lower = (gsp_magnitude_count_source_entry) + p * gsp_mod_right_count_source_entry_lower)) \/ (gsp_sign_count_source_entry = 1 /\ (exists gsp_mod_left_count_source_entry_reflected gsp_mod_right_count_source_entry_reflected. (a * gsp_value_count_source_entry) + p * gsp_mod_left_count_source_entry_reflected = ((2 * h) * gsp_magnitude_count_source_entry) + p * gsp_mod_right_count_source_entry_reflected))))))))))) -> exists n. (((exists ff_u_gsp_count_result_sum ff_v_gsp_count_result_sum. ((((exists ff_h_gsp_count_result_sum_start. ff_h_gsp_count_result_sum_start + S (0) = S ((S (0)) * ff_v_gsp_count_result_sum)) /\ exists ff_q_gsp_count_result_sum_start. ff_u_gsp_count_result_sum = ff_q_gsp_count_result_sum_start * S ((S (0)) * ff_v_gsp_count_result_sum) + (0))) /\ ((((exists ff_h_gsp_count_result_sum_terminal. ff_h_gsp_count_result_sum_terminal + S (n) = S ((S (l)) * ff_v_gsp_count_result_sum)) /\ exists ff_q_gsp_count_result_sum_terminal. ff_u_gsp_count_result_sum = ff_q_gsp_count_result_sum_terminal * S ((S (l)) * ff_v_gsp_count_result_sum) + (n))) /\ forall ff_i_gsp_count_result_sum. (exists ff_lt_gsp_count_result_sum_bound. ff_lt_gsp_count_result_sum_bound + S ff_i_gsp_count_result_sum = l) -> exists ff_a_gsp_count_result_sum ff_r_gsp_count_result_sum ff_s_gsp_count_result_sum. ((((exists ff_h_gsp_count_result_sum_summand. ff_h_gsp_count_result_sum_summand + S (ff_a_gsp_count_result_sum) = S ((S (ff_i_gsp_count_result_sum)) * sc)) /\ exists ff_q_gsp_count_result_sum_summand. sb = ff_q_gsp_count_result_sum_summand * S ((S (ff_i_gsp_count_result_sum)) * sc) + (ff_a_gsp_count_result_sum))) /\ ((((exists ff_h_gsp_count_result_sum_partial. ff_h_gsp_count_result_sum_partial + S (ff_r_gsp_count_result_sum) = S ((S (ff_i_gsp_count_result_sum)) * ff_v_gsp_count_result_sum)) /\ exists ff_q_gsp_count_result_sum_partial. ff_u_gsp_count_result_sum = ff_q_gsp_count_result_sum_partial * S ((S (ff_i_gsp_count_result_sum)) * ff_v_gsp_count_result_sum) + (ff_r_gsp_count_result_sum))) /\ ((((exists ff_h_gsp_count_result_sum_successor. ff_h_gsp_count_result_sum_successor + S (ff_s_gsp_count_result_sum) = S ((S (S ff_i_gsp_count_result_sum)) * ff_v_gsp_count_result_sum)) /\ exists ff_q_gsp_count_result_sum_successor. ff_u_gsp_count_result_sum = ff_q_gsp_count_result_sum_successor * S ((S (S ff_i_gsp_count_result_sum)) * ff_v_gsp_count_result_sum) + (ff_s_gsp_count_result_sum))) /\ ff_s_gsp_count_result_sum = ff_r_gsp_count_result_sum + ff_a_gsp_count_result_sum)))))) /\ (forall ff_i_gsp_count_result_bits. (exists ff_lt_gsp_count_result_bits_bound. ff_lt_gsp_count_result_bits_bound + S ff_i_gsp_count_result_bits = l) -> exists ff_bit_gsp_count_result_bits. ((((exists ff_h_gsp_count_result_bits_decoded. ff_h_gsp_count_result_bits_decoded + S (ff_bit_gsp_count_result_bits) = S ((S (ff_i_gsp_count_result_bits)) * sc)) /\ exists ff_q_gsp_count_result_bits_decoded. sb = ff_q_gsp_count_result_bits_decoded * S ((S (ff_i_gsp_count_result_bits)) * sc) + (ff_bit_gsp_count_result_bits))) /\ (ff_bit_gsp_count_result_bits = 0 \/ ff_bit_gsp_count_result_bits = 1)))))

Structural proof guide

Generated structural guide

The encoded reflection bits have a native relational count of their ones.

Use the direct prerequisites gauss_signed_half_prefix_all_bits, bit_count_exists as previously established PA formulas.

The proof proceeds by intermediate claims (1).

Referenced ingredients

PA0076 gauss_signed_half_prefix_all_bits PA003I bit_count_exists

Proof neighborhood

Direct dependencies

PA0076 gauss_signed_half_prefix_all_bits PA003I bit_count_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

29 script commands · 4 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 prefix all bitsbit count 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 l
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hprefix
03Establish hbitsL12–21

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

  1. L12
    have hbits : forall ff_i_gsp_count_bits. (exists ff_lt_gsp_count_bits_bound. ff_lt_gsp_count_bits_bound + S ff_i_gsp_count_bits = l) -> exists ff_bit_gsp_count_bits. ((((exists ff_h_gsp_count_bits_decoded. ff_h_gsp_count_bits_decoded + S (ff_bit_gsp_count_bits) = S ((S (ff_i_gsp_count_bits)) * sc)) /\ exists ff_q_gsp_count_bits_decoded. sb = ff_q_gsp_count_bits_decoded * S ((S (ff_i_gsp_count_bits)) * sc) + (ff_bit_gsp_count_bits))) /\ (ff_bit_gsp_count_bits = 0 \/ ff_bit_gsp_count_bits = 1))
  2. L13
    specialize gauss_signed_half_prefix_all_bits p
  3. L14
    specialize gauss_signed_half_prefix_all_bits h
  4. L15
    specialize gauss_signed_half_prefix_all_bits a
  5. L16
    specialize gauss_signed_half_prefix_all_bits b
  6. L17
    specialize gauss_signed_half_prefix_all_bits c
  7. L18
    specialize gauss_signed_half_prefix_all_bits mb
  8. L19
    specialize gauss_signed_half_prefix_all_bits mc
  9. L20
    specialize gauss_signed_half_prefix_all_bits sb
  10. L21
    specialize gauss_signed_half_prefix_all_bits sc
04Use earlier factsL22–29

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

  1. L22
    specialize gauss_signed_half_prefix_all_bits l
  2. L23
    apply gauss_signed_half_prefix_all_bits
  3. L24
    exact hprefix
  4. L25
    specialize bit_count_exists sb
  5. L26
    specialize bit_count_exists sc
  6. L27
    specialize bit_count_exists l
  7. L28
    apply bit_count_exists
  8. L29
    exact hbits

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 l
  11. 0011intro hprefix
  12. 0012have hbits : forall ff_i_gsp_count_bits. (exists ff_lt_gsp_count_bits_bound. ff_lt_gsp_count_bits_bound + S ff_i_gsp_count_bits = l) -> exists ff_bit_gsp_count_bits. ((((exists ff_h_gsp_count_bits_decoded. ff_h_gsp_count_bits_decoded + S (ff_bit_gsp_count_bits) = S ((S (ff_i_gsp_count_bits)) * sc)) /\ exists ff_q_gsp_count_bits_decoded. sb = ff_q_gsp_count_bits_decoded * S ((S (ff_i_gsp_count_bits)) * sc) + (ff_bit_gsp_count_bits))) /\ (ff_bit_gsp_count_bits = 0 \/ ff_bit_gsp_count_bits = 1))
  13. 0013specialize gauss_signed_half_prefix_all_bits p
  14. 0014specialize gauss_signed_half_prefix_all_bits h
  15. 0015specialize gauss_signed_half_prefix_all_bits a
  16. 0016specialize gauss_signed_half_prefix_all_bits b
  17. 0017specialize gauss_signed_half_prefix_all_bits c
  18. 0018specialize gauss_signed_half_prefix_all_bits mb
  19. 0019specialize gauss_signed_half_prefix_all_bits mc
  20. 0020specialize gauss_signed_half_prefix_all_bits sb
  21. 0021specialize gauss_signed_half_prefix_all_bits sc
  22. 0022specialize gauss_signed_half_prefix_all_bits l
  23. 0023apply gauss_signed_half_prefix_all_bits
  24. 0024exact hprefix
  25. 0025specialize bit_count_exists sb
  26. 0026specialize bit_count_exists sc
  27. 0027specialize bit_count_exists l
  28. 0028apply bit_count_exists
  29. 0029exact hbits