LU0001 · theorem body

lucas_prime_row_interior_divisible

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

Every interior coefficient in prime Pascal row p is divisible by p.

historical independently replay-verified empty-context experiment; the experiment itself persisted no certificate and granted no release authority; current checked use follows separately sealed proof bundles; no Stable promotion.

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. ∀ j. ∀ C. Prime(p) → k + j = p → Lt(k,p) → Lt(j,p) → Choose(p,k,C) → Dvd(p,C)

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 PD0003 Dvd PD0004 Prime PD0041 Choose

In local proof propositions

none
Exact expanded first-order statement
forall p k j C. ((~(p = 1) /\ forall frm_prime_left_lucas_row_prime frm_prime_right_lucas_row_prime. p = frm_prime_left_lucas_row_prime * frm_prime_right_lucas_row_prime -> frm_prime_left_lucas_row_prime = 1 \/ frm_prime_right_lucas_row_prime = 1)) -> k + j = p -> (exists ldc_lt_row_left. ldc_lt_row_left + S (k) = p) -> (exists ldc_lt_row_right. ldc_lt_row_right + S (j) = p) -> (((exists bcf_lt_gap_lucas_row_choose_out_of_range. bcf_lt_gap_lucas_row_choose_out_of_range + S (p) = k) /\ C = 0) \/ ((exists bcf_le_gap_lucas_row_choose_in_range. bcf_le_gap_lucas_row_choose_in_range + (k) = p) /\ (exists bcf_row_code_code_lucas_row_choose bcf_row_code_scale_lucas_row_choose bcf_row_scale_code_lucas_row_choose bcf_row_scale_scale_lucas_row_choose bcf_row_code_lucas_row_choose bcf_row_scale_lucas_row_choose. ((forall bcf_row_index_lucas_row_choose_table. (exists bcf_lt_gap_lucas_row_choose_table_row_bound. bcf_lt_gap_lucas_row_choose_table_row_bound + S (bcf_row_index_lucas_row_choose_table) = S (p)) -> exists bcf_row_code_lucas_row_choose_table bcf_row_scale_lucas_row_choose_table. ((((exists bcf_height_lucas_row_choose_table_decoded_row_code. bcf_height_lucas_row_choose_table_decoded_row_code + S (bcf_row_code_lucas_row_choose_table) = S ((S (bcf_row_index_lucas_row_choose_table)) * bcf_row_code_scale_lucas_row_choose)) /\ exists bcf_quotient_lucas_row_choose_table_decoded_row_code. bcf_row_code_code_lucas_row_choose = bcf_quotient_lucas_row_choose_table_decoded_row_code * S ((S (bcf_row_index_lucas_row_choose_table)) * bcf_row_code_scale_lucas_row_choose) + (bcf_row_code_lucas_row_choose_table))) /\ ((((exists bcf_height_lucas_row_choose_table_decoded_row_scale. bcf_height_lucas_row_choose_table_decoded_row_scale + S (bcf_row_scale_lucas_row_choose_table) = S ((S (bcf_row_index_lucas_row_choose_table)) * bcf_row_scale_scale_lucas_row_choose)) /\ exists bcf_quotient_lucas_row_choose_table_decoded_row_scale. bcf_row_scale_code_lucas_row_choose = bcf_quotient_lucas_row_choose_table_decoded_row_scale * S ((S (bcf_row_index_lucas_row_choose_table)) * bcf_row_scale_scale_lucas_row_choose) + (bcf_row_scale_lucas_row_choose_table))) /\ ((bcf_row_index_lucas_row_choose_table = 0 /\ (forall bcf_index_lucas_row_choose_table_zero_row. (exists bcf_lt_gap_lucas_row_choose_table_zero_row_bound. bcf_lt_gap_lucas_row_choose_table_zero_row_bound + S (bcf_index_lucas_row_choose_table_zero_row) = S (p)) -> exists bcf_value_lucas_row_choose_table_zero_row. ((((exists bcf_height_lucas_row_choose_table_zero_row_entry. bcf_height_lucas_row_choose_table_zero_row_entry + S (bcf_value_lucas_row_choose_table_zero_row) = S ((S (bcf_index_lucas_row_choose_table_zero_row)) * bcf_row_scale_lucas_row_choose_table)) /\ exists bcf_quotient_lucas_row_choose_table_zero_row_entry. bcf_row_code_lucas_row_choose_table = bcf_quotient_lucas_row_choose_table_zero_row_entry * S ((S (bcf_index_lucas_row_choose_table_zero_row)) * bcf_row_scale_lucas_row_choose_table) + (bcf_value_lucas_row_choose_table_zero_row))) /\ ((bcf_index_lucas_row_choose_table_zero_row = 0 /\ bcf_value_lucas_row_choose_table_zero_row = 1) \/ exists bcf_predecessor_lucas_row_choose_table_zero_row. bcf_index_lucas_row_choose_table_zero_row = S bcf_predecessor_lucas_row_choose_table_zero_row /\ bcf_value_lucas_row_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_row_choose_table bcf_previous_code_lucas_row_choose_table bcf_previous_scale_lucas_row_choose_table. bcf_row_index_lucas_row_choose_table = S bcf_predecessor_lucas_row_choose_table /\ ((((exists bcf_height_lucas_row_choose_table_decoded_previous_code. bcf_height_lucas_row_choose_table_decoded_previous_code + S (bcf_previous_code_lucas_row_choose_table) = S ((S (bcf_predecessor_lucas_row_choose_table)) * bcf_row_code_scale_lucas_row_choose)) /\ exists bcf_quotient_lucas_row_choose_table_decoded_previous_code. bcf_row_code_code_lucas_row_choose = bcf_quotient_lucas_row_choose_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_row_choose_table)) * bcf_row_code_scale_lucas_row_choose) + (bcf_previous_code_lucas_row_choose_table))) /\ ((((exists bcf_height_lucas_row_choose_table_decoded_previous_scale. bcf_height_lucas_row_choose_table_decoded_previous_scale + S (bcf_previous_scale_lucas_row_choose_table) = S ((S (bcf_predecessor_lucas_row_choose_table)) * bcf_row_scale_scale_lucas_row_choose)) /\ exists bcf_quotient_lucas_row_choose_table_decoded_previous_scale. bcf_row_scale_code_lucas_row_choose = bcf_quotient_lucas_row_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_row_choose_table)) * bcf_row_scale_scale_lucas_row_choose) + (bcf_previous_scale_lucas_row_choose_table))) /\ (forall bcf_index_lucas_row_choose_table_row_step. (exists bcf_lt_gap_lucas_row_choose_table_row_step_bound. bcf_lt_gap_lucas_row_choose_table_row_step_bound + S (bcf_index_lucas_row_choose_table_row_step) = S (p)) -> exists bcf_value_lucas_row_choose_table_row_step. ((((exists bcf_height_lucas_row_choose_table_row_step_entry. bcf_height_lucas_row_choose_table_row_step_entry + S (bcf_value_lucas_row_choose_table_row_step) = S ((S (bcf_index_lucas_row_choose_table_row_step)) * bcf_row_scale_lucas_row_choose_table)) /\ exists bcf_quotient_lucas_row_choose_table_row_step_entry. bcf_row_code_lucas_row_choose_table = bcf_quotient_lucas_row_choose_table_row_step_entry * S ((S (bcf_index_lucas_row_choose_table_row_step)) * bcf_row_scale_lucas_row_choose_table) + (bcf_value_lucas_row_choose_table_row_step))) /\ ((bcf_index_lucas_row_choose_table_row_step = 0 /\ bcf_value_lucas_row_choose_table_row_step = 1) \/ exists bcf_predecessor_lucas_row_choose_table_row_step bcf_left_lucas_row_choose_table_row_step bcf_right_lucas_row_choose_table_row_step. bcf_index_lucas_row_choose_table_row_step = S bcf_predecessor_lucas_row_choose_table_row_step /\ ((((exists bcf_height_lucas_row_choose_table_row_step_previous_left. bcf_height_lucas_row_choose_table_row_step_previous_left + S (bcf_left_lucas_row_choose_table_row_step) = S ((S (bcf_predecessor_lucas_row_choose_table_row_step)) * bcf_previous_scale_lucas_row_choose_table)) /\ exists bcf_quotient_lucas_row_choose_table_row_step_previous_left. bcf_previous_code_lucas_row_choose_table = bcf_quotient_lucas_row_choose_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_row_choose_table_row_step)) * bcf_previous_scale_lucas_row_choose_table) + (bcf_left_lucas_row_choose_table_row_step))) /\ ((((exists bcf_height_lucas_row_choose_table_row_step_previous_right. bcf_height_lucas_row_choose_table_row_step_previous_right + S (bcf_right_lucas_row_choose_table_row_step) = S ((S (S (bcf_predecessor_lucas_row_choose_table_row_step))) * bcf_previous_scale_lucas_row_choose_table)) /\ exists bcf_quotient_lucas_row_choose_table_row_step_previous_right. bcf_previous_code_lucas_row_choose_table = bcf_quotient_lucas_row_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_row_choose_table_row_step))) * bcf_previous_scale_lucas_row_choose_table) + (bcf_right_lucas_row_choose_table_row_step))) /\ bcf_value_lucas_row_choose_table_row_step = bcf_left_lucas_row_choose_table_row_step + bcf_right_lucas_row_choose_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_row_choose_decoded_row_code. bcf_height_lucas_row_choose_decoded_row_code + S (bcf_row_code_lucas_row_choose) = S ((S (p)) * bcf_row_code_scale_lucas_row_choose)) /\ exists bcf_quotient_lucas_row_choose_decoded_row_code. bcf_row_code_code_lucas_row_choose = bcf_quotient_lucas_row_choose_decoded_row_code * S ((S (p)) * bcf_row_code_scale_lucas_row_choose) + (bcf_row_code_lucas_row_choose))) /\ ((((exists bcf_height_lucas_row_choose_decoded_row_scale. bcf_height_lucas_row_choose_decoded_row_scale + S (bcf_row_scale_lucas_row_choose) = S ((S (p)) * bcf_row_scale_scale_lucas_row_choose)) /\ exists bcf_quotient_lucas_row_choose_decoded_row_scale. bcf_row_scale_code_lucas_row_choose = bcf_quotient_lucas_row_choose_decoded_row_scale * S ((S (p)) * bcf_row_scale_scale_lucas_row_choose) + (bcf_row_scale_lucas_row_choose))) /\ (((exists bcf_height_lucas_row_choose_decoded_value. bcf_height_lucas_row_choose_decoded_value + S (C) = S ((S (k)) * bcf_row_scale_lucas_row_choose)) /\ exists bcf_quotient_lucas_row_choose_decoded_value. bcf_row_code_lucas_row_choose = bcf_quotient_lucas_row_choose_decoded_value * S ((S (k)) * bcf_row_scale_lucas_row_choose) + (C))))))))) -> (exists ldc_quotient_row. C = p * ldc_quotient_row)

