LU000T · theorem body

lucas_prime_row_interior_zero_mod

Alpha v34 checked-use · independently kernel and Lean verified; 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.

Statement with defined notation

∀ p. ∀ k. ∀ C. Prime(p) → ¬k = 0 → Lt(k,p) → Choose(p,k,C) → ModEq(p,C,0)

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0004 Prime PD0008 ModEq PD0041 Choose

In local proof propositions

PD0002 Lt
Exact expanded first-order 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)

Proof neighborhood

Direct theorem prerequisites

LU000S lucas_positive_digit_has_bounded_complement LU0001 lucas_prime_row_interior_divisible LU000R lucas_divisible_implies_zero_mod

Direct theorem dependents

LU000W lucas_prime_shift_below_base

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (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 : ∃ j. k + j = p ∧ Lt(j,p)Definitions: Lt(j,p)Original native command in the exact edition
  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 defined 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 : ∃ j. k + j = p ∧ Lt(j,p)
    Exact native replay linehave 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