LU000T

lucas_prime_row_interior_zero_mod

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Every nonboundary coefficient of the prime Pascal row is constructively congruent to zero.

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 first-order arithmetic statement

forall p k C. ((~(p = 1) /\ forall frm_prime_left_lucas_convolution_prime frm_prime_right_lucas_convolution_prime. p = frm_prime_left_lucas_convolution_prime * frm_prime_right_lucas_convolution_prime -> frm_prime_left_lucas_convolution_prime = 1 \/ frm_prime_right_lucas_convolution_prime = 1)) -> ~(k = 0) -> (exists lcv_gap_interior_bound. lcv_gap_interior_bound + S (k) = (p)) -> (((exists bcf_lt_gap_lucas_convolution_interior_choose_out_of_range. bcf_lt_gap_lucas_convolution_interior_choose_out_of_range + S (p) = k) /\ C = 0) \/ ((exists bcf_le_gap_lucas_convolution_interior_choose_in_range. bcf_le_gap_lucas_convolution_interior_choose_in_range + (k) = p) /\ (exists bcf_row_code_code_lucas_convolution_interior_choose bcf_row_code_scale_lucas_convolution_interior_choose bcf_row_scale_code_lucas_convolution_interior_choose bcf_row_scale_scale_lucas_convolution_interior_choose bcf_row_code_lucas_convolution_interior_choose bcf_row_scale_lucas_convolution_interior_choose. ((forall bcf_row_index_lucas_convolution_interior_choose_table. (exists bcf_lt_gap_lucas_convolution_interior_choose_table_row_bound. bcf_lt_gap_lucas_convolution_interior_choose_table_row_bound + S (bcf_row_index_lucas_convolution_interior_choose_table) = S (p)) -> exists bcf_row_code_lucas_convolution_interior_choose_table bcf_row_scale_lucas_convolution_interior_choose_table. ((((exists bcf_height_lucas_convolution_interior_choose_table_decoded_row_code. bcf_height_lucas_convolution_interior_choose_table_decoded_row_code + S (bcf_row_code_lucas_convolution_interior_choose_table) = S ((S (bcf_row_index_lucas_convolution_interior_choose_table)) * bcf_row_code_scale_lucas_convolution_interior_choose)) /\ exists bcf_quotient_lucas_convolution_interior_choose_table_decoded_row_code. bcf_row_code_code_lucas_convolution_interior_choose = bcf_quotient_lucas_convolution_interior_choose_table_decoded_row_code * S ((S (bcf_row_index_lucas_convolution_interior_choose_table)) * bcf_row_code_scale_lucas_convolution_interior_choose) + (bcf_row_code_lucas_convolution_interior_choose_table))) /\ ((((exists bcf_height_lucas_convolution_interior_choose_table_decoded_row_scale. bcf_height_lucas_convolution_interior_choose_table_decoded_row_scale + S (bcf_row_scale_lucas_convolution_interior_choose_table) = S ((S (bcf_row_index_lucas_convolution_interior_choose_table)) * bcf_row_scale_scale_lucas_convolution_interior_choose)) /\ exists bcf_quotient_lucas_convolution_interior_choose_table_decoded_row_scale. bcf_row_scale_code_lucas_convolution_interior_choose = bcf_quotient_lucas_convolution_interior_choose_table_decoded_row_scale * S ((S (bcf_row_index_lucas_convolution_interior_choose_table)) * bcf_row_scale_scale_lucas_convolution_interior_choose) + (bcf_row_scale_lucas_convolution_interior_choose_table))) /\ ((bcf_row_index_lucas_convolution_interior_choose_table = 0 /\ (forall bcf_index_lucas_convolution_interior_choose_table_zero_row. (exists bcf_lt_gap_lucas_convolution_interior_choose_table_zero_row_bound. bcf_lt_gap_lucas_convolution_interior_choose_table_zero_row_bound + S (bcf_index_lucas_convolution_interior_choose_table_zero_row) = S (p)) -> exists bcf_value_lucas_convolution_interior_choose_table_zero_row. ((((exists bcf_height_lucas_convolution_interior_choose_table_zero_row_entry. bcf_height_lucas_convolution_interior_choose_table_zero_row_entry + S (bcf_value_lucas_convolution_interior_choose_table_zero_row) = S ((S (bcf_index_lucas_convolution_interior_choose_table_zero_row)) * bcf_row_scale_lucas_convolution_interior_choose_table)) /\ exists bcf_quotient_lucas_convolution_interior_choose_table_zero_row_entry. bcf_row_code_lucas_convolution_interior_choose_table = bcf_quotient_lucas_convolution_interior_choose_table_zero_row_entry * S ((S (bcf_index_lucas_convolution_interior_choose_table_zero_row)) * bcf_row_scale_lucas_convolution_interior_choose_table) + (bcf_value_lucas_convolution_interior_choose_table_zero_row))) /\ ((bcf_index_lucas_convolution_interior_choose_table_zero_row = 0 /\ bcf_value_lucas_convolution_interior_choose_table_zero_row = 1) \/ exists bcf_predecessor_lucas_convolution_interior_choose_table_zero_row. bcf_index_lucas_convolution_interior_choose_table_zero_row = S bcf_predecessor_lucas_convolution_interior_choose_table_zero_row /\ bcf_value_lucas_convolution_interior_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_convolution_interior_choose_table bcf_previous_code_lucas_convolution_interior_choose_table bcf_previous_scale_lucas_convolution_interior_choose_table. bcf_row_index_lucas_convolution_interior_choose_table = S bcf_predecessor_lucas_convolution_interior_choose_table /\ ((((exists bcf_height_lucas_convolution_interior_choose_table_decoded_previous_code. bcf_height_lucas_convolution_interior_choose_table_decoded_previous_code + S (bcf_previous_code_lucas_convolution_interior_choose_table) = S ((S (bcf_predecessor_lucas_convolution_interior_choose_table)) * bcf_row_code_scale_lucas_convolution_interior_choose)) /\ exists bcf_quotient_lucas_convolution_interior_choose_table_decoded_previous_code. bcf_row_code_code_lucas_convolution_interior_choose = bcf_quotient_lucas_convolution_interior_choose_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_convolution_interior_choose_table)) * bcf_row_code_scale_lucas_convolution_interior_choose) + (bcf_previous_code_lucas_convolution_interior_choose_table))) /\ ((((exists bcf_height_lucas_convolution_interior_choose_table_decoded_previous_scale. bcf_height_lucas_convolution_interior_choose_table_decoded_previous_scale + S (bcf_previous_scale_lucas_convolution_interior_choose_table) = S ((S (bcf_predecessor_lucas_convolution_interior_choose_table)) * bcf_row_scale_scale_lucas_convolution_interior_choose)) /\ exists bcf_quotient_lucas_convolution_interior_choose_table_decoded_previous_scale. bcf_row_scale_code_lucas_convolution_interior_choose = bcf_quotient_lucas_convolution_interior_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_convolution_interior_choose_table)) * bcf_row_scale_scale_lucas_convolution_interior_choose) + (bcf_previous_scale_lucas_convolution_interior_choose_table))) /\ (forall bcf_index_lucas_convolution_interior_choose_table_row_step. (exists bcf_lt_gap_lucas_convolution_interior_choose_table_row_step_bound. bcf_lt_gap_lucas_convolution_interior_choose_table_row_step_bound + S (bcf_index_lucas_convolution_interior_choose_table_row_step) = S (p)) -> exists bcf_value_lucas_convolution_interior_choose_table_row_step. ((((exists bcf_height_lucas_convolution_interior_choose_table_row_step_entry. bcf_height_lucas_convolution_interior_choose_table_row_step_entry + S (bcf_value_lucas_convolution_interior_choose_table_row_step) = S ((S (bcf_index_lucas_convolution_interior_choose_table_row_step)) * bcf_row_scale_lucas_convolution_interior_choose_table)) /\ exists bcf_quotient_lucas_convolution_interior_choose_table_row_step_entry. bcf_row_code_lucas_convolution_interior_choose_table = bcf_quotient_lucas_convolution_interior_choose_table_row_step_entry * S ((S (bcf_index_lucas_convolution_interior_choose_table_row_step)) * bcf_row_scale_lucas_convolution_interior_choose_table) + (bcf_value_lucas_convolution_interior_choose_table_row_step))) /\ ((bcf_index_lucas_convolution_interior_choose_table_row_step = 0 /\ bcf_value_lucas_convolution_interior_choose_table_row_step = 1) \/ exists bcf_predecessor_lucas_convolution_interior_choose_table_row_step bcf_left_lucas_convolution_interior_choose_table_row_step bcf_right_lucas_convolution_interior_choose_table_row_step. bcf_index_lucas_convolution_interior_choose_table_row_step = S bcf_predecessor_lucas_convolution_interior_choose_table_row_step /\ ((((exists bcf_height_lucas_convolution_interior_choose_table_row_step_previous_left. bcf_height_lucas_convolution_interior_choose_table_row_step_previous_left + S (bcf_left_lucas_convolution_interior_choose_table_row_step) = S ((S (bcf_predecessor_lucas_convolution_interior_choose_table_row_step)) * bcf_previous_scale_lucas_convolution_interior_choose_table)) /\ exists bcf_quotient_lucas_convolution_interior_choose_table_row_step_previous_left. bcf_previous_code_lucas_convolution_interior_choose_table = bcf_quotient_lucas_convolution_interior_choose_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_convolution_interior_choose_table_row_step)) * bcf_previous_scale_lucas_convolution_interior_choose_table) + (bcf_left_lucas_convolution_interior_choose_table_row_step))) /\ ((((exists bcf_height_lucas_convolution_interior_choose_table_row_step_previous_right. bcf_height_lucas_convolution_interior_choose_table_row_step_previous_right + S (bcf_right_lucas_convolution_interior_choose_table_row_step) = S ((S (S (bcf_predecessor_lucas_convolution_interior_choose_table_row_step))) * bcf_previous_scale_lucas_convolution_interior_choose_table)) /\ exists bcf_quotient_lucas_convolution_interior_choose_table_row_step_previous_right. bcf_previous_code_lucas_convolution_interior_choose_table = bcf_quotient_lucas_convolution_interior_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_convolution_interior_choose_table_row_step))) * bcf_previous_scale_lucas_convolution_interior_choose_table) + (bcf_right_lucas_convolution_interior_choose_table_row_step))) /\ bcf_value_lucas_convolution_interior_choose_table_row_step = bcf_left_lucas_convolution_interior_choose_table_row_step + bcf_right_lucas_convolution_interior_choose_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_convolution_interior_choose_decoded_row_code. bcf_height_lucas_convolution_interior_choose_decoded_row_code + S (bcf_row_code_lucas_convolution_interior_choose) = S ((S (p)) * bcf_row_code_scale_lucas_convolution_interior_choose)) /\ exists bcf_quotient_lucas_convolution_interior_choose_decoded_row_code. bcf_row_code_code_lucas_convolution_interior_choose = bcf_quotient_lucas_convolution_interior_choose_decoded_row_code * S ((S (p)) * bcf_row_code_scale_lucas_convolution_interior_choose) + (bcf_row_code_lucas_convolution_interior_choose))) /\ ((((exists bcf_height_lucas_convolution_interior_choose_decoded_row_scale. bcf_height_lucas_convolution_interior_choose_decoded_row_scale + S (bcf_row_scale_lucas_convolution_interior_choose) = S ((S (p)) * bcf_row_scale_scale_lucas_convolution_interior_choose)) /\ exists bcf_quotient_lucas_convolution_interior_choose_decoded_row_scale. bcf_row_scale_code_lucas_convolution_interior_choose = bcf_quotient_lucas_convolution_interior_choose_decoded_row_scale * S ((S (p)) * bcf_row_scale_scale_lucas_convolution_interior_choose) + (bcf_row_scale_lucas_convolution_interior_choose))) /\ (((exists bcf_height_lucas_convolution_interior_choose_decoded_value. bcf_height_lucas_convolution_interior_choose_decoded_value + S (C) = S ((S (k)) * bcf_row_scale_lucas_convolution_interior_choose)) /\ exists bcf_quotient_lucas_convolution_interior_choose_decoded_value. bcf_row_code_lucas_convolution_interior_choose = bcf_quotient_lucas_convolution_interior_choose_decoded_value * S ((S (k)) * bcf_row_scale_lucas_convolution_interior_choose) + (C))))))))) -> (exists lcv_left_interior_result lcv_right_interior_result. (C) + (p) * lcv_left_interior_result = (0) + (p) * lcv_right_interior_result)

