PA0077 · theorem

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.

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. BitCount(sb,sc,l,x)

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 PD0017 BitCount

9 occurrences

In local proof propositions

PD0016 AllBits

1 occurrences

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

Proof neighborhood

Direct theorem prerequisites

PA0076 gauss_signed_half_prefix_all_bits PA003I bit_count_exists

Direct theorem dependents

PA0085 gauss_lemma_power_congruence_exists

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 · 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.

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 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 : AllBits(sb,sc,l)Definitions: AllBits(sb,sc,l)Original native command in the exact edition
  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 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 l
  11. 0011intro hprefix
  12. 0012have hbits : AllBits(sb,sc,l)
    Exact native replay linehave 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