LU0001

lucas_prime_row_interior_divisible

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

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

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 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)

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 22 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

Historical empty-context replay experiment only; that experiment persisted no certificate and granted no release authority. Current checked use follows separately sealed, independently verified proof bundles; there is no Stable promotion.

Proof neighborhood

Direct dependencies

choose_prime_divides_between Alpha theorem; checked-use authorized le_refl Stable theorem; checked-use authorized

Direct dependents

LU000I lucas_prime_row_sparse_complete LU000T lucas_prime_row_interior_zero_mod

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

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.

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 exact 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