Proof neighborhood

Direct theorem prerequisites

choose_prime_divides_between · Alpha closed le_refl · Stable closed

Direct theorem dependents

LU000I lucas_prime_row_sparse_complete LU000T lucas_prime_row_interior_zero_mod

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

22 script commands · 3 reading checkpoints · 0 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.

01Fix variables and assumptionsL1–9

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

  1. L1
    intro p
  2. L2
    intro k
  3. L3
    intro j
  4. L4
    intro C
  5. L5
    intro hp
  6. L6
    intro hsum
  7. L7
    intro hk
  8. L8
    intro hj
  9. L9
    intro hchoose
02Use earlier factsL10–19

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

  1. L10
    specialize choose_prime_divides_between p
  2. L11
    specialize choose_prime_divides_between k
  3. L12
    specialize choose_prime_divides_between j
  4. L13
    specialize choose_prime_divides_between p
  5. L14
    specialize choose_prime_divides_between C
  6. L15
    apply choose_prime_divides_between
  7. L16
    exact hsum
  8. L17
    exact hp
  9. L18
    exact hk
  10. L19
    exact hj
03Use earlier factsL20–22

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

  1. L20
    specialize le_refl p
  2. L21
    exact le_refl
  3. L22
    exact hchoose

Library-wide reading audit

Original defined command ledger · 22 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro j
  4. 0004intro C
  5. 0005intro hp
  6. 0006intro hsum
  7. 0007intro hk
  8. 0008intro hj
  9. 0009intro hchoose
  10. 0010specialize choose_prime_divides_between p
  11. 0011specialize choose_prime_divides_between k
  12. 0012specialize choose_prime_divides_between j
  13. 0013specialize choose_prime_divides_between p
  14. 0014specialize choose_prime_divides_between C
  15. 0015apply choose_prime_divides_between
  16. 0016exact hsum
  17. 0017exact hp
  18. 0018exact hk
  19. 0019exact hj
  20. 0020specialize le_refl p
  21. 0021exact le_refl
  22. 0022exact hchoose