Constructive proof overview

Generated structural guide

Every nonboundary coefficient of the prime Pascal row is constructively congruent to zero.

The unchanged tactic script uses 3 declared prerequisites and contains 28 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

LU000S lucas_positive_digit_has_bounded_complement LU0001 lucas_prime_row_interior_divisible LU000R lucas_divisible_implies_zero_mod

Direct dependents

LU000W lucas_prime_shift_below_base

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

28 script commands · 5 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 (3)
lucas positive digit has bounded complementlucas prime row interior divisiblelucas divisible implies zero mod
01Fix variables and assumptionsL1–7

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

  1. L1
    intro p
  2. L2
    intro k
  3. L3
    intro C
  4. L4
    intro hprime
  5. L5
    intro hnonzero
  6. L6
    intro hbound
  7. L7
    intro hchoose
02Establish hcomplementL8–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas positive digit has bounded complement.

  1. L8
    have hcomplement : exists j. ((k + j = p) /\ (exists lcv_gap_interior_complement. lcv_gap_interior_complement + S (j) = (p)))
  2. L9
    specialize lucas_positive_digit_has_bounded_complement p
  3. L10
    specialize lucas_positive_digit_has_bounded_complement k
  4. L11
    apply lucas_positive_digit_has_bounded_complement
  5. L12
    exact hnonzero
  6. L13
    exact hbound
03Separate the logical casesL14–15

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

  1. L14
    cases hcomplement
  2. L15
    cases hcomplement_witness
04Use earlier factsL16–25

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

  1. L16
    specialize lucas_divisible_implies_zero_mod p
  2. L17
    specialize lucas_divisible_implies_zero_mod C
  3. L18
    apply lucas_divisible_implies_zero_mod
  4. L19
    specialize lucas_prime_row_interior_divisible p
  5. L20
    specialize lucas_prime_row_interior_divisible k
  6. L21
    specialize lucas_prime_row_interior_divisible x
  7. L22
    specialize lucas_prime_row_interior_divisible C
  8. L23
    apply lucas_prime_row_interior_divisible
  9. L24
    exact hprime
  10. L25
    exact hcomplement_witness_left
05Use earlier factsL26–28

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

  1. L26
    exact hbound
  2. L27
    exact hcomplement_witness_right
  3. L28
    exact hchoose

Library-wide reading audit

Original exact command ledger · 28 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro C
  4. 0004intro hprime
  5. 0005intro hnonzero
  6. 0006intro hbound
  7. 0007intro hchoose
  8. 0008have hcomplement : exists j. ((k + j = p) /\ (exists lcv_gap_interior_complement. lcv_gap_interior_complement + S (j) = (p)))
  9. 0009specialize lucas_positive_digit_has_bounded_complement p
  10. 0010specialize lucas_positive_digit_has_bounded_complement k
  11. 0011apply lucas_positive_digit_has_bounded_complement
  12. 0012exact hnonzero
  13. 0013exact hbound
  14. 0014cases hcomplement
  15. 0015cases hcomplement_witness
  16. 0016specialize lucas_divisible_implies_zero_mod p
  17. 0017specialize lucas_divisible_implies_zero_mod C
  18. 0018apply lucas_divisible_implies_zero_mod
  19. 0019specialize lucas_prime_row_interior_divisible p
  20. 0020specialize lucas_prime_row_interior_divisible k
  21. 0021specialize lucas_prime_row_interior_divisible x
  22. 0022specialize lucas_prime_row_interior_divisible C
  23. 0023apply lucas_prime_row_interior_divisible
  24. 0024exact hprime
  25. 0025exact hcomplement_witness_left
  26. 0026exact hbound
  27. 0027exact hcomplement_witness_right
  28. 0028exact hchoose