PA00DK

distinct_odd_prime_half_row_count_prefix_exists_bounded

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

Every bounded initial set of rows has a semantic count prefix.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded PA statement

forall p q h k l. p = 2 * h + 1 -> q = 2 * k + 1 -> ((~(p = 1) /\ forall frp_prime_left_rectangle_count_prime_p frp_prime_right_rectangle_count_prime_p. p = frp_prime_left_rectangle_count_prime_p * frp_prime_right_rectangle_count_prime_p -> frp_prime_left_rectangle_count_prime_p = 1 \/ frp_prime_right_rectangle_count_prime_p = 1)) -> ((~(q = 1) /\ forall frp_prime_left_rectangle_count_prime_q frp_prime_right_rectangle_count_prime_q. q = frp_prime_left_rectangle_count_prime_q * frp_prime_right_rectangle_count_prime_q -> frp_prime_left_rectangle_count_prime_q = 1 \/ frp_prime_right_rectangle_count_prime_q = 1)) -> ~(p = q) -> (exists erc_le_gap_rectangle_count_length_bound. erc_le_gap_rectangle_count_length_bound + (l) = h) -> (exists cb cc. (forall erc_row_rectangle_count_bounded_prefix. (exists erc_lt_gap_rectangle_count_bounded_prefix_bound. erc_lt_gap_rectangle_count_bounded_prefix_bound + S (erc_row_rectangle_count_bounded_prefix) = l) -> exists erc_count_rectangle_count_bounded_prefix. ((((exists ff_h_erc_rectangle_count_bounded_prefix_decoded. ff_h_erc_rectangle_count_bounded_prefix_decoded + S (erc_count_rectangle_count_bounded_prefix) = S ((S (erc_row_rectangle_count_bounded_prefix)) * cc)) /\ exists ff_q_erc_rectangle_count_bounded_prefix_decoded. cb = ff_q_erc_rectangle_count_bounded_prefix_decoded * S ((S (erc_row_rectangle_count_bounded_prefix)) * cc) + (erc_count_rectangle_count_bounded_prefix))) /\ (exists erc_row_code_rectangle_count_bounded_prefix_witness erc_row_scale_rectangle_count_bounded_prefix_witness. ((forall eri_column_erc_rectangle_count_bounded_prefix_witness_row. (exists eri_gap_erc_rectangle_count_bounded_prefix_witness_row_bound. eri_gap_erc_rectangle_count_bounded_prefix_witness_row_bound + S (eri_column_erc_rectangle_count_bounded_prefix_witness_row) = k) -> exists eri_bit_erc_rectangle_count_bounded_prefix_witness_row. ((((exists ff_h_eri_erc_rectangle_count_bounded_prefix_witness_row_decoded. ff_h_eri_erc_rectangle_count_bounded_prefix_witness_row_decoded + S (eri_bit_erc_rectangle_count_bounded_prefix_witness_row) = S ((S (eri_column_erc_rectangle_count_bounded_prefix_witness_row)) * erc_row_scale_rectangle_count_bounded_prefix_witness)) /\ exists ff_q_eri_erc_rectangle_count_bounded_prefix_witness_row_decoded. erc_row_code_rectangle_count_bounded_prefix_witness = ff_q_eri_erc_rectangle_count_bounded_prefix_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_bounded_prefix_witness_row)) * erc_row_scale_rectangle_count_bounded_prefix_witness) + (eri_bit_erc_rectangle_count_bounded_prefix_witness_row))) /\ (((eri_bit_erc_rectangle_count_bounded_prefix_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_bounded_prefix_witness_row_choice_left. eri_gap_erc_rectangle_count_bounded_prefix_witness_row_choice_left + S (q * S erc_row_rectangle_count_bounded_prefix) = p * S eri_column_erc_rectangle_count_bounded_prefix_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_bounded_prefix_witness_row_choice_right. eri_gap_erc_rectangle_count_bounded_prefix_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_bounded_prefix_witness_row) = q * S erc_row_rectangle_count_bounded_prefix))) \/ (eri_bit_erc_rectangle_count_bounded_prefix_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_bounded_prefix_witness_row_choice_right. eri_gap_erc_rectangle_count_bounded_prefix_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_bounded_prefix_witness_row) = q * S erc_row_rectangle_count_bounded_prefix) /\ ~(exists eri_gap_erc_rectangle_count_bounded_prefix_witness_row_choice_left. eri_gap_erc_rectangle_count_bounded_prefix_witness_row_choice_left + S (q * S erc_row_rectangle_count_bounded_prefix) = p * S eri_column_erc_rectangle_count_bounded_prefix_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_bounded_prefix_witness_count_sum ff_v_erc_rectangle_count_bounded_prefix_witness_count_sum. ((((exists ff_h_erc_rectangle_count_bounded_prefix_witness_count_sum_start. ff_h_erc_rectangle_count_bounded_prefix_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_bounded_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_bounded_prefix_witness_count_sum_start. ff_u_erc_rectangle_count_bounded_prefix_witness_count_sum = ff_q_erc_rectangle_count_bounded_prefix_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_bounded_prefix_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_bounded_prefix_witness_count_sum_terminal. ff_h_erc_rectangle_count_bounded_prefix_witness_count_sum_terminal + S (erc_count_rectangle_count_bounded_prefix) = S ((S (k)) * ff_v_erc_rectangle_count_bounded_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_bounded_prefix_witness_count_sum_terminal. ff_u_erc_rectangle_count_bounded_prefix_witness_count_sum = ff_q_erc_rectangle_count_bounded_prefix_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_bounded_prefix_witness_count_sum) + (erc_count_rectangle_count_bounded_prefix))) /\ forall ff_i_erc_rectangle_count_bounded_prefix_witness_count_sum. (exists ff_lt_erc_rectangle_count_bounded_prefix_witness_count_sum_bound. ff_lt_erc_rectangle_count_bounded_prefix_witness_count_sum_bound + S ff_i_erc_rectangle_count_bounded_prefix_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_bounded_prefix_witness_count_sum ff_r_erc_rectangle_count_bounded_prefix_witness_count_sum ff_s_erc_rectangle_count_bounded_prefix_witness_count_sum. ((((exists ff_h_erc_rectangle_count_bounded_prefix_witness_count_sum_summand. ff_h_erc_rectangle_count_bounded_prefix_witness_count_sum_summand + S (ff_a_erc_rectangle_count_bounded_prefix_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_bounded_prefix_witness_count_sum)) * erc_row_scale_rectangle_count_bounded_prefix_witness)) /\ exists ff_q_erc_rectangle_count_bounded_prefix_witness_count_sum_summand. erc_row_code_rectangle_count_bounded_prefix_witness = ff_q_erc_rectangle_count_bounded_prefix_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_bounded_prefix_witness_count_sum)) * erc_row_scale_rectangle_count_bounded_prefix_witness) + (ff_a_erc_rectangle_count_bounded_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_bounded_prefix_witness_count_sum_partial. ff_h_erc_rectangle_count_bounded_prefix_witness_count_sum_partial + S (ff_r_erc_rectangle_count_bounded_prefix_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_bounded_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_bounded_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_bounded_prefix_witness_count_sum_partial. ff_u_erc_rectangle_count_bounded_prefix_witness_count_sum = ff_q_erc_rectangle_count_bounded_prefix_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_bounded_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_bounded_prefix_witness_count_sum) + (ff_r_erc_rectangle_count_bounded_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_bounded_prefix_witness_count_sum_successor. ff_h_erc_rectangle_count_bounded_prefix_witness_count_sum_successor + S (ff_s_erc_rectangle_count_bounded_prefix_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_bounded_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_bounded_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_bounded_prefix_witness_count_sum_successor. ff_u_erc_rectangle_count_bounded_prefix_witness_count_sum = ff_q_erc_rectangle_count_bounded_prefix_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_bounded_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_bounded_prefix_witness_count_sum) + (ff_s_erc_rectangle_count_bounded_prefix_witness_count_sum))) /\ ff_s_erc_rectangle_count_bounded_prefix_witness_count_sum = ff_r_erc_rectangle_count_bounded_prefix_witness_count_sum + ff_a_erc_rectangle_count_bounded_prefix_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_bounded_prefix_witness_count_bits. (exists ff_lt_erc_rectangle_count_bounded_prefix_witness_count_bits_bound. ff_lt_erc_rectangle_count_bounded_prefix_witness_count_bits_bound + S ff_i_erc_rectangle_count_bounded_prefix_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_bounded_prefix_witness_count_bits. ((((exists ff_h_erc_rectangle_count_bounded_prefix_witness_count_bits_decoded. ff_h_erc_rectangle_count_bounded_prefix_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_bounded_prefix_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_bounded_prefix_witness_count_bits)) * erc_row_scale_rectangle_count_bounded_prefix_witness)) /\ exists ff_q_erc_rectangle_count_bounded_prefix_witness_count_bits_decoded. erc_row_code_rectangle_count_bounded_prefix_witness = ff_q_erc_rectangle_count_bounded_prefix_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_bounded_prefix_witness_count_bits)) * erc_row_scale_rectangle_count_bounded_prefix_witness) + (ff_bit_erc_rectangle_count_bounded_prefix_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_bounded_prefix_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_bounded_prefix_witness_count_bits = 1))))))))))

Structural proof guide

Generated structural guide

Every bounded initial set of rows has a semantic count prefix.

Use the direct prerequisites distinct_odd_prime_half_row_count_choices_bounded, eisenstein_rectangle_row_count_prefix_exists as previously established PA formulas.

The proof proceeds by intermediate claims (1).

Referenced ingredients

PA00DH distinct_odd_prime_half_row_count_choices_bounded PA00DJ eisenstein_rectangle_row_count_prefix_exists

Proof neighborhood

Direct dependencies

PA00DH distinct_odd_prime_half_row_count_choices_bounded PA00DJ eisenstein_rectangle_row_count_prefix_exists

Direct dependents

PA00DL distinct_odd_prime_half_row_count_prefix_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

30 script commands · 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)
distinct odd prime half row count choices boundedeisenstein rectangle row count prefix exists

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro h
  4. L4
    intro k
  5. L5
    intro l
  6. L6
    intro hpodd
  7. L7
    intro hqodd
  8. L8
    intro hp
  9. L9
    intro hq
  10. L10
    intro hpq
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hlh
03Establish hchoicesL12–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply distinct odd prime half row count choices bounded.

  1. L12
    have hchoices : ∀ erc_row_rectangle_count_bounded_choices. Lt(erc_row_rectangle_count_bounded_choices,l) → ∃ x. ∃ y. ∃ z. (∀ n. Lt(n,k) → ∃ m. BetaAt(y,z,n,m) ∧ (m = 0 ∧ (Lt(q · S erc_row_rectangle_count_bounded_choices,p · S n) ∧ ¬Lt(p · S n,q · S erc_row_rectangle_count_bounded_choices)) ∨ m = 1 ∧ (Lt(p · S n,q · S erc_row_rectangle_count_bounded_choices) ∧ ¬Lt(q · S erc_row_rectangle_count_bounded_choices,p · S n)))) ∧ BitCount(y,z,k,x)Definitions: LtBetaAtBitCount
  2. L13
    specialize distinct_odd_prime_half_row_count_choices_bounded p
  3. L14
    specialize distinct_odd_prime_half_row_count_choices_bounded q
  4. L15
    specialize distinct_odd_prime_half_row_count_choices_bounded h
  5. L16
    specialize distinct_odd_prime_half_row_count_choices_bounded k
  6. L17
    specialize distinct_odd_prime_half_row_count_choices_bounded l
  7. L18
    apply distinct_odd_prime_half_row_count_choices_bounded
  8. L19
    exact hpodd
  9. L20
    exact hqodd
  10. L21
    exact hp
04Use earlier factsL22–30

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

  1. L22
    exact hq
  2. L23
    exact hpq
  3. L24
    exact hlh
  4. L25
    specialize eisenstein_rectangle_row_count_prefix_exists p
  5. L26
    specialize eisenstein_rectangle_row_count_prefix_exists q
  6. L27
    specialize eisenstein_rectangle_row_count_prefix_exists k
  7. L28
    specialize eisenstein_rectangle_row_count_prefix_exists l
  8. L29
    apply eisenstein_rectangle_row_count_prefix_exists
  9. L30
    exact hchoices

Library-wide reading audit

Original exact command ledger · 30 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro h
  4. 0004intro k
  5. 0005intro l
  6. 0006intro hpodd
  7. 0007intro hqodd
  8. 0008intro hp
  9. 0009intro hq
  10. 0010intro hpq
  11. 0011intro hlh
  12. 0012have hchoices : forall erc_row_rectangle_count_bounded_choices. (exists erc_lt_gap_rectangle_count_bounded_choices_bound. erc_lt_gap_rectangle_count_bounded_choices_bound + S (erc_row_rectangle_count_bounded_choices) = l) -> exists erc_count_rectangle_count_bounded_choices. (exists erc_row_code_rectangle_count_bounded_choices_witness erc_row_scale_rectangle_count_bounded_choices_witness. ((forall eri_column_erc_rectangle_count_bounded_choices_witness_row. (exists eri_gap_erc_rectangle_count_bounded_choices_witness_row_bound. eri_gap_erc_rectangle_count_bounded_choices_witness_row_bound + S (eri_column_erc_rectangle_count_bounded_choices_witness_row) = k) -> exists eri_bit_erc_rectangle_count_bounded_choices_witness_row. ((((exists ff_h_eri_erc_rectangle_count_bounded_choices_witness_row_decoded. ff_h_eri_erc_rectangle_count_bounded_choices_witness_row_decoded + S (eri_bit_erc_rectangle_count_bounded_choices_witness_row) = S ((S (eri_column_erc_rectangle_count_bounded_choices_witness_row)) * erc_row_scale_rectangle_count_bounded_choices_witness)) /\ exists ff_q_eri_erc_rectangle_count_bounded_choices_witness_row_decoded. erc_row_code_rectangle_count_bounded_choices_witness = ff_q_eri_erc_rectangle_count_bounded_choices_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_bounded_choices_witness_row)) * erc_row_scale_rectangle_count_bounded_choices_witness) + (eri_bit_erc_rectangle_count_bounded_choices_witness_row))) /\ (((eri_bit_erc_rectangle_count_bounded_choices_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_bounded_choices_witness_row_choice_left. eri_gap_erc_rectangle_count_bounded_choices_witness_row_choice_left + S (q * S erc_row_rectangle_count_bounded_choices) = p * S eri_column_erc_rectangle_count_bounded_choices_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_bounded_choices_witness_row_choice_right. eri_gap_erc_rectangle_count_bounded_choices_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_bounded_choices_witness_row) = q * S erc_row_rectangle_count_bounded_choices))) \/ (eri_bit_erc_rectangle_count_bounded_choices_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_bounded_choices_witness_row_choice_right. eri_gap_erc_rectangle_count_bounded_choices_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_bounded_choices_witness_row) = q * S erc_row_rectangle_count_bounded_choices) /\ ~(exists eri_gap_erc_rectangle_count_bounded_choices_witness_row_choice_left. eri_gap_erc_rectangle_count_bounded_choices_witness_row_choice_left + S (q * S erc_row_rectangle_count_bounded_choices) = p * S eri_column_erc_rectangle_count_bounded_choices_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_bounded_choices_witness_count_sum ff_v_erc_rectangle_count_bounded_choices_witness_count_sum. ((((exists ff_h_erc_rectangle_count_bounded_choices_witness_count_sum_start. ff_h_erc_rectangle_count_bounded_choices_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_bounded_choices_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_bounded_choices_witness_count_sum_start. ff_u_erc_rectangle_count_bounded_choices_witness_count_sum = ff_q_erc_rectangle_count_bounded_choices_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_bounded_choices_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_bounded_choices_witness_count_sum_terminal. ff_h_erc_rectangle_count_bounded_choices_witness_count_sum_terminal + S (erc_count_rectangle_count_bounded_choices) = S ((S (k)) * ff_v_erc_rectangle_count_bounded_choices_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_bounded_choices_witness_count_sum_terminal. ff_u_erc_rectangle_count_bounded_choices_witness_count_sum = ff_q_erc_rectangle_count_bounded_choices_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_bounded_choices_witness_count_sum) + (erc_count_rectangle_count_bounded_choices))) /\ forall ff_i_erc_rectangle_count_bounded_choices_witness_count_sum. (exists ff_lt_erc_rectangle_count_bounded_choices_witness_count_sum_bound. ff_lt_erc_rectangle_count_bounded_choices_witness_count_sum_bound + S ff_i_erc_rectangle_count_bounded_choices_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_bounded_choices_witness_count_sum ff_r_erc_rectangle_count_bounded_choices_witness_count_sum ff_s_erc_rectangle_count_bounded_choices_witness_count_sum. ((((exists ff_h_erc_rectangle_count_bounded_choices_witness_count_sum_summand. ff_h_erc_rectangle_count_bounded_choices_witness_count_sum_summand + S (ff_a_erc_rectangle_count_bounded_choices_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_bounded_choices_witness_count_sum)) * erc_row_scale_rectangle_count_bounded_choices_witness)) /\ exists ff_q_erc_rectangle_count_bounded_choices_witness_count_sum_summand. erc_row_code_rectangle_count_bounded_choices_witness = ff_q_erc_rectangle_count_bounded_choices_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_bounded_choices_witness_count_sum)) * erc_row_scale_rectangle_count_bounded_choices_witness) + (ff_a_erc_rectangle_count_bounded_choices_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_bounded_choices_witness_count_sum_partial. ff_h_erc_rectangle_count_bounded_choices_witness_count_sum_partial + S (ff_r_erc_rectangle_count_bounded_choices_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_bounded_choices_witness_count_sum)) * ff_v_erc_rectangle_count_bounded_choices_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_bounded_choices_witness_count_sum_partial. ff_u_erc_rectangle_count_bounded_choices_witness_count_sum = ff_q_erc_rectangle_count_bounded_choices_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_bounded_choices_witness_count_sum)) * ff_v_erc_rectangle_count_bounded_choices_witness_count_sum) + (ff_r_erc_rectangle_count_bounded_choices_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_bounded_choices_witness_count_sum_successor. ff_h_erc_rectangle_count_bounded_choices_witness_count_sum_successor + S (ff_s_erc_rectangle_count_bounded_choices_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_bounded_choices_witness_count_sum)) * ff_v_erc_rectangle_count_bounded_choices_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_bounded_choices_witness_count_sum_successor. ff_u_erc_rectangle_count_bounded_choices_witness_count_sum = ff_q_erc_rectangle_count_bounded_choices_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_bounded_choices_witness_count_sum)) * ff_v_erc_rectangle_count_bounded_choices_witness_count_sum) + (ff_s_erc_rectangle_count_bounded_choices_witness_count_sum))) /\ ff_s_erc_rectangle_count_bounded_choices_witness_count_sum = ff_r_erc_rectangle_count_bounded_choices_witness_count_sum + ff_a_erc_rectangle_count_bounded_choices_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_bounded_choices_witness_count_bits. (exists ff_lt_erc_rectangle_count_bounded_choices_witness_count_bits_bound. ff_lt_erc_rectangle_count_bounded_choices_witness_count_bits_bound + S ff_i_erc_rectangle_count_bounded_choices_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_bounded_choices_witness_count_bits. ((((exists ff_h_erc_rectangle_count_bounded_choices_witness_count_bits_decoded. ff_h_erc_rectangle_count_bounded_choices_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_bounded_choices_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_bounded_choices_witness_count_bits)) * erc_row_scale_rectangle_count_bounded_choices_witness)) /\ exists ff_q_erc_rectangle_count_bounded_choices_witness_count_bits_decoded. erc_row_code_rectangle_count_bounded_choices_witness = ff_q_erc_rectangle_count_bounded_choices_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_bounded_choices_witness_count_bits)) * erc_row_scale_rectangle_count_bounded_choices_witness) + (ff_bit_erc_rectangle_count_bounded_choices_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_bounded_choices_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_bounded_choices_witness_count_bits = 1)))))))
  13. 0013specialize distinct_odd_prime_half_row_count_choices_bounded p
  14. 0014specialize distinct_odd_prime_half_row_count_choices_bounded q
  15. 0015specialize distinct_odd_prime_half_row_count_choices_bounded h
  16. 0016specialize distinct_odd_prime_half_row_count_choices_bounded k
  17. 0017specialize distinct_odd_prime_half_row_count_choices_bounded l
  18. 0018apply distinct_odd_prime_half_row_count_choices_bounded
  19. 0019exact hpodd
  20. 0020exact hqodd
  21. 0021exact hp
  22. 0022exact hq
  23. 0023exact hpq
  24. 0024exact hlh
  25. 0025specialize eisenstein_rectangle_row_count_prefix_exists p
  26. 0026specialize eisenstein_rectangle_row_count_prefix_exists q
  27. 0027specialize eisenstein_rectangle_row_count_prefix_exists k
  28. 0028specialize eisenstein_rectangle_row_count_prefix_exists l
  29. 0029apply eisenstein_rectangle_row_count_prefix_exists
  30. 0030exact hchoices