PA0085

gauss_lemma_power_congruence_exists

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

Gauss's signed half-range count controls a^h modulo the odd prime.

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. p = 2 * h + 1 -> ((~(p = 1) /\ forall frp_prime_left_lemma_endpoint_prime frp_prime_right_lemma_endpoint_prime. p = frp_prime_left_lemma_endpoint_prime * frp_prime_right_lemma_endpoint_prime -> frp_prime_left_lemma_endpoint_prime = 1 \/ frp_prime_right_lemma_endpoint_prime = 1)) -> (~(exists gsp_divisor_factor_lemma_endpoint_nondivisor. a = p * gsp_divisor_factor_lemma_endpoint_nondivisor)) -> (forall gsp_range_index_lemma_endpoint_half_range. (exists gsp_lt_gap_lemma_endpoint_half_range_range_bound. gsp_lt_gap_lemma_endpoint_half_range_range_bound + S gsp_range_index_lemma_endpoint_half_range = h) -> (((exists gsp_beta_height_lemma_endpoint_half_range_range_entry. gsp_beta_height_lemma_endpoint_half_range_range_entry + S (1 + gsp_range_index_lemma_endpoint_half_range) = S ((S (gsp_range_index_lemma_endpoint_half_range)) * c)) /\ exists gsp_beta_quotient_lemma_endpoint_half_range_range_entry. b = gsp_beta_quotient_lemma_endpoint_half_range_range_entry * S ((S (gsp_range_index_lemma_endpoint_half_range)) * c) + (1 + gsp_range_index_lemma_endpoint_half_range)))) -> (exists e A R. ((exists ff_b_lemma_endpoint_multiplier_power ff_c_lemma_endpoint_multiplier_power. ((forall ff_i_lemma_endpoint_multiplier_power_repeat. (exists ff_lt_lemma_endpoint_multiplier_power_repeat_bound. ff_lt_lemma_endpoint_multiplier_power_repeat_bound + S ff_i_lemma_endpoint_multiplier_power_repeat = h) -> (((exists ff_h_lemma_endpoint_multiplier_power_repeat_decoded. ff_h_lemma_endpoint_multiplier_power_repeat_decoded + S (a) = S ((S (ff_i_lemma_endpoint_multiplier_power_repeat)) * ff_c_lemma_endpoint_multiplier_power)) /\ exists ff_q_lemma_endpoint_multiplier_power_repeat_decoded. ff_b_lemma_endpoint_multiplier_power = ff_q_lemma_endpoint_multiplier_power_repeat_decoded * S ((S (ff_i_lemma_endpoint_multiplier_power_repeat)) * ff_c_lemma_endpoint_multiplier_power) + (a)))) /\ (exists ff_u_lemma_endpoint_multiplier_power_product ff_v_lemma_endpoint_multiplier_power_product. ((((exists ff_h_lemma_endpoint_multiplier_power_product_start. ff_h_lemma_endpoint_multiplier_power_product_start + S (1) = S ((S (0)) * ff_v_lemma_endpoint_multiplier_power_product)) /\ exists ff_q_lemma_endpoint_multiplier_power_product_start. ff_u_lemma_endpoint_multiplier_power_product = ff_q_lemma_endpoint_multiplier_power_product_start * S ((S (0)) * ff_v_lemma_endpoint_multiplier_power_product) + (1))) /\ ((((exists ff_h_lemma_endpoint_multiplier_power_product_terminal. ff_h_lemma_endpoint_multiplier_power_product_terminal + S (A) = S ((S (h)) * ff_v_lemma_endpoint_multiplier_power_product)) /\ exists ff_q_lemma_endpoint_multiplier_power_product_terminal. ff_u_lemma_endpoint_multiplier_power_product = ff_q_lemma_endpoint_multiplier_power_product_terminal * S ((S (h)) * ff_v_lemma_endpoint_multiplier_power_product) + (A))) /\ forall ff_i_lemma_endpoint_multiplier_power_product. (exists ff_lt_lemma_endpoint_multiplier_power_product_bound. ff_lt_lemma_endpoint_multiplier_power_product_bound + S ff_i_lemma_endpoint_multiplier_power_product = h) -> exists ff_p_lemma_endpoint_multiplier_power_product ff_r_lemma_endpoint_multiplier_power_product ff_s_lemma_endpoint_multiplier_power_product. ((((exists ff_h_lemma_endpoint_multiplier_power_product_factor. ff_h_lemma_endpoint_multiplier_power_product_factor + S (ff_p_lemma_endpoint_multiplier_power_product) = S ((S (ff_i_lemma_endpoint_multiplier_power_product)) * ff_c_lemma_endpoint_multiplier_power)) /\ exists ff_q_lemma_endpoint_multiplier_power_product_factor. ff_b_lemma_endpoint_multiplier_power = ff_q_lemma_endpoint_multiplier_power_product_factor * S ((S (ff_i_lemma_endpoint_multiplier_power_product)) * ff_c_lemma_endpoint_multiplier_power) + (ff_p_lemma_endpoint_multiplier_power_product))) /\ ((((exists ff_h_lemma_endpoint_multiplier_power_product_partial. ff_h_lemma_endpoint_multiplier_power_product_partial + S (ff_r_lemma_endpoint_multiplier_power_product) = S ((S (ff_i_lemma_endpoint_multiplier_power_product)) * ff_v_lemma_endpoint_multiplier_power_product)) /\ exists ff_q_lemma_endpoint_multiplier_power_product_partial. ff_u_lemma_endpoint_multiplier_power_product = ff_q_lemma_endpoint_multiplier_power_product_partial * S ((S (ff_i_lemma_endpoint_multiplier_power_product)) * ff_v_lemma_endpoint_multiplier_power_product) + (ff_r_lemma_endpoint_multiplier_power_product))) /\ ((((exists ff_h_lemma_endpoint_multiplier_power_product_successor. ff_h_lemma_endpoint_multiplier_power_product_successor + S (ff_s_lemma_endpoint_multiplier_power_product) = S ((S (S ff_i_lemma_endpoint_multiplier_power_product)) * ff_v_lemma_endpoint_multiplier_power_product)) /\ exists ff_q_lemma_endpoint_multiplier_power_product_successor. ff_u_lemma_endpoint_multiplier_power_product = ff_q_lemma_endpoint_multiplier_power_product_successor * S ((S (S ff_i_lemma_endpoint_multiplier_power_product)) * ff_v_lemma_endpoint_multiplier_power_product) + (ff_s_lemma_endpoint_multiplier_power_product))) /\ ff_s_lemma_endpoint_multiplier_power_product = ff_r_lemma_endpoint_multiplier_power_product * ff_p_lemma_endpoint_multiplier_power_product)))))))) /\ ((exists ff_b_lemma_endpoint_result_sign_power_expanded ff_c_lemma_endpoint_result_sign_power_expanded. ((forall ff_i_lemma_endpoint_result_sign_power_expanded_repeat. (exists ff_lt_lemma_endpoint_result_sign_power_expanded_repeat_bound. ff_lt_lemma_endpoint_result_sign_power_expanded_repeat_bound + S ff_i_lemma_endpoint_result_sign_power_expanded_repeat = e) -> (((exists ff_h_lemma_endpoint_result_sign_power_expanded_repeat_decoded. ff_h_lemma_endpoint_result_sign_power_expanded_repeat_decoded + S ((2 * h)) = S ((S (ff_i_lemma_endpoint_result_sign_power_expanded_repeat)) * ff_c_lemma_endpoint_result_sign_power_expanded)) /\ exists ff_q_lemma_endpoint_result_sign_power_expanded_repeat_decoded. ff_b_lemma_endpoint_result_sign_power_expanded = ff_q_lemma_endpoint_result_sign_power_expanded_repeat_decoded * S ((S (ff_i_lemma_endpoint_result_sign_power_expanded_repeat)) * ff_c_lemma_endpoint_result_sign_power_expanded) + ((2 * h))))) /\ (exists ff_u_lemma_endpoint_result_sign_power_expanded_product ff_v_lemma_endpoint_result_sign_power_expanded_product. ((((exists ff_h_lemma_endpoint_result_sign_power_expanded_product_start. ff_h_lemma_endpoint_result_sign_power_expanded_product_start + S (1) = S ((S (0)) * ff_v_lemma_endpoint_result_sign_power_expanded_product)) /\ exists ff_q_lemma_endpoint_result_sign_power_expanded_product_start. ff_u_lemma_endpoint_result_sign_power_expanded_product = ff_q_lemma_endpoint_result_sign_power_expanded_product_start * S ((S (0)) * ff_v_lemma_endpoint_result_sign_power_expanded_product) + (1))) /\ ((((exists ff_h_lemma_endpoint_result_sign_power_expanded_product_terminal. ff_h_lemma_endpoint_result_sign_power_expanded_product_terminal + S (R) = S ((S (e)) * ff_v_lemma_endpoint_result_sign_power_expanded_product)) /\ exists ff_q_lemma_endpoint_result_sign_power_expanded_product_terminal. ff_u_lemma_endpoint_result_sign_power_expanded_product = ff_q_lemma_endpoint_result_sign_power_expanded_product_terminal * S ((S (e)) * ff_v_lemma_endpoint_result_sign_power_expanded_product) + (R))) /\ forall ff_i_lemma_endpoint_result_sign_power_expanded_product. (exists ff_lt_lemma_endpoint_result_sign_power_expanded_product_bound. ff_lt_lemma_endpoint_result_sign_power_expanded_product_bound + S ff_i_lemma_endpoint_result_sign_power_expanded_product = e) -> exists ff_p_lemma_endpoint_result_sign_power_expanded_product ff_r_lemma_endpoint_result_sign_power_expanded_product ff_s_lemma_endpoint_result_sign_power_expanded_product. ((((exists ff_h_lemma_endpoint_result_sign_power_expanded_product_factor. ff_h_lemma_endpoint_result_sign_power_expanded_product_factor + S (ff_p_lemma_endpoint_result_sign_power_expanded_product) = S ((S (ff_i_lemma_endpoint_result_sign_power_expanded_product)) * ff_c_lemma_endpoint_result_sign_power_expanded)) /\ exists ff_q_lemma_endpoint_result_sign_power_expanded_product_factor. ff_b_lemma_endpoint_result_sign_power_expanded = ff_q_lemma_endpoint_result_sign_power_expanded_product_factor * S ((S (ff_i_lemma_endpoint_result_sign_power_expanded_product)) * ff_c_lemma_endpoint_result_sign_power_expanded) + (ff_p_lemma_endpoint_result_sign_power_expanded_product))) /\ ((((exists ff_h_lemma_endpoint_result_sign_power_expanded_product_partial. ff_h_lemma_endpoint_result_sign_power_expanded_product_partial + S (ff_r_lemma_endpoint_result_sign_power_expanded_product) = S ((S (ff_i_lemma_endpoint_result_sign_power_expanded_product)) * ff_v_lemma_endpoint_result_sign_power_expanded_product)) /\ exists ff_q_lemma_endpoint_result_sign_power_expanded_product_partial. ff_u_lemma_endpoint_result_sign_power_expanded_product = ff_q_lemma_endpoint_result_sign_power_expanded_product_partial * S ((S (ff_i_lemma_endpoint_result_sign_power_expanded_product)) * ff_v_lemma_endpoint_result_sign_power_expanded_product) + (ff_r_lemma_endpoint_result_sign_power_expanded_product))) /\ ((((exists ff_h_lemma_endpoint_result_sign_power_expanded_product_successor. ff_h_lemma_endpoint_result_sign_power_expanded_product_successor + S (ff_s_lemma_endpoint_result_sign_power_expanded_product) = S ((S (S ff_i_lemma_endpoint_result_sign_power_expanded_product)) * ff_v_lemma_endpoint_result_sign_power_expanded_product)) /\ exists ff_q_lemma_endpoint_result_sign_power_expanded_product_successor. ff_u_lemma_endpoint_result_sign_power_expanded_product = ff_q_lemma_endpoint_result_sign_power_expanded_product_successor * S ((S (S ff_i_lemma_endpoint_result_sign_power_expanded_product)) * ff_v_lemma_endpoint_result_sign_power_expanded_product) + (ff_s_lemma_endpoint_result_sign_power_expanded_product))) /\ ff_s_lemma_endpoint_result_sign_power_expanded_product = ff_r_lemma_endpoint_result_sign_power_expanded_product * ff_p_lemma_endpoint_result_sign_power_expanded_product)))))))) /\ ((exists mb mc sb sc. ((forall gsp_index_lemma_endpoint_signed_prefix. (exists gsp_lt_gap_lemma_endpoint_signed_prefix_index_bound. gsp_lt_gap_lemma_endpoint_signed_prefix_index_bound + S gsp_index_lemma_endpoint_signed_prefix = h) -> (exists gsp_value_lemma_endpoint_signed_prefix_entry gsp_magnitude_lemma_endpoint_signed_prefix_entry gsp_sign_lemma_endpoint_signed_prefix_entry. (((exists ff_h_gsp_lemma_endpoint_signed_prefix_entry_source. ff_h_gsp_lemma_endpoint_signed_prefix_entry_source + S (gsp_value_lemma_endpoint_signed_prefix_entry) = S ((S (gsp_index_lemma_endpoint_signed_prefix)) * c)) /\ exists ff_q_gsp_lemma_endpoint_signed_prefix_entry_source. b = ff_q_gsp_lemma_endpoint_signed_prefix_entry_source * S ((S (gsp_index_lemma_endpoint_signed_prefix)) * c) + (gsp_value_lemma_endpoint_signed_prefix_entry))) /\ ((((exists ff_h_gsp_lemma_endpoint_signed_prefix_entry_magnitude. ff_h_gsp_lemma_endpoint_signed_prefix_entry_magnitude + S (gsp_magnitude_lemma_endpoint_signed_prefix_entry) = S ((S (gsp_index_lemma_endpoint_signed_prefix)) * mc)) /\ exists ff_q_gsp_lemma_endpoint_signed_prefix_entry_magnitude. mb = ff_q_gsp_lemma_endpoint_signed_prefix_entry_magnitude * S ((S (gsp_index_lemma_endpoint_signed_prefix)) * mc) + (gsp_magnitude_lemma_endpoint_signed_prefix_entry))) /\ ((((exists ff_h_gsp_lemma_endpoint_signed_prefix_entry_sign. ff_h_gsp_lemma_endpoint_signed_prefix_entry_sign + S (gsp_sign_lemma_endpoint_signed_prefix_entry) = S ((S (gsp_index_lemma_endpoint_signed_prefix)) * sc)) /\ exists ff_q_gsp_lemma_endpoint_signed_prefix_entry_sign. sb = ff_q_gsp_lemma_endpoint_signed_prefix_entry_sign * S ((S (gsp_index_lemma_endpoint_signed_prefix)) * sc) + (gsp_sign_lemma_endpoint_signed_prefix_entry))) /\ ((exists gsp_lt_gap_lemma_endpoint_signed_prefix_entry_positive. gsp_lt_gap_lemma_endpoint_signed_prefix_entry_positive + S 0 = gsp_magnitude_lemma_endpoint_signed_prefix_entry) /\ ((exists gsp_le_gap_lemma_endpoint_signed_prefix_entry_bounded. gsp_le_gap_lemma_endpoint_signed_prefix_entry_bounded + gsp_magnitude_lemma_endpoint_signed_prefix_entry = h) /\ ((gsp_sign_lemma_endpoint_signed_prefix_entry = 0 \/ gsp_sign_lemma_endpoint_signed_prefix_entry = 1) /\ (((gsp_sign_lemma_endpoint_signed_prefix_entry = 0 /\ (exists gsp_mod_left_lemma_endpoint_signed_prefix_entry_lower gsp_mod_right_lemma_endpoint_signed_prefix_entry_lower. (a * gsp_value_lemma_endpoint_signed_prefix_entry) + p * gsp_mod_left_lemma_endpoint_signed_prefix_entry_lower = (gsp_magnitude_lemma_endpoint_signed_prefix_entry) + p * gsp_mod_right_lemma_endpoint_signed_prefix_entry_lower)) \/ (gsp_sign_lemma_endpoint_signed_prefix_entry = 1 /\ (exists gsp_mod_left_lemma_endpoint_signed_prefix_entry_reflected gsp_mod_right_lemma_endpoint_signed_prefix_entry_reflected. (a * gsp_value_lemma_endpoint_signed_prefix_entry) + p * gsp_mod_left_lemma_endpoint_signed_prefix_entry_reflected = ((2 * h) * gsp_magnitude_lemma_endpoint_signed_prefix_entry) + p * gsp_mod_right_lemma_endpoint_signed_prefix_entry_reflected))))))))))) /\ (((exists ff_u_lemma_endpoint_bit_count_sum ff_v_lemma_endpoint_bit_count_sum. ((((exists ff_h_lemma_endpoint_bit_count_sum_start. ff_h_lemma_endpoint_bit_count_sum_start + S (0) = S ((S (0)) * ff_v_lemma_endpoint_bit_count_sum)) /\ exists ff_q_lemma_endpoint_bit_count_sum_start. ff_u_lemma_endpoint_bit_count_sum = ff_q_lemma_endpoint_bit_count_sum_start * S ((S (0)) * ff_v_lemma_endpoint_bit_count_sum) + (0))) /\ ((((exists ff_h_lemma_endpoint_bit_count_sum_terminal. ff_h_lemma_endpoint_bit_count_sum_terminal + S (e) = S ((S (h)) * ff_v_lemma_endpoint_bit_count_sum)) /\ exists ff_q_lemma_endpoint_bit_count_sum_terminal. ff_u_lemma_endpoint_bit_count_sum = ff_q_lemma_endpoint_bit_count_sum_terminal * S ((S (h)) * ff_v_lemma_endpoint_bit_count_sum) + (e))) /\ forall ff_i_lemma_endpoint_bit_count_sum. (exists ff_lt_lemma_endpoint_bit_count_sum_bound. ff_lt_lemma_endpoint_bit_count_sum_bound + S ff_i_lemma_endpoint_bit_count_sum = h) -> exists ff_a_lemma_endpoint_bit_count_sum ff_r_lemma_endpoint_bit_count_sum ff_s_lemma_endpoint_bit_count_sum. ((((exists ff_h_lemma_endpoint_bit_count_sum_summand. ff_h_lemma_endpoint_bit_count_sum_summand + S (ff_a_lemma_endpoint_bit_count_sum) = S ((S (ff_i_lemma_endpoint_bit_count_sum)) * sc)) /\ exists ff_q_lemma_endpoint_bit_count_sum_summand. sb = ff_q_lemma_endpoint_bit_count_sum_summand * S ((S (ff_i_lemma_endpoint_bit_count_sum)) * sc) + (ff_a_lemma_endpoint_bit_count_sum))) /\ ((((exists ff_h_lemma_endpoint_bit_count_sum_partial. ff_h_lemma_endpoint_bit_count_sum_partial + S (ff_r_lemma_endpoint_bit_count_sum) = S ((S (ff_i_lemma_endpoint_bit_count_sum)) * ff_v_lemma_endpoint_bit_count_sum)) /\ exists ff_q_lemma_endpoint_bit_count_sum_partial. ff_u_lemma_endpoint_bit_count_sum = ff_q_lemma_endpoint_bit_count_sum_partial * S ((S (ff_i_lemma_endpoint_bit_count_sum)) * ff_v_lemma_endpoint_bit_count_sum) + (ff_r_lemma_endpoint_bit_count_sum))) /\ ((((exists ff_h_lemma_endpoint_bit_count_sum_successor. ff_h_lemma_endpoint_bit_count_sum_successor + S (ff_s_lemma_endpoint_bit_count_sum) = S ((S (S ff_i_lemma_endpoint_bit_count_sum)) * ff_v_lemma_endpoint_bit_count_sum)) /\ exists ff_q_lemma_endpoint_bit_count_sum_successor. ff_u_lemma_endpoint_bit_count_sum = ff_q_lemma_endpoint_bit_count_sum_successor * S ((S (S ff_i_lemma_endpoint_bit_count_sum)) * ff_v_lemma_endpoint_bit_count_sum) + (ff_s_lemma_endpoint_bit_count_sum))) /\ ff_s_lemma_endpoint_bit_count_sum = ff_r_lemma_endpoint_bit_count_sum + ff_a_lemma_endpoint_bit_count_sum)))))) /\ (forall ff_i_lemma_endpoint_bit_count_bits. (exists ff_lt_lemma_endpoint_bit_count_bits_bound. ff_lt_lemma_endpoint_bit_count_bits_bound + S ff_i_lemma_endpoint_bit_count_bits = h) -> exists ff_bit_lemma_endpoint_bit_count_bits. ((((exists ff_h_lemma_endpoint_bit_count_bits_decoded. ff_h_lemma_endpoint_bit_count_bits_decoded + S (ff_bit_lemma_endpoint_bit_count_bits) = S ((S (ff_i_lemma_endpoint_bit_count_bits)) * sc)) /\ exists ff_q_lemma_endpoint_bit_count_bits_decoded. sb = ff_q_lemma_endpoint_bit_count_bits_decoded * S ((S (ff_i_lemma_endpoint_bit_count_bits)) * sc) + (ff_bit_lemma_endpoint_bit_count_bits))) /\ (ff_bit_lemma_endpoint_bit_count_bits = 0 \/ ff_bit_lemma_endpoint_bit_count_bits = 1))))))) /\ (exists gle_left_lemma_endpoint_result gle_right_lemma_endpoint_result. A + p * gle_left_lemma_endpoint_result = R + p * gle_right_lemma_endpoint_result)))))

Structural proof guide

Generated structural guide

Gauss's signed half-range count controls a^h modulo the odd prime.

Use the direct prerequisites gauss_half_range_signed_prefix_exists, gauss_signed_half_bit_count_exists, gauss_signed_half_magnitude_range, gauss_signed_half_magnitude_injective, gauss_signed_half_predecessor_recode_exists, beta_product_exists, beta_sign_factor_product_power_exists, beta_pointwise_mul_product_exists, pow_exists, gauss_signed_products_cancel_mod as previously established PA formulas.

The proof proceeds by case analysis (22), intermediate claims (12), certified simplification (1).

Referenced ingredients

PA0075 gauss_half_range_signed_prefix_exists PA0077 gauss_signed_half_bit_count_exists PA0078 gauss_signed_half_magnitude_range PA007C gauss_signed_half_magnitude_injective PA007E gauss_signed_half_predecessor_recode_exists PA003X beta_product_exists PA007J beta_sign_factor_product_power_exists PA007O beta_pointwise_mul_product_exists PA0046 pow_exists PA0084 gauss_signed_products_cancel_mod

Proof neighborhood

Direct dependencies

PA0075 gauss_half_range_signed_prefix_exists PA0077 gauss_signed_half_bit_count_exists PA0078 gauss_signed_half_magnitude_range PA007C gauss_signed_half_magnitude_injective PA007E gauss_signed_half_predecessor_recode_exists PA003X beta_product_exists PA007J beta_sign_factor_product_power_exists PA007O beta_pointwise_mul_product_exists PA0046 pow_exists PA0084 gauss_signed_products_cancel_mod

Direct dependents

PA00BV arbitrary_gauss_lemma_complete

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

193 script commands · 41 reading checkpoints · 12 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 (10)
gauss half range signed prefix existsgauss signed half bit count existsgauss signed half magnitude rangegauss signed half magnitude injectivegauss signed half predecessor recode existsbeta product existsbeta sign factor product power existsbeta pointwise mul product existspow existsgauss signed products cancel mod

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–9

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 hpodd
  7. L7
    intro hprime
  8. L8
    intro hnotdiv
  9. L9
    intro hhalf
02Establish hpsuccL10–13

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

  1. L10
    have hpsucc : p = S (2 * h)
  2. L11
    trans 2 * h + 1
  3. L12
    exact hpodd
  4. L13
    simp
03Establish hsigned_existsL14–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gauss half range signed prefix exists.

  1. L14
    have hsigned_exists : ∃ 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)))))))Definitions: LeLtModEqBetaAt
  2. L15
    specialize gauss_half_range_signed_prefix_exists p
  3. L16
    specialize gauss_half_range_signed_prefix_exists h
  4. L17
    specialize gauss_half_range_signed_prefix_exists a
  5. L18
    specialize gauss_half_range_signed_prefix_exists b
  6. L19
    specialize gauss_half_range_signed_prefix_exists c
  7. L20
    apply gauss_half_range_signed_prefix_exists
  8. L21
    exact hpodd
  9. L22
    exact hprime
  10. L23
    exact hnotdiv
04Use earlier factsL24–24

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

  1. L24
    exact hhalf
05Separate the logical casesL25–28

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

  1. L25
    cases hsigned_exists
  2. L26
    cases hsigned_exists_witness
  3. L27
    cases hsigned_exists_witness_witness
  4. L28
    cases hsigned_exists_witness_witness_witness
06Establish hcount_existsL29–38

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

  1. L29
    have hcount_exists : ∃ e. BitCount(x2,x3,h,e)Definitions: BitCount
  2. L30
    specialize gauss_signed_half_bit_count_exists p
  3. L31
    specialize gauss_signed_half_bit_count_exists h
  4. L32
    specialize gauss_signed_half_bit_count_exists a
  5. L33
    specialize gauss_signed_half_bit_count_exists b
  6. L34
    specialize gauss_signed_half_bit_count_exists c
  7. L35
    specialize gauss_signed_half_bit_count_exists x
  8. L36
    specialize gauss_signed_half_bit_count_exists x1
  9. L37
    specialize gauss_signed_half_bit_count_exists x2
  10. L38
    specialize gauss_signed_half_bit_count_exists x3
07Use earlier factsL39–41

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

  1. L39
    specialize gauss_signed_half_bit_count_exists h
  2. L40
    apply gauss_signed_half_bit_count_exists
  3. L41
    exact hsigned_exists_witness_witness_witness_witness
08Separate the logical casesL42–42

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

  1. L42
    cases hcount_exists
09Establish hmagnitude_rangeL43–52

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

  1. L43
    have hmagnitude_range : ∀ gmp_index_lemma_endpoint_magnitude_range. Lt(gmp_index_lemma_endpoint_magnitude_range,h) → ∃ y. BetaAt(x,x1,gmp_index_lemma_endpoint_magnitude_range,y) ∧ (Lt(0,y) ∧ Le(y,h))Definitions: LeLtBetaAt
  2. L44
    specialize gauss_signed_half_magnitude_range p
  3. L45
    specialize gauss_signed_half_magnitude_range h
  4. L46
    specialize gauss_signed_half_magnitude_range a
  5. L47
    specialize gauss_signed_half_magnitude_range b
  6. L48
    specialize gauss_signed_half_magnitude_range c
  7. L49
    specialize gauss_signed_half_magnitude_range x
  8. L50
    specialize gauss_signed_half_magnitude_range x1
  9. L51
    specialize gauss_signed_half_magnitude_range x2
  10. L52
    specialize gauss_signed_half_magnitude_range x3
10Use earlier factsL53–55

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

  1. L53
    specialize gauss_signed_half_magnitude_range h
  2. L54
    apply gauss_signed_half_magnitude_range
  3. L55
    exact hsigned_exists_witness_witness_witness_witness
11Establish hmagnitude_injectiveL56–65

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

  1. L56
    have hmagnitude_injective : InjectivePrefix(x,x1,h)Definitions: InjectivePrefix
  2. L57
    specialize gauss_signed_half_magnitude_injective p
  3. L58
    specialize gauss_signed_half_magnitude_injective h
  4. L59
    specialize gauss_signed_half_magnitude_injective a
  5. L60
    specialize gauss_signed_half_magnitude_injective b
  6. L61
    specialize gauss_signed_half_magnitude_injective c
  7. L62
    specialize gauss_signed_half_magnitude_injective x
  8. L63
    specialize gauss_signed_half_magnitude_injective x1
  9. L64
    specialize gauss_signed_half_magnitude_injective x2
  10. L65
    specialize gauss_signed_half_magnitude_injective x3
12Use earlier factsL66–71

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

  1. L66
    apply gauss_signed_half_magnitude_injective
  2. L67
    exact hpodd
  3. L68
    exact hprime
  4. L69
    exact hnotdiv
  5. L70
    exact hhalf
  6. L71
    exact hsigned_exists_witness_witness_witness_witness
13Establish hrecode_existsL72–81

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

  1. L72
    have hrecode_exists : ∃ rb. ∃ rc. ∀ y. ∀ z. Lt(y,h) → BetaAt(x,x1,y,S z) → BetaAt(rb,rc,y,z)Definitions: LtBetaAt
  2. L73
    specialize gauss_signed_half_predecessor_recode_exists p
  3. L74
    specialize gauss_signed_half_predecessor_recode_exists h
  4. L75
    specialize gauss_signed_half_predecessor_recode_exists a
  5. L76
    specialize gauss_signed_half_predecessor_recode_exists b
  6. L77
    specialize gauss_signed_half_predecessor_recode_exists c
  7. L78
    specialize gauss_signed_half_predecessor_recode_exists x
  8. L79
    specialize gauss_signed_half_predecessor_recode_exists x1
  9. L80
    specialize gauss_signed_half_predecessor_recode_exists x2
  10. L81
    specialize gauss_signed_half_predecessor_recode_exists x3
14Use earlier factsL82–83

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

  1. L82
    apply gauss_signed_half_predecessor_recode_exists
  2. L83
    exact hsigned_exists_witness_witness_witness_witness
15Separate the logical casesL84–85

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

  1. L84
    cases hrecode_exists
  2. L85
    cases hrecode_exists_witness
16Establish hcanonical_product_existsL86–90

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

  1. L86
    have hcanonical_product_exists : ∃ P. Product(b,c,h,P)Definitions: Product
  2. L87
    specialize beta_product_exists b
  3. L88
    specialize beta_product_exists c
  4. L89
    specialize beta_product_exists h
  5. L90
    exact beta_product_exists
17Separate the logical casesL91–91

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

  1. L91
    cases hcanonical_product_exists
18Establish hmagnitude_product_existsL92–96

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

  1. L92
    have hmagnitude_product_exists : ∃ M. Product(x,x1,h,M)Definitions: Product
  2. L93
    specialize beta_product_exists x
  3. L94
    specialize beta_product_exists x1
  4. L95
    specialize beta_product_exists h
  5. L96
    exact beta_product_exists
19Separate the logical casesL97–97

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

  1. L97
    cases hmagnitude_product_exists
20Establish hsign_packageL98–107

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta sign factor product power exists.

  1. L98
    have hsign_package : ∃ fb. ∃ fc. ∃ Sprod. ∃ R. (∀ x. ∀ y. Lt(x,h) → BetaAt(x2,x3,x,y) → y = 0 ∧ BetaAt(fb,fc,x,1) ∨ y = 1 ∧ BetaAt(fb,fc,x,2 · h)) ∧ (Product(fb,fc,h,Sprod) ∧ (Pow(2 · h,x4,R) ∧ Sprod = R))Definitions: LtBetaAtProductPow
  2. L99
    specialize beta_sign_factor_product_power_exists p
  3. L100
    specialize beta_sign_factor_product_power_exists (2 * h)
  4. L101
    specialize beta_sign_factor_product_power_exists x2
  5. L102
    specialize beta_sign_factor_product_power_exists x3
  6. L103
    specialize beta_sign_factor_product_power_exists h
  7. L104
    specialize beta_sign_factor_product_power_exists x4
  8. L105
    apply beta_sign_factor_product_power_exists
  9. L106
    exact hpsucc
  10. L107
    exact hcount_exists_witness
21Separate the logical casesL108–114

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

  1. L108
    cases hsign_package
  2. L109
    cases hsign_package_witness
  3. L110
    cases hsign_package_witness_witness
  4. L111
    cases hsign_package_witness_witness_witness
  5. L112
    cases hsign_package_witness_witness_witness_witness
  6. L113
    cases hsign_package_witness_witness_witness_witness_right
  7. L114
    cases hsign_package_witness_witness_witness_witness_right_right
22Establish hpointwise_packageL115–124

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta pointwise mul product exists.

  1. L115
    have hpointwise_package : ∃ tb. ∃ tc. ∃ T. (∀ y. ∀ z. ∀ n. ∀ m. Lt(y,h) → BetaAt(x,x1,y,z) → BetaAt(x9,x10,y,n) → BetaAt(tb,tc,y,m) → m = z · n) ∧ (Product(tb,tc,h,T) ∧ T = x8 · x11)Definitions: LtBetaAtProduct
  2. L116
    specialize beta_pointwise_mul_product_exists x
  3. L117
    specialize beta_pointwise_mul_product_exists x1
  4. L118
    specialize beta_pointwise_mul_product_exists x9
  5. L119
    specialize beta_pointwise_mul_product_exists x10
  6. L120
    specialize beta_pointwise_mul_product_exists h
  7. L121
    specialize beta_pointwise_mul_product_exists x8
  8. L122
    specialize beta_pointwise_mul_product_exists x11
  9. L123
    apply beta_pointwise_mul_product_exists
  10. L124
    exact hmagnitude_product_exists_witness
23Use earlier factsL125–125

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

  1. L125
    exact hsign_package_witness_witness_witness_witness_right_left
24Separate the logical casesL126–130

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

  1. L126
    cases hpointwise_package
  2. L127
    cases hpointwise_package_witness
  3. L128
    cases hpointwise_package_witness_witness
  4. L129
    cases hpointwise_package_witness_witness_witness
  5. L130
    cases hpointwise_package_witness_witness_witness_right
25Establish hmultiplier_power_existsL131–134

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

  1. L131
    have hmultiplier_power_exists : ∃ A. Pow(a,h,A)Definitions: Pow
  2. L132
    specialize pow_exists a
  3. L133
    specialize pow_exists h
  4. L134
    exact pow_exists
26Separate the logical casesL135–135

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

  1. L135
    cases hmultiplier_power_exists
27Establish hcancelledL136–145

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

  1. L136
    have hcancelled : exists gle_left_lemma_endpoint_local_result gle_right_lemma_endpoint_local_result. x16 + p * gle_left_lemma_endpoint_local_result = x12 + p * gle_right_lemma_endpoint_local_result
  2. L137
    specialize gauss_signed_products_cancel_mod p
  3. L138
    specialize gauss_signed_products_cancel_mod h
  4. L139
    specialize gauss_signed_products_cancel_mod (2 * h)
  5. L140
    specialize gauss_signed_products_cancel_mod a
  6. L141
    specialize gauss_signed_products_cancel_mod b
  7. L142
    specialize gauss_signed_products_cancel_mod c
  8. L143
    specialize gauss_signed_products_cancel_mod x
  9. L144
    specialize gauss_signed_products_cancel_mod x1
  10. L145
    specialize gauss_signed_products_cancel_mod x5
28Use earlier factsL146–155

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

  1. L146
    specialize gauss_signed_products_cancel_mod x6
  2. L147
    specialize gauss_signed_products_cancel_mod x2
  3. L148
    specialize gauss_signed_products_cancel_mod x3
  4. L149
    specialize gauss_signed_products_cancel_mod x9
  5. L150
    specialize gauss_signed_products_cancel_mod x10
  6. L151
    specialize gauss_signed_products_cancel_mod x13
  7. L152
    specialize gauss_signed_products_cancel_mod x14
  8. L153
    specialize gauss_signed_products_cancel_mod x4
  9. L154
    specialize gauss_signed_products_cancel_mod x7
  10. L155
    specialize gauss_signed_products_cancel_mod x8
29Use earlier factsL156–162

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

  1. L156
    specialize gauss_signed_products_cancel_mod x11
  2. L157
    specialize gauss_signed_products_cancel_mod x15
  3. L158
    specialize gauss_signed_products_cancel_mod x16
  4. L159
    specialize gauss_signed_products_cancel_mod x12
  5. L160
    apply gauss_signed_products_cancel_mod
  6. L161
    exact hprime
  7. L162
    exact hpsucc
30Calculate and transport equalitiesL163–163

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L163
    refl
31Use earlier factsL164–173

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

  1. L164
    exact hsigned_exists_witness_witness_witness_witness
  2. L165
    exact hsign_package_witness_witness_witness_witness_left
  3. L166
    exact hpointwise_package_witness_witness_witness_left
  4. L167
    exact hmagnitude_range
  5. L168
    exact hmagnitude_injective
  6. L169
    exact hrecode_exists_witness_witness
  7. L170
    exact hhalf
  8. L171
    exact hcount_exists_witness
  9. L172
    exact hcanonical_product_exists_witness
  10. L173
    exact hmagnitude_product_exists_witness
32Use earlier factsL174–177

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

  1. L174
    exact hsign_package_witness_witness_witness_witness_right_left
  2. L175
    exact hpointwise_package_witness_witness_witness_right_left
  3. L176
    exact hmultiplier_power_exists_witness
  4. L177
    exact hsign_package_witness_witness_witness_witness_right_right_left
33Construct an explicit witnessL178–180

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

  1. L178
    exists x4
  2. L179
    exists x16
  3. L180
    exists x12
34Separate the logical casesL181–181

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

  1. L181
    split
35Use earlier factsL182–182

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

  1. L182
    exact hmultiplier_power_exists_witness
36Separate the logical casesL183–183

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

  1. L183
    split
37Use earlier factsL184–184

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

  1. L184
    exact hsign_package_witness_witness_witness_witness_right_right_left
38Separate the logical casesL185–185

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

  1. L185
    split
39Construct an explicit witnessL186–189

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

  1. L186
    exists x
  2. L187
    exists x1
  3. L188
    exists x2
  4. L189
    exists x3
40Separate the logical casesL190–190

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

  1. L190
    split
41Use earlier factsL191–193

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

  1. L191
    exact hsigned_exists_witness_witness_witness_witness
  2. L192
    exact hcount_exists_witness
  3. L193
    exact hcancelled

Library-wide reading audit

Original exact command ledger · 193 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro a
  4. 0004intro b
  5. 0005intro c
  6. 0006intro hpodd
  7. 0007intro hprime
  8. 0008intro hnotdiv
  9. 0009intro hhalf
  10. 0010have hpsucc : p = S (2 * h)
  11. 0011trans 2 * h + 1
  12. 0012exact hpodd
  13. 0013simp
  14. 0014have hsigned_exists : exists mb mc sb sc. (forall gsp_index_lemma_endpoint_signed_prefix. (exists gsp_lt_gap_lemma_endpoint_signed_prefix_index_bound. gsp_lt_gap_lemma_endpoint_signed_prefix_index_bound + S gsp_index_lemma_endpoint_signed_prefix = h) -> (exists gsp_value_lemma_endpoint_signed_prefix_entry gsp_magnitude_lemma_endpoint_signed_prefix_entry gsp_sign_lemma_endpoint_signed_prefix_entry. (((exists ff_h_gsp_lemma_endpoint_signed_prefix_entry_source. ff_h_gsp_lemma_endpoint_signed_prefix_entry_source + S (gsp_value_lemma_endpoint_signed_prefix_entry) = S ((S (gsp_index_lemma_endpoint_signed_prefix)) * c)) /\ exists ff_q_gsp_lemma_endpoint_signed_prefix_entry_source. b = ff_q_gsp_lemma_endpoint_signed_prefix_entry_source * S ((S (gsp_index_lemma_endpoint_signed_prefix)) * c) + (gsp_value_lemma_endpoint_signed_prefix_entry))) /\ ((((exists ff_h_gsp_lemma_endpoint_signed_prefix_entry_magnitude. ff_h_gsp_lemma_endpoint_signed_prefix_entry_magnitude + S (gsp_magnitude_lemma_endpoint_signed_prefix_entry) = S ((S (gsp_index_lemma_endpoint_signed_prefix)) * mc)) /\ exists ff_q_gsp_lemma_endpoint_signed_prefix_entry_magnitude. mb = ff_q_gsp_lemma_endpoint_signed_prefix_entry_magnitude * S ((S (gsp_index_lemma_endpoint_signed_prefix)) * mc) + (gsp_magnitude_lemma_endpoint_signed_prefix_entry))) /\ ((((exists ff_h_gsp_lemma_endpoint_signed_prefix_entry_sign. ff_h_gsp_lemma_endpoint_signed_prefix_entry_sign + S (gsp_sign_lemma_endpoint_signed_prefix_entry) = S ((S (gsp_index_lemma_endpoint_signed_prefix)) * sc)) /\ exists ff_q_gsp_lemma_endpoint_signed_prefix_entry_sign. sb = ff_q_gsp_lemma_endpoint_signed_prefix_entry_sign * S ((S (gsp_index_lemma_endpoint_signed_prefix)) * sc) + (gsp_sign_lemma_endpoint_signed_prefix_entry))) /\ ((exists gsp_lt_gap_lemma_endpoint_signed_prefix_entry_positive. gsp_lt_gap_lemma_endpoint_signed_prefix_entry_positive + S 0 = gsp_magnitude_lemma_endpoint_signed_prefix_entry) /\ ((exists gsp_le_gap_lemma_endpoint_signed_prefix_entry_bounded. gsp_le_gap_lemma_endpoint_signed_prefix_entry_bounded + gsp_magnitude_lemma_endpoint_signed_prefix_entry = h) /\ ((gsp_sign_lemma_endpoint_signed_prefix_entry = 0 \/ gsp_sign_lemma_endpoint_signed_prefix_entry = 1) /\ (((gsp_sign_lemma_endpoint_signed_prefix_entry = 0 /\ (exists gsp_mod_left_lemma_endpoint_signed_prefix_entry_lower gsp_mod_right_lemma_endpoint_signed_prefix_entry_lower. (a * gsp_value_lemma_endpoint_signed_prefix_entry) + p * gsp_mod_left_lemma_endpoint_signed_prefix_entry_lower = (gsp_magnitude_lemma_endpoint_signed_prefix_entry) + p * gsp_mod_right_lemma_endpoint_signed_prefix_entry_lower)) \/ (gsp_sign_lemma_endpoint_signed_prefix_entry = 1 /\ (exists gsp_mod_left_lemma_endpoint_signed_prefix_entry_reflected gsp_mod_right_lemma_endpoint_signed_prefix_entry_reflected. (a * gsp_value_lemma_endpoint_signed_prefix_entry) + p * gsp_mod_left_lemma_endpoint_signed_prefix_entry_reflected = ((2 * h) * gsp_magnitude_lemma_endpoint_signed_prefix_entry) + p * gsp_mod_right_lemma_endpoint_signed_prefix_entry_reflected)))))))))))
  15. 0015specialize gauss_half_range_signed_prefix_exists p
  16. 0016specialize gauss_half_range_signed_prefix_exists h
  17. 0017specialize gauss_half_range_signed_prefix_exists a
  18. 0018specialize gauss_half_range_signed_prefix_exists b
  19. 0019specialize gauss_half_range_signed_prefix_exists c
  20. 0020apply gauss_half_range_signed_prefix_exists
  21. 0021exact hpodd
  22. 0022exact hprime
  23. 0023exact hnotdiv
  24. 0024exact hhalf
  25. 0025cases hsigned_exists
  26. 0026cases hsigned_exists_witness
  27. 0027cases hsigned_exists_witness_witness
  28. 0028cases hsigned_exists_witness_witness_witness
  29. 0029have hcount_exists : exists e. (((exists ff_u_lemma_endpoint_local_bit_count_sum ff_v_lemma_endpoint_local_bit_count_sum. ((((exists ff_h_lemma_endpoint_local_bit_count_sum_start. ff_h_lemma_endpoint_local_bit_count_sum_start + S (0) = S ((S (0)) * ff_v_lemma_endpoint_local_bit_count_sum)) /\ exists ff_q_lemma_endpoint_local_bit_count_sum_start. ff_u_lemma_endpoint_local_bit_count_sum = ff_q_lemma_endpoint_local_bit_count_sum_start * S ((S (0)) * ff_v_lemma_endpoint_local_bit_count_sum) + (0))) /\ ((((exists ff_h_lemma_endpoint_local_bit_count_sum_terminal. ff_h_lemma_endpoint_local_bit_count_sum_terminal + S (e) = S ((S (h)) * ff_v_lemma_endpoint_local_bit_count_sum)) /\ exists ff_q_lemma_endpoint_local_bit_count_sum_terminal. ff_u_lemma_endpoint_local_bit_count_sum = ff_q_lemma_endpoint_local_bit_count_sum_terminal * S ((S (h)) * ff_v_lemma_endpoint_local_bit_count_sum) + (e))) /\ forall ff_i_lemma_endpoint_local_bit_count_sum. (exists ff_lt_lemma_endpoint_local_bit_count_sum_bound. ff_lt_lemma_endpoint_local_bit_count_sum_bound + S ff_i_lemma_endpoint_local_bit_count_sum = h) -> exists ff_a_lemma_endpoint_local_bit_count_sum ff_r_lemma_endpoint_local_bit_count_sum ff_s_lemma_endpoint_local_bit_count_sum. ((((exists ff_h_lemma_endpoint_local_bit_count_sum_summand. ff_h_lemma_endpoint_local_bit_count_sum_summand + S (ff_a_lemma_endpoint_local_bit_count_sum) = S ((S (ff_i_lemma_endpoint_local_bit_count_sum)) * x3)) /\ exists ff_q_lemma_endpoint_local_bit_count_sum_summand. x2 = ff_q_lemma_endpoint_local_bit_count_sum_summand * S ((S (ff_i_lemma_endpoint_local_bit_count_sum)) * x3) + (ff_a_lemma_endpoint_local_bit_count_sum))) /\ ((((exists ff_h_lemma_endpoint_local_bit_count_sum_partial. ff_h_lemma_endpoint_local_bit_count_sum_partial + S (ff_r_lemma_endpoint_local_bit_count_sum) = S ((S (ff_i_lemma_endpoint_local_bit_count_sum)) * ff_v_lemma_endpoint_local_bit_count_sum)) /\ exists ff_q_lemma_endpoint_local_bit_count_sum_partial. ff_u_lemma_endpoint_local_bit_count_sum = ff_q_lemma_endpoint_local_bit_count_sum_partial * S ((S (ff_i_lemma_endpoint_local_bit_count_sum)) * ff_v_lemma_endpoint_local_bit_count_sum) + (ff_r_lemma_endpoint_local_bit_count_sum))) /\ ((((exists ff_h_lemma_endpoint_local_bit_count_sum_successor. ff_h_lemma_endpoint_local_bit_count_sum_successor + S (ff_s_lemma_endpoint_local_bit_count_sum) = S ((S (S ff_i_lemma_endpoint_local_bit_count_sum)) * ff_v_lemma_endpoint_local_bit_count_sum)) /\ exists ff_q_lemma_endpoint_local_bit_count_sum_successor. ff_u_lemma_endpoint_local_bit_count_sum = ff_q_lemma_endpoint_local_bit_count_sum_successor * S ((S (S ff_i_lemma_endpoint_local_bit_count_sum)) * ff_v_lemma_endpoint_local_bit_count_sum) + (ff_s_lemma_endpoint_local_bit_count_sum))) /\ ff_s_lemma_endpoint_local_bit_count_sum = ff_r_lemma_endpoint_local_bit_count_sum + ff_a_lemma_endpoint_local_bit_count_sum)))))) /\ (forall ff_i_lemma_endpoint_local_bit_count_bits. (exists ff_lt_lemma_endpoint_local_bit_count_bits_bound. ff_lt_lemma_endpoint_local_bit_count_bits_bound + S ff_i_lemma_endpoint_local_bit_count_bits = h) -> exists ff_bit_lemma_endpoint_local_bit_count_bits. ((((exists ff_h_lemma_endpoint_local_bit_count_bits_decoded. ff_h_lemma_endpoint_local_bit_count_bits_decoded + S (ff_bit_lemma_endpoint_local_bit_count_bits) = S ((S (ff_i_lemma_endpoint_local_bit_count_bits)) * x3)) /\ exists ff_q_lemma_endpoint_local_bit_count_bits_decoded. x2 = ff_q_lemma_endpoint_local_bit_count_bits_decoded * S ((S (ff_i_lemma_endpoint_local_bit_count_bits)) * x3) + (ff_bit_lemma_endpoint_local_bit_count_bits))) /\ (ff_bit_lemma_endpoint_local_bit_count_bits = 0 \/ ff_bit_lemma_endpoint_local_bit_count_bits = 1)))))
  30. 0030specialize gauss_signed_half_bit_count_exists p
  31. 0031specialize gauss_signed_half_bit_count_exists h
  32. 0032specialize gauss_signed_half_bit_count_exists a
  33. 0033specialize gauss_signed_half_bit_count_exists b
  34. 0034specialize gauss_signed_half_bit_count_exists c
  35. 0035specialize gauss_signed_half_bit_count_exists x
  36. 0036specialize gauss_signed_half_bit_count_exists x1
  37. 0037specialize gauss_signed_half_bit_count_exists x2
  38. 0038specialize gauss_signed_half_bit_count_exists x3
  39. 0039specialize gauss_signed_half_bit_count_exists h
  40. 0040apply gauss_signed_half_bit_count_exists
  41. 0041exact hsigned_exists_witness_witness_witness_witness
  42. 0042cases hcount_exists
  43. 0043have hmagnitude_range : forall gmp_index_lemma_endpoint_magnitude_range. (exists gsp_lt_gap_lemma_endpoint_magnitude_range_index_bound. gsp_lt_gap_lemma_endpoint_magnitude_range_index_bound + S gmp_index_lemma_endpoint_magnitude_range = h) -> exists gmp_magnitude_lemma_endpoint_magnitude_range. ((((exists ff_h_gmp_lemma_endpoint_magnitude_range_decoded. ff_h_gmp_lemma_endpoint_magnitude_range_decoded + S (gmp_magnitude_lemma_endpoint_magnitude_range) = S ((S (gmp_index_lemma_endpoint_magnitude_range)) * x1)) /\ exists ff_q_gmp_lemma_endpoint_magnitude_range_decoded. x = ff_q_gmp_lemma_endpoint_magnitude_range_decoded * S ((S (gmp_index_lemma_endpoint_magnitude_range)) * x1) + (gmp_magnitude_lemma_endpoint_magnitude_range))) /\ ((exists gsp_lt_gap_lemma_endpoint_magnitude_range_positive. gsp_lt_gap_lemma_endpoint_magnitude_range_positive + S 0 = gmp_magnitude_lemma_endpoint_magnitude_range) /\ (exists gsp_le_gap_lemma_endpoint_magnitude_range_bounded. gsp_le_gap_lemma_endpoint_magnitude_range_bounded + gmp_magnitude_lemma_endpoint_magnitude_range = h)))
  44. 0044specialize gauss_signed_half_magnitude_range p
  45. 0045specialize gauss_signed_half_magnitude_range h
  46. 0046specialize gauss_signed_half_magnitude_range a
  47. 0047specialize gauss_signed_half_magnitude_range b
  48. 0048specialize gauss_signed_half_magnitude_range c
  49. 0049specialize gauss_signed_half_magnitude_range x
  50. 0050specialize gauss_signed_half_magnitude_range x1
  51. 0051specialize gauss_signed_half_magnitude_range x2
  52. 0052specialize gauss_signed_half_magnitude_range x3
  53. 0053specialize gauss_signed_half_magnitude_range h
  54. 0054apply gauss_signed_half_magnitude_range
  55. 0055exact hsigned_exists_witness_witness_witness_witness
  56. 0056have hmagnitude_injective : forall fp_i_lemma_endpoint_magnitude_injective fp_j_lemma_endpoint_magnitude_injective fp_value_lemma_endpoint_magnitude_injective. (exists fp_gap_lemma_endpoint_magnitude_injective_i. fp_gap_lemma_endpoint_magnitude_injective_i + S fp_i_lemma_endpoint_magnitude_injective = h) -> (exists fp_gap_lemma_endpoint_magnitude_injective_j. fp_gap_lemma_endpoint_magnitude_injective_j + S fp_j_lemma_endpoint_magnitude_injective = h) -> (((exists ff_h_lemma_endpoint_magnitude_injective_left. ff_h_lemma_endpoint_magnitude_injective_left + S (fp_value_lemma_endpoint_magnitude_injective) = S ((S (fp_i_lemma_endpoint_magnitude_injective)) * x1)) /\ exists ff_q_lemma_endpoint_magnitude_injective_left. x = ff_q_lemma_endpoint_magnitude_injective_left * S ((S (fp_i_lemma_endpoint_magnitude_injective)) * x1) + (fp_value_lemma_endpoint_magnitude_injective))) -> (((exists ff_h_lemma_endpoint_magnitude_injective_right. ff_h_lemma_endpoint_magnitude_injective_right + S (fp_value_lemma_endpoint_magnitude_injective) = S ((S (fp_j_lemma_endpoint_magnitude_injective)) * x1)) /\ exists ff_q_lemma_endpoint_magnitude_injective_right. x = ff_q_lemma_endpoint_magnitude_injective_right * S ((S (fp_j_lemma_endpoint_magnitude_injective)) * x1) + (fp_value_lemma_endpoint_magnitude_injective))) -> fp_i_lemma_endpoint_magnitude_injective = fp_j_lemma_endpoint_magnitude_injective
  57. 0057specialize gauss_signed_half_magnitude_injective p
  58. 0058specialize gauss_signed_half_magnitude_injective h
  59. 0059specialize gauss_signed_half_magnitude_injective a
  60. 0060specialize gauss_signed_half_magnitude_injective b
  61. 0061specialize gauss_signed_half_magnitude_injective c
  62. 0062specialize gauss_signed_half_magnitude_injective x
  63. 0063specialize gauss_signed_half_magnitude_injective x1
  64. 0064specialize gauss_signed_half_magnitude_injective x2
  65. 0065specialize gauss_signed_half_magnitude_injective x3
  66. 0066apply gauss_signed_half_magnitude_injective
  67. 0067exact hpodd
  68. 0068exact hprime
  69. 0069exact hnotdiv
  70. 0070exact hhalf
  71. 0071exact hsigned_exists_witness_witness_witness_witness
  72. 0072have hrecode_exists : exists rb rc. (forall gmp_index_lemma_endpoint_predecessor_recode gmp_predecessor_lemma_endpoint_predecessor_recode. (exists gsp_lt_gap_lemma_endpoint_predecessor_recode_index_bound. gsp_lt_gap_lemma_endpoint_predecessor_recode_index_bound + S gmp_index_lemma_endpoint_predecessor_recode = h) -> (((exists gsp_beta_height_gmp_lemma_endpoint_predecessor_recode_source. gsp_beta_height_gmp_lemma_endpoint_predecessor_recode_source + S (S gmp_predecessor_lemma_endpoint_predecessor_recode) = S ((S (gmp_index_lemma_endpoint_predecessor_recode)) * x1)) /\ exists gsp_beta_quotient_gmp_lemma_endpoint_predecessor_recode_source. x = gsp_beta_quotient_gmp_lemma_endpoint_predecessor_recode_source * S ((S (gmp_index_lemma_endpoint_predecessor_recode)) * x1) + (S gmp_predecessor_lemma_endpoint_predecessor_recode))) -> (((exists ff_h_gmp_lemma_endpoint_predecessor_recode_target. ff_h_gmp_lemma_endpoint_predecessor_recode_target + S (gmp_predecessor_lemma_endpoint_predecessor_recode) = S ((S (gmp_index_lemma_endpoint_predecessor_recode)) * rc)) /\ exists ff_q_gmp_lemma_endpoint_predecessor_recode_target. rb = ff_q_gmp_lemma_endpoint_predecessor_recode_target * S ((S (gmp_index_lemma_endpoint_predecessor_recode)) * rc) + (gmp_predecessor_lemma_endpoint_predecessor_recode))))
  73. 0073specialize gauss_signed_half_predecessor_recode_exists p
  74. 0074specialize gauss_signed_half_predecessor_recode_exists h
  75. 0075specialize gauss_signed_half_predecessor_recode_exists a
  76. 0076specialize gauss_signed_half_predecessor_recode_exists b
  77. 0077specialize gauss_signed_half_predecessor_recode_exists c
  78. 0078specialize gauss_signed_half_predecessor_recode_exists x
  79. 0079specialize gauss_signed_half_predecessor_recode_exists x1
  80. 0080specialize gauss_signed_half_predecessor_recode_exists x2
  81. 0081specialize gauss_signed_half_predecessor_recode_exists x3
  82. 0082apply gauss_signed_half_predecessor_recode_exists
  83. 0083exact hsigned_exists_witness_witness_witness_witness
  84. 0084cases hrecode_exists
  85. 0085cases hrecode_exists_witness
  86. 0086have hcanonical_product_exists : exists P. (exists ff_u_lemma_endpoint_canonical_product ff_v_lemma_endpoint_canonical_product. ((((exists ff_h_lemma_endpoint_canonical_product_start. ff_h_lemma_endpoint_canonical_product_start + S (1) = S ((S (0)) * ff_v_lemma_endpoint_canonical_product)) /\ exists ff_q_lemma_endpoint_canonical_product_start. ff_u_lemma_endpoint_canonical_product = ff_q_lemma_endpoint_canonical_product_start * S ((S (0)) * ff_v_lemma_endpoint_canonical_product) + (1))) /\ ((((exists ff_h_lemma_endpoint_canonical_product_terminal. ff_h_lemma_endpoint_canonical_product_terminal + S (P) = S ((S (h)) * ff_v_lemma_endpoint_canonical_product)) /\ exists ff_q_lemma_endpoint_canonical_product_terminal. ff_u_lemma_endpoint_canonical_product = ff_q_lemma_endpoint_canonical_product_terminal * S ((S (h)) * ff_v_lemma_endpoint_canonical_product) + (P))) /\ forall ff_i_lemma_endpoint_canonical_product. (exists ff_lt_lemma_endpoint_canonical_product_bound. ff_lt_lemma_endpoint_canonical_product_bound + S ff_i_lemma_endpoint_canonical_product = h) -> exists ff_p_lemma_endpoint_canonical_product ff_r_lemma_endpoint_canonical_product ff_s_lemma_endpoint_canonical_product. ((((exists ff_h_lemma_endpoint_canonical_product_factor. ff_h_lemma_endpoint_canonical_product_factor + S (ff_p_lemma_endpoint_canonical_product) = S ((S (ff_i_lemma_endpoint_canonical_product)) * c)) /\ exists ff_q_lemma_endpoint_canonical_product_factor. b = ff_q_lemma_endpoint_canonical_product_factor * S ((S (ff_i_lemma_endpoint_canonical_product)) * c) + (ff_p_lemma_endpoint_canonical_product))) /\ ((((exists ff_h_lemma_endpoint_canonical_product_partial. ff_h_lemma_endpoint_canonical_product_partial + S (ff_r_lemma_endpoint_canonical_product) = S ((S (ff_i_lemma_endpoint_canonical_product)) * ff_v_lemma_endpoint_canonical_product)) /\ exists ff_q_lemma_endpoint_canonical_product_partial. ff_u_lemma_endpoint_canonical_product = ff_q_lemma_endpoint_canonical_product_partial * S ((S (ff_i_lemma_endpoint_canonical_product)) * ff_v_lemma_endpoint_canonical_product) + (ff_r_lemma_endpoint_canonical_product))) /\ ((((exists ff_h_lemma_endpoint_canonical_product_successor. ff_h_lemma_endpoint_canonical_product_successor + S (ff_s_lemma_endpoint_canonical_product) = S ((S (S ff_i_lemma_endpoint_canonical_product)) * ff_v_lemma_endpoint_canonical_product)) /\ exists ff_q_lemma_endpoint_canonical_product_successor. ff_u_lemma_endpoint_canonical_product = ff_q_lemma_endpoint_canonical_product_successor * S ((S (S ff_i_lemma_endpoint_canonical_product)) * ff_v_lemma_endpoint_canonical_product) + (ff_s_lemma_endpoint_canonical_product))) /\ ff_s_lemma_endpoint_canonical_product = ff_r_lemma_endpoint_canonical_product * ff_p_lemma_endpoint_canonical_product))))))
  87. 0087specialize beta_product_exists b
  88. 0088specialize beta_product_exists c
  89. 0089specialize beta_product_exists h
  90. 0090exact beta_product_exists
  91. 0091cases hcanonical_product_exists
  92. 0092have hmagnitude_product_exists : exists M. (exists ff_u_lemma_endpoint_magnitude_product ff_v_lemma_endpoint_magnitude_product. ((((exists ff_h_lemma_endpoint_magnitude_product_start. ff_h_lemma_endpoint_magnitude_product_start + S (1) = S ((S (0)) * ff_v_lemma_endpoint_magnitude_product)) /\ exists ff_q_lemma_endpoint_magnitude_product_start. ff_u_lemma_endpoint_magnitude_product = ff_q_lemma_endpoint_magnitude_product_start * S ((S (0)) * ff_v_lemma_endpoint_magnitude_product) + (1))) /\ ((((exists ff_h_lemma_endpoint_magnitude_product_terminal. ff_h_lemma_endpoint_magnitude_product_terminal + S (M) = S ((S (h)) * ff_v_lemma_endpoint_magnitude_product)) /\ exists ff_q_lemma_endpoint_magnitude_product_terminal. ff_u_lemma_endpoint_magnitude_product = ff_q_lemma_endpoint_magnitude_product_terminal * S ((S (h)) * ff_v_lemma_endpoint_magnitude_product) + (M))) /\ forall ff_i_lemma_endpoint_magnitude_product. (exists ff_lt_lemma_endpoint_magnitude_product_bound. ff_lt_lemma_endpoint_magnitude_product_bound + S ff_i_lemma_endpoint_magnitude_product = h) -> exists ff_p_lemma_endpoint_magnitude_product ff_r_lemma_endpoint_magnitude_product ff_s_lemma_endpoint_magnitude_product. ((((exists ff_h_lemma_endpoint_magnitude_product_factor. ff_h_lemma_endpoint_magnitude_product_factor + S (ff_p_lemma_endpoint_magnitude_product) = S ((S (ff_i_lemma_endpoint_magnitude_product)) * x1)) /\ exists ff_q_lemma_endpoint_magnitude_product_factor. x = ff_q_lemma_endpoint_magnitude_product_factor * S ((S (ff_i_lemma_endpoint_magnitude_product)) * x1) + (ff_p_lemma_endpoint_magnitude_product))) /\ ((((exists ff_h_lemma_endpoint_magnitude_product_partial. ff_h_lemma_endpoint_magnitude_product_partial + S (ff_r_lemma_endpoint_magnitude_product) = S ((S (ff_i_lemma_endpoint_magnitude_product)) * ff_v_lemma_endpoint_magnitude_product)) /\ exists ff_q_lemma_endpoint_magnitude_product_partial. ff_u_lemma_endpoint_magnitude_product = ff_q_lemma_endpoint_magnitude_product_partial * S ((S (ff_i_lemma_endpoint_magnitude_product)) * ff_v_lemma_endpoint_magnitude_product) + (ff_r_lemma_endpoint_magnitude_product))) /\ ((((exists ff_h_lemma_endpoint_magnitude_product_successor. ff_h_lemma_endpoint_magnitude_product_successor + S (ff_s_lemma_endpoint_magnitude_product) = S ((S (S ff_i_lemma_endpoint_magnitude_product)) * ff_v_lemma_endpoint_magnitude_product)) /\ exists ff_q_lemma_endpoint_magnitude_product_successor. ff_u_lemma_endpoint_magnitude_product = ff_q_lemma_endpoint_magnitude_product_successor * S ((S (S ff_i_lemma_endpoint_magnitude_product)) * ff_v_lemma_endpoint_magnitude_product) + (ff_s_lemma_endpoint_magnitude_product))) /\ ff_s_lemma_endpoint_magnitude_product = ff_r_lemma_endpoint_magnitude_product * ff_p_lemma_endpoint_magnitude_product))))))
  93. 0093specialize beta_product_exists x
  94. 0094specialize beta_product_exists x1
  95. 0095specialize beta_product_exists h
  96. 0096exact beta_product_exists
  97. 0097cases hmagnitude_product_exists
  98. 0098have hsign_package : exists fb fc Sprod R. ((forall gspf_index_lemma_endpoint_sign_factors_expanded gspf_bit_lemma_endpoint_sign_factors_expanded. (exists gsp_lt_gap_lemma_endpoint_sign_factors_expanded_bound. gsp_lt_gap_lemma_endpoint_sign_factors_expanded_bound + S gspf_index_lemma_endpoint_sign_factors_expanded = h) -> (((exists ff_h_gspf_lemma_endpoint_sign_factors_expanded_bit. ff_h_gspf_lemma_endpoint_sign_factors_expanded_bit + S (gspf_bit_lemma_endpoint_sign_factors_expanded) = S ((S (gspf_index_lemma_endpoint_sign_factors_expanded)) * x3)) /\ exists ff_q_gspf_lemma_endpoint_sign_factors_expanded_bit. x2 = ff_q_gspf_lemma_endpoint_sign_factors_expanded_bit * S ((S (gspf_index_lemma_endpoint_sign_factors_expanded)) * x3) + (gspf_bit_lemma_endpoint_sign_factors_expanded))) -> (((gspf_bit_lemma_endpoint_sign_factors_expanded = 0) /\ (((exists gsp_beta_height_gspf_lemma_endpoint_sign_factors_expanded_one. gsp_beta_height_gspf_lemma_endpoint_sign_factors_expanded_one + S (1) = S ((S (gspf_index_lemma_endpoint_sign_factors_expanded)) * fc)) /\ exists gsp_beta_quotient_gspf_lemma_endpoint_sign_factors_expanded_one. fb = gsp_beta_quotient_gspf_lemma_endpoint_sign_factors_expanded_one * S ((S (gspf_index_lemma_endpoint_sign_factors_expanded)) * fc) + (1)))) \/ ((gspf_bit_lemma_endpoint_sign_factors_expanded = 1) /\ (((exists ff_h_gspf_lemma_endpoint_sign_factors_expanded_predecessor. ff_h_gspf_lemma_endpoint_sign_factors_expanded_predecessor + S ((2 * h)) = S ((S (gspf_index_lemma_endpoint_sign_factors_expanded)) * fc)) /\ exists ff_q_gspf_lemma_endpoint_sign_factors_expanded_predecessor. fb = ff_q_gspf_lemma_endpoint_sign_factors_expanded_predecessor * S ((S (gspf_index_lemma_endpoint_sign_factors_expanded)) * fc) + ((2 * h))))))) /\ ((exists ff_u_lemma_endpoint_sign_product ff_v_lemma_endpoint_sign_product. ((((exists ff_h_lemma_endpoint_sign_product_start. ff_h_lemma_endpoint_sign_product_start + S (1) = S ((S (0)) * ff_v_lemma_endpoint_sign_product)) /\ exists ff_q_lemma_endpoint_sign_product_start. ff_u_lemma_endpoint_sign_product = ff_q_lemma_endpoint_sign_product_start * S ((S (0)) * ff_v_lemma_endpoint_sign_product) + (1))) /\ ((((exists ff_h_lemma_endpoint_sign_product_terminal. ff_h_lemma_endpoint_sign_product_terminal + S (Sprod) = S ((S (h)) * ff_v_lemma_endpoint_sign_product)) /\ exists ff_q_lemma_endpoint_sign_product_terminal. ff_u_lemma_endpoint_sign_product = ff_q_lemma_endpoint_sign_product_terminal * S ((S (h)) * ff_v_lemma_endpoint_sign_product) + (Sprod))) /\ forall ff_i_lemma_endpoint_sign_product. (exists ff_lt_lemma_endpoint_sign_product_bound. ff_lt_lemma_endpoint_sign_product_bound + S ff_i_lemma_endpoint_sign_product = h) -> exists ff_p_lemma_endpoint_sign_product ff_r_lemma_endpoint_sign_product ff_s_lemma_endpoint_sign_product. ((((exists ff_h_lemma_endpoint_sign_product_factor. ff_h_lemma_endpoint_sign_product_factor + S (ff_p_lemma_endpoint_sign_product) = S ((S (ff_i_lemma_endpoint_sign_product)) * fc)) /\ exists ff_q_lemma_endpoint_sign_product_factor. fb = ff_q_lemma_endpoint_sign_product_factor * S ((S (ff_i_lemma_endpoint_sign_product)) * fc) + (ff_p_lemma_endpoint_sign_product))) /\ ((((exists ff_h_lemma_endpoint_sign_product_partial. ff_h_lemma_endpoint_sign_product_partial + S (ff_r_lemma_endpoint_sign_product) = S ((S (ff_i_lemma_endpoint_sign_product)) * ff_v_lemma_endpoint_sign_product)) /\ exists ff_q_lemma_endpoint_sign_product_partial. ff_u_lemma_endpoint_sign_product = ff_q_lemma_endpoint_sign_product_partial * S ((S (ff_i_lemma_endpoint_sign_product)) * ff_v_lemma_endpoint_sign_product) + (ff_r_lemma_endpoint_sign_product))) /\ ((((exists ff_h_lemma_endpoint_sign_product_successor. ff_h_lemma_endpoint_sign_product_successor + S (ff_s_lemma_endpoint_sign_product) = S ((S (S ff_i_lemma_endpoint_sign_product)) * ff_v_lemma_endpoint_sign_product)) /\ exists ff_q_lemma_endpoint_sign_product_successor. ff_u_lemma_endpoint_sign_product = ff_q_lemma_endpoint_sign_product_successor * S ((S (S ff_i_lemma_endpoint_sign_product)) * ff_v_lemma_endpoint_sign_product) + (ff_s_lemma_endpoint_sign_product))) /\ ff_s_lemma_endpoint_sign_product = ff_r_lemma_endpoint_sign_product * ff_p_lemma_endpoint_sign_product)))))) /\ ((exists ff_b_lemma_endpoint_sign_power_expanded ff_c_lemma_endpoint_sign_power_expanded. ((forall ff_i_lemma_endpoint_sign_power_expanded_repeat. (exists ff_lt_lemma_endpoint_sign_power_expanded_repeat_bound. ff_lt_lemma_endpoint_sign_power_expanded_repeat_bound + S ff_i_lemma_endpoint_sign_power_expanded_repeat = x4) -> (((exists ff_h_lemma_endpoint_sign_power_expanded_repeat_decoded. ff_h_lemma_endpoint_sign_power_expanded_repeat_decoded + S ((2 * h)) = S ((S (ff_i_lemma_endpoint_sign_power_expanded_repeat)) * ff_c_lemma_endpoint_sign_power_expanded)) /\ exists ff_q_lemma_endpoint_sign_power_expanded_repeat_decoded. ff_b_lemma_endpoint_sign_power_expanded = ff_q_lemma_endpoint_sign_power_expanded_repeat_decoded * S ((S (ff_i_lemma_endpoint_sign_power_expanded_repeat)) * ff_c_lemma_endpoint_sign_power_expanded) + ((2 * h))))) /\ (exists ff_u_lemma_endpoint_sign_power_expanded_product ff_v_lemma_endpoint_sign_power_expanded_product. ((((exists ff_h_lemma_endpoint_sign_power_expanded_product_start. ff_h_lemma_endpoint_sign_power_expanded_product_start + S (1) = S ((S (0)) * ff_v_lemma_endpoint_sign_power_expanded_product)) /\ exists ff_q_lemma_endpoint_sign_power_expanded_product_start. ff_u_lemma_endpoint_sign_power_expanded_product = ff_q_lemma_endpoint_sign_power_expanded_product_start * S ((S (0)) * ff_v_lemma_endpoint_sign_power_expanded_product) + (1))) /\ ((((exists ff_h_lemma_endpoint_sign_power_expanded_product_terminal. ff_h_lemma_endpoint_sign_power_expanded_product_terminal + S (R) = S ((S (x4)) * ff_v_lemma_endpoint_sign_power_expanded_product)) /\ exists ff_q_lemma_endpoint_sign_power_expanded_product_terminal. ff_u_lemma_endpoint_sign_power_expanded_product = ff_q_lemma_endpoint_sign_power_expanded_product_terminal * S ((S (x4)) * ff_v_lemma_endpoint_sign_power_expanded_product) + (R))) /\ forall ff_i_lemma_endpoint_sign_power_expanded_product. (exists ff_lt_lemma_endpoint_sign_power_expanded_product_bound. ff_lt_lemma_endpoint_sign_power_expanded_product_bound + S ff_i_lemma_endpoint_sign_power_expanded_product = x4) -> exists ff_p_lemma_endpoint_sign_power_expanded_product ff_r_lemma_endpoint_sign_power_expanded_product ff_s_lemma_endpoint_sign_power_expanded_product. ((((exists ff_h_lemma_endpoint_sign_power_expanded_product_factor. ff_h_lemma_endpoint_sign_power_expanded_product_factor + S (ff_p_lemma_endpoint_sign_power_expanded_product) = S ((S (ff_i_lemma_endpoint_sign_power_expanded_product)) * ff_c_lemma_endpoint_sign_power_expanded)) /\ exists ff_q_lemma_endpoint_sign_power_expanded_product_factor. ff_b_lemma_endpoint_sign_power_expanded = ff_q_lemma_endpoint_sign_power_expanded_product_factor * S ((S (ff_i_lemma_endpoint_sign_power_expanded_product)) * ff_c_lemma_endpoint_sign_power_expanded) + (ff_p_lemma_endpoint_sign_power_expanded_product))) /\ ((((exists ff_h_lemma_endpoint_sign_power_expanded_product_partial. ff_h_lemma_endpoint_sign_power_expanded_product_partial + S (ff_r_lemma_endpoint_sign_power_expanded_product) = S ((S (ff_i_lemma_endpoint_sign_power_expanded_product)) * ff_v_lemma_endpoint_sign_power_expanded_product)) /\ exists ff_q_lemma_endpoint_sign_power_expanded_product_partial. ff_u_lemma_endpoint_sign_power_expanded_product = ff_q_lemma_endpoint_sign_power_expanded_product_partial * S ((S (ff_i_lemma_endpoint_sign_power_expanded_product)) * ff_v_lemma_endpoint_sign_power_expanded_product) + (ff_r_lemma_endpoint_sign_power_expanded_product))) /\ ((((exists ff_h_lemma_endpoint_sign_power_expanded_product_successor. ff_h_lemma_endpoint_sign_power_expanded_product_successor + S (ff_s_lemma_endpoint_sign_power_expanded_product) = S ((S (S ff_i_lemma_endpoint_sign_power_expanded_product)) * ff_v_lemma_endpoint_sign_power_expanded_product)) /\ exists ff_q_lemma_endpoint_sign_power_expanded_product_successor. ff_u_lemma_endpoint_sign_power_expanded_product = ff_q_lemma_endpoint_sign_power_expanded_product_successor * S ((S (S ff_i_lemma_endpoint_sign_power_expanded_product)) * ff_v_lemma_endpoint_sign_power_expanded_product) + (ff_s_lemma_endpoint_sign_power_expanded_product))) /\ ff_s_lemma_endpoint_sign_power_expanded_product = ff_r_lemma_endpoint_sign_power_expanded_product * ff_p_lemma_endpoint_sign_power_expanded_product)))))))) /\ Sprod = R)))
  99. 0099specialize beta_sign_factor_product_power_exists p
  100. 0100specialize beta_sign_factor_product_power_exists (2 * h)
  101. 0101specialize beta_sign_factor_product_power_exists x2
  102. 0102specialize beta_sign_factor_product_power_exists x3
  103. 0103specialize beta_sign_factor_product_power_exists h
  104. 0104specialize beta_sign_factor_product_power_exists x4
  105. 0105apply beta_sign_factor_product_power_exists
  106. 0106exact hpsucc
  107. 0107exact hcount_exists_witness
  108. 0108cases hsign_package
  109. 0109cases hsign_package_witness
  110. 0110cases hsign_package_witness_witness
  111. 0111cases hsign_package_witness_witness_witness
  112. 0112cases hsign_package_witness_witness_witness_witness
  113. 0113cases hsign_package_witness_witness_witness_witness_right
  114. 0114cases hsign_package_witness_witness_witness_witness_right_right
  115. 0115have hpointwise_package : exists tb tc T. ((forall fpmp_index_lemma_endpoint_pointwise_products fpmp_left_lemma_endpoint_pointwise_products fpmp_right_lemma_endpoint_pointwise_products fpmp_target_lemma_endpoint_pointwise_products. (exists fpmp_gap_lemma_endpoint_pointwise_products. fpmp_gap_lemma_endpoint_pointwise_products + S fpmp_index_lemma_endpoint_pointwise_products = h) -> (((exists ff_h_fpmp_lemma_endpoint_pointwise_products_left. ff_h_fpmp_lemma_endpoint_pointwise_products_left + S (fpmp_left_lemma_endpoint_pointwise_products) = S ((S (fpmp_index_lemma_endpoint_pointwise_products)) * x1)) /\ exists ff_q_fpmp_lemma_endpoint_pointwise_products_left. x = ff_q_fpmp_lemma_endpoint_pointwise_products_left * S ((S (fpmp_index_lemma_endpoint_pointwise_products)) * x1) + (fpmp_left_lemma_endpoint_pointwise_products))) -> (((exists ff_h_fpmp_lemma_endpoint_pointwise_products_right. ff_h_fpmp_lemma_endpoint_pointwise_products_right + S (fpmp_right_lemma_endpoint_pointwise_products) = S ((S (fpmp_index_lemma_endpoint_pointwise_products)) * x10)) /\ exists ff_q_fpmp_lemma_endpoint_pointwise_products_right. x9 = ff_q_fpmp_lemma_endpoint_pointwise_products_right * S ((S (fpmp_index_lemma_endpoint_pointwise_products)) * x10) + (fpmp_right_lemma_endpoint_pointwise_products))) -> (((exists ff_h_fpmp_lemma_endpoint_pointwise_products_target. ff_h_fpmp_lemma_endpoint_pointwise_products_target + S (fpmp_target_lemma_endpoint_pointwise_products) = S ((S (fpmp_index_lemma_endpoint_pointwise_products)) * tc)) /\ exists ff_q_fpmp_lemma_endpoint_pointwise_products_target. tb = ff_q_fpmp_lemma_endpoint_pointwise_products_target * S ((S (fpmp_index_lemma_endpoint_pointwise_products)) * tc) + (fpmp_target_lemma_endpoint_pointwise_products))) -> fpmp_target_lemma_endpoint_pointwise_products = fpmp_left_lemma_endpoint_pointwise_products * fpmp_right_lemma_endpoint_pointwise_products) /\ ((exists ff_u_lemma_endpoint_target_product ff_v_lemma_endpoint_target_product. ((((exists ff_h_lemma_endpoint_target_product_start. ff_h_lemma_endpoint_target_product_start + S (1) = S ((S (0)) * ff_v_lemma_endpoint_target_product)) /\ exists ff_q_lemma_endpoint_target_product_start. ff_u_lemma_endpoint_target_product = ff_q_lemma_endpoint_target_product_start * S ((S (0)) * ff_v_lemma_endpoint_target_product) + (1))) /\ ((((exists ff_h_lemma_endpoint_target_product_terminal. ff_h_lemma_endpoint_target_product_terminal + S (T) = S ((S (h)) * ff_v_lemma_endpoint_target_product)) /\ exists ff_q_lemma_endpoint_target_product_terminal. ff_u_lemma_endpoint_target_product = ff_q_lemma_endpoint_target_product_terminal * S ((S (h)) * ff_v_lemma_endpoint_target_product) + (T))) /\ forall ff_i_lemma_endpoint_target_product. (exists ff_lt_lemma_endpoint_target_product_bound. ff_lt_lemma_endpoint_target_product_bound + S ff_i_lemma_endpoint_target_product = h) -> exists ff_p_lemma_endpoint_target_product ff_r_lemma_endpoint_target_product ff_s_lemma_endpoint_target_product. ((((exists ff_h_lemma_endpoint_target_product_factor. ff_h_lemma_endpoint_target_product_factor + S (ff_p_lemma_endpoint_target_product) = S ((S (ff_i_lemma_endpoint_target_product)) * tc)) /\ exists ff_q_lemma_endpoint_target_product_factor. tb = ff_q_lemma_endpoint_target_product_factor * S ((S (ff_i_lemma_endpoint_target_product)) * tc) + (ff_p_lemma_endpoint_target_product))) /\ ((((exists ff_h_lemma_endpoint_target_product_partial. ff_h_lemma_endpoint_target_product_partial + S (ff_r_lemma_endpoint_target_product) = S ((S (ff_i_lemma_endpoint_target_product)) * ff_v_lemma_endpoint_target_product)) /\ exists ff_q_lemma_endpoint_target_product_partial. ff_u_lemma_endpoint_target_product = ff_q_lemma_endpoint_target_product_partial * S ((S (ff_i_lemma_endpoint_target_product)) * ff_v_lemma_endpoint_target_product) + (ff_r_lemma_endpoint_target_product))) /\ ((((exists ff_h_lemma_endpoint_target_product_successor. ff_h_lemma_endpoint_target_product_successor + S (ff_s_lemma_endpoint_target_product) = S ((S (S ff_i_lemma_endpoint_target_product)) * ff_v_lemma_endpoint_target_product)) /\ exists ff_q_lemma_endpoint_target_product_successor. ff_u_lemma_endpoint_target_product = ff_q_lemma_endpoint_target_product_successor * S ((S (S ff_i_lemma_endpoint_target_product)) * ff_v_lemma_endpoint_target_product) + (ff_s_lemma_endpoint_target_product))) /\ ff_s_lemma_endpoint_target_product = ff_r_lemma_endpoint_target_product * ff_p_lemma_endpoint_target_product)))))) /\ T = x8 * x11))
  116. 0116specialize beta_pointwise_mul_product_exists x
  117. 0117specialize beta_pointwise_mul_product_exists x1
  118. 0118specialize beta_pointwise_mul_product_exists x9
  119. 0119specialize beta_pointwise_mul_product_exists x10
  120. 0120specialize beta_pointwise_mul_product_exists h
  121. 0121specialize beta_pointwise_mul_product_exists x8
  122. 0122specialize beta_pointwise_mul_product_exists x11
  123. 0123apply beta_pointwise_mul_product_exists
  124. 0124exact hmagnitude_product_exists_witness
  125. 0125exact hsign_package_witness_witness_witness_witness_right_left
  126. 0126cases hpointwise_package
  127. 0127cases hpointwise_package_witness
  128. 0128cases hpointwise_package_witness_witness
  129. 0129cases hpointwise_package_witness_witness_witness
  130. 0130cases hpointwise_package_witness_witness_witness_right
  131. 0131have hmultiplier_power_exists : exists A. (exists ff_b_lemma_endpoint_multiplier_power ff_c_lemma_endpoint_multiplier_power. ((forall ff_i_lemma_endpoint_multiplier_power_repeat. (exists ff_lt_lemma_endpoint_multiplier_power_repeat_bound. ff_lt_lemma_endpoint_multiplier_power_repeat_bound + S ff_i_lemma_endpoint_multiplier_power_repeat = h) -> (((exists ff_h_lemma_endpoint_multiplier_power_repeat_decoded. ff_h_lemma_endpoint_multiplier_power_repeat_decoded + S (a) = S ((S (ff_i_lemma_endpoint_multiplier_power_repeat)) * ff_c_lemma_endpoint_multiplier_power)) /\ exists ff_q_lemma_endpoint_multiplier_power_repeat_decoded. ff_b_lemma_endpoint_multiplier_power = ff_q_lemma_endpoint_multiplier_power_repeat_decoded * S ((S (ff_i_lemma_endpoint_multiplier_power_repeat)) * ff_c_lemma_endpoint_multiplier_power) + (a)))) /\ (exists ff_u_lemma_endpoint_multiplier_power_product ff_v_lemma_endpoint_multiplier_power_product. ((((exists ff_h_lemma_endpoint_multiplier_power_product_start. ff_h_lemma_endpoint_multiplier_power_product_start + S (1) = S ((S (0)) * ff_v_lemma_endpoint_multiplier_power_product)) /\ exists ff_q_lemma_endpoint_multiplier_power_product_start. ff_u_lemma_endpoint_multiplier_power_product = ff_q_lemma_endpoint_multiplier_power_product_start * S ((S (0)) * ff_v_lemma_endpoint_multiplier_power_product) + (1))) /\ ((((exists ff_h_lemma_endpoint_multiplier_power_product_terminal. ff_h_lemma_endpoint_multiplier_power_product_terminal + S (A) = S ((S (h)) * ff_v_lemma_endpoint_multiplier_power_product)) /\ exists ff_q_lemma_endpoint_multiplier_power_product_terminal. ff_u_lemma_endpoint_multiplier_power_product = ff_q_lemma_endpoint_multiplier_power_product_terminal * S ((S (h)) * ff_v_lemma_endpoint_multiplier_power_product) + (A))) /\ forall ff_i_lemma_endpoint_multiplier_power_product. (exists ff_lt_lemma_endpoint_multiplier_power_product_bound. ff_lt_lemma_endpoint_multiplier_power_product_bound + S ff_i_lemma_endpoint_multiplier_power_product = h) -> exists ff_p_lemma_endpoint_multiplier_power_product ff_r_lemma_endpoint_multiplier_power_product ff_s_lemma_endpoint_multiplier_power_product. ((((exists ff_h_lemma_endpoint_multiplier_power_product_factor. ff_h_lemma_endpoint_multiplier_power_product_factor + S (ff_p_lemma_endpoint_multiplier_power_product) = S ((S (ff_i_lemma_endpoint_multiplier_power_product)) * ff_c_lemma_endpoint_multiplier_power)) /\ exists ff_q_lemma_endpoint_multiplier_power_product_factor. ff_b_lemma_endpoint_multiplier_power = ff_q_lemma_endpoint_multiplier_power_product_factor * S ((S (ff_i_lemma_endpoint_multiplier_power_product)) * ff_c_lemma_endpoint_multiplier_power) + (ff_p_lemma_endpoint_multiplier_power_product))) /\ ((((exists ff_h_lemma_endpoint_multiplier_power_product_partial. ff_h_lemma_endpoint_multiplier_power_product_partial + S (ff_r_lemma_endpoint_multiplier_power_product) = S ((S (ff_i_lemma_endpoint_multiplier_power_product)) * ff_v_lemma_endpoint_multiplier_power_product)) /\ exists ff_q_lemma_endpoint_multiplier_power_product_partial. ff_u_lemma_endpoint_multiplier_power_product = ff_q_lemma_endpoint_multiplier_power_product_partial * S ((S (ff_i_lemma_endpoint_multiplier_power_product)) * ff_v_lemma_endpoint_multiplier_power_product) + (ff_r_lemma_endpoint_multiplier_power_product))) /\ ((((exists ff_h_lemma_endpoint_multiplier_power_product_successor. ff_h_lemma_endpoint_multiplier_power_product_successor + S (ff_s_lemma_endpoint_multiplier_power_product) = S ((S (S ff_i_lemma_endpoint_multiplier_power_product)) * ff_v_lemma_endpoint_multiplier_power_product)) /\ exists ff_q_lemma_endpoint_multiplier_power_product_successor. ff_u_lemma_endpoint_multiplier_power_product = ff_q_lemma_endpoint_multiplier_power_product_successor * S ((S (S ff_i_lemma_endpoint_multiplier_power_product)) * ff_v_lemma_endpoint_multiplier_power_product) + (ff_s_lemma_endpoint_multiplier_power_product))) /\ ff_s_lemma_endpoint_multiplier_power_product = ff_r_lemma_endpoint_multiplier_power_product * ff_p_lemma_endpoint_multiplier_power_product))))))))
  132. 0132specialize pow_exists a
  133. 0133specialize pow_exists h
  134. 0134exact pow_exists
  135. 0135cases hmultiplier_power_exists
  136. 0136have hcancelled : exists gle_left_lemma_endpoint_local_result gle_right_lemma_endpoint_local_result. x16 + p * gle_left_lemma_endpoint_local_result = x12 + p * gle_right_lemma_endpoint_local_result
  137. 0137specialize gauss_signed_products_cancel_mod p
  138. 0138specialize gauss_signed_products_cancel_mod h
  139. 0139specialize gauss_signed_products_cancel_mod (2 * h)
  140. 0140specialize gauss_signed_products_cancel_mod a
  141. 0141specialize gauss_signed_products_cancel_mod b
  142. 0142specialize gauss_signed_products_cancel_mod c
  143. 0143specialize gauss_signed_products_cancel_mod x
  144. 0144specialize gauss_signed_products_cancel_mod x1
  145. 0145specialize gauss_signed_products_cancel_mod x5
  146. 0146specialize gauss_signed_products_cancel_mod x6
  147. 0147specialize gauss_signed_products_cancel_mod x2
  148. 0148specialize gauss_signed_products_cancel_mod x3
  149. 0149specialize gauss_signed_products_cancel_mod x9
  150. 0150specialize gauss_signed_products_cancel_mod x10
  151. 0151specialize gauss_signed_products_cancel_mod x13
  152. 0152specialize gauss_signed_products_cancel_mod x14
  153. 0153specialize gauss_signed_products_cancel_mod x4
  154. 0154specialize gauss_signed_products_cancel_mod x7
  155. 0155specialize gauss_signed_products_cancel_mod x8
  156. 0156specialize gauss_signed_products_cancel_mod x11
  157. 0157specialize gauss_signed_products_cancel_mod x15
  158. 0158specialize gauss_signed_products_cancel_mod x16
  159. 0159specialize gauss_signed_products_cancel_mod x12
  160. 0160apply gauss_signed_products_cancel_mod
  161. 0161exact hprime
  162. 0162exact hpsucc
  163. 0163refl
  164. 0164exact hsigned_exists_witness_witness_witness_witness
  165. 0165exact hsign_package_witness_witness_witness_witness_left
  166. 0166exact hpointwise_package_witness_witness_witness_left
  167. 0167exact hmagnitude_range
  168. 0168exact hmagnitude_injective
  169. 0169exact hrecode_exists_witness_witness
  170. 0170exact hhalf
  171. 0171exact hcount_exists_witness
  172. 0172exact hcanonical_product_exists_witness
  173. 0173exact hmagnitude_product_exists_witness
  174. 0174exact hsign_package_witness_witness_witness_witness_right_left
  175. 0175exact hpointwise_package_witness_witness_witness_right_left
  176. 0176exact hmultiplier_power_exists_witness
  177. 0177exact hsign_package_witness_witness_witness_witness_right_right_left
  178. 0178exists x4
  179. 0179exists x16
  180. 0180exists x12
  181. 0181split
  182. 0182exact hmultiplier_power_exists_witness
  183. 0183split
  184. 0184exact hsign_package_witness_witness_witness_witness_right_right_left
  185. 0185split
  186. 0186exists x
  187. 0187exists x1
  188. 0188exists x2
  189. 0189exists x3
  190. 0190split
  191. 0191exact hsigned_exists_witness_witness_witness_witness
  192. 0192exact hcount_exists_witness
  193. 0193exact hcancelled