LU0004

lucas_digit_no_carry_iff_not_divides

Dependency-curried candidate body; not Alpha-enrolled; no checked-use authority

For two base-p digits, a carry-free sum is equivalent to constructive nondivisibility of their binomial coefficient.

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 a b C. ((~(p = 1) /\ forall frm_prime_left_lucas_digit_prime frm_prime_right_lucas_digit_prime. p = frm_prime_left_lucas_digit_prime * frm_prime_right_lucas_digit_prime -> frm_prime_left_lucas_digit_prime = 1 \/ frm_prime_right_lucas_digit_prime = 1)) -> (exists ldc_lt_left. ldc_lt_left + S (a) = p) -> (exists ldc_lt_right. ldc_lt_right + S (b) = p) -> (((exists bcf_lt_gap_lucas_digit_choose_out_of_range. bcf_lt_gap_lucas_digit_choose_out_of_range + S (a + b) = a) /\ C = 0) \/ ((exists bcf_le_gap_lucas_digit_choose_in_range. bcf_le_gap_lucas_digit_choose_in_range + (a) = a + b) /\ (exists bcf_row_code_code_lucas_digit_choose bcf_row_code_scale_lucas_digit_choose bcf_row_scale_code_lucas_digit_choose bcf_row_scale_scale_lucas_digit_choose bcf_row_code_lucas_digit_choose bcf_row_scale_lucas_digit_choose. ((forall bcf_row_index_lucas_digit_choose_table. (exists bcf_lt_gap_lucas_digit_choose_table_row_bound. bcf_lt_gap_lucas_digit_choose_table_row_bound + S (bcf_row_index_lucas_digit_choose_table) = S (a + b)) -> exists bcf_row_code_lucas_digit_choose_table bcf_row_scale_lucas_digit_choose_table. ((((exists bcf_height_lucas_digit_choose_table_decoded_row_code. bcf_height_lucas_digit_choose_table_decoded_row_code + S (bcf_row_code_lucas_digit_choose_table) = S ((S (bcf_row_index_lucas_digit_choose_table)) * bcf_row_code_scale_lucas_digit_choose)) /\ exists bcf_quotient_lucas_digit_choose_table_decoded_row_code. bcf_row_code_code_lucas_digit_choose = bcf_quotient_lucas_digit_choose_table_decoded_row_code * S ((S (bcf_row_index_lucas_digit_choose_table)) * bcf_row_code_scale_lucas_digit_choose) + (bcf_row_code_lucas_digit_choose_table))) /\ ((((exists bcf_height_lucas_digit_choose_table_decoded_row_scale. bcf_height_lucas_digit_choose_table_decoded_row_scale + S (bcf_row_scale_lucas_digit_choose_table) = S ((S (bcf_row_index_lucas_digit_choose_table)) * bcf_row_scale_scale_lucas_digit_choose)) /\ exists bcf_quotient_lucas_digit_choose_table_decoded_row_scale. bcf_row_scale_code_lucas_digit_choose = bcf_quotient_lucas_digit_choose_table_decoded_row_scale * S ((S (bcf_row_index_lucas_digit_choose_table)) * bcf_row_scale_scale_lucas_digit_choose) + (bcf_row_scale_lucas_digit_choose_table))) /\ ((bcf_row_index_lucas_digit_choose_table = 0 /\ (forall bcf_index_lucas_digit_choose_table_zero_row. (exists bcf_lt_gap_lucas_digit_choose_table_zero_row_bound. bcf_lt_gap_lucas_digit_choose_table_zero_row_bound + S (bcf_index_lucas_digit_choose_table_zero_row) = S (a + b)) -> exists bcf_value_lucas_digit_choose_table_zero_row. ((((exists bcf_height_lucas_digit_choose_table_zero_row_entry. bcf_height_lucas_digit_choose_table_zero_row_entry + S (bcf_value_lucas_digit_choose_table_zero_row) = S ((S (bcf_index_lucas_digit_choose_table_zero_row)) * bcf_row_scale_lucas_digit_choose_table)) /\ exists bcf_quotient_lucas_digit_choose_table_zero_row_entry. bcf_row_code_lucas_digit_choose_table = bcf_quotient_lucas_digit_choose_table_zero_row_entry * S ((S (bcf_index_lucas_digit_choose_table_zero_row)) * bcf_row_scale_lucas_digit_choose_table) + (bcf_value_lucas_digit_choose_table_zero_row))) /\ ((bcf_index_lucas_digit_choose_table_zero_row = 0 /\ bcf_value_lucas_digit_choose_table_zero_row = 1) \/ exists bcf_predecessor_lucas_digit_choose_table_zero_row. bcf_index_lucas_digit_choose_table_zero_row = S bcf_predecessor_lucas_digit_choose_table_zero_row /\ bcf_value_lucas_digit_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_digit_choose_table bcf_previous_code_lucas_digit_choose_table bcf_previous_scale_lucas_digit_choose_table. bcf_row_index_lucas_digit_choose_table = S bcf_predecessor_lucas_digit_choose_table /\ ((((exists bcf_height_lucas_digit_choose_table_decoded_previous_code. bcf_height_lucas_digit_choose_table_decoded_previous_code + S (bcf_previous_code_lucas_digit_choose_table) = S ((S (bcf_predecessor_lucas_digit_choose_table)) * bcf_row_code_scale_lucas_digit_choose)) /\ exists bcf_quotient_lucas_digit_choose_table_decoded_previous_code. bcf_row_code_code_lucas_digit_choose = bcf_quotient_lucas_digit_choose_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_digit_choose_table)) * bcf_row_code_scale_lucas_digit_choose) + (bcf_previous_code_lucas_digit_choose_table))) /\ ((((exists bcf_height_lucas_digit_choose_table_decoded_previous_scale. bcf_height_lucas_digit_choose_table_decoded_previous_scale + S (bcf_previous_scale_lucas_digit_choose_table) = S ((S (bcf_predecessor_lucas_digit_choose_table)) * bcf_row_scale_scale_lucas_digit_choose)) /\ exists bcf_quotient_lucas_digit_choose_table_decoded_previous_scale. bcf_row_scale_code_lucas_digit_choose = bcf_quotient_lucas_digit_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_digit_choose_table)) * bcf_row_scale_scale_lucas_digit_choose) + (bcf_previous_scale_lucas_digit_choose_table))) /\ (forall bcf_index_lucas_digit_choose_table_row_step. (exists bcf_lt_gap_lucas_digit_choose_table_row_step_bound. bcf_lt_gap_lucas_digit_choose_table_row_step_bound + S (bcf_index_lucas_digit_choose_table_row_step) = S (a + b)) -> exists bcf_value_lucas_digit_choose_table_row_step. ((((exists bcf_height_lucas_digit_choose_table_row_step_entry. bcf_height_lucas_digit_choose_table_row_step_entry + S (bcf_value_lucas_digit_choose_table_row_step) = S ((S (bcf_index_lucas_digit_choose_table_row_step)) * bcf_row_scale_lucas_digit_choose_table)) /\ exists bcf_quotient_lucas_digit_choose_table_row_step_entry. bcf_row_code_lucas_digit_choose_table = bcf_quotient_lucas_digit_choose_table_row_step_entry * S ((S (bcf_index_lucas_digit_choose_table_row_step)) * bcf_row_scale_lucas_digit_choose_table) + (bcf_value_lucas_digit_choose_table_row_step))) /\ ((bcf_index_lucas_digit_choose_table_row_step = 0 /\ bcf_value_lucas_digit_choose_table_row_step = 1) \/ exists bcf_predecessor_lucas_digit_choose_table_row_step bcf_left_lucas_digit_choose_table_row_step bcf_right_lucas_digit_choose_table_row_step. bcf_index_lucas_digit_choose_table_row_step = S bcf_predecessor_lucas_digit_choose_table_row_step /\ ((((exists bcf_height_lucas_digit_choose_table_row_step_previous_left. bcf_height_lucas_digit_choose_table_row_step_previous_left + S (bcf_left_lucas_digit_choose_table_row_step) = S ((S (bcf_predecessor_lucas_digit_choose_table_row_step)) * bcf_previous_scale_lucas_digit_choose_table)) /\ exists bcf_quotient_lucas_digit_choose_table_row_step_previous_left. bcf_previous_code_lucas_digit_choose_table = bcf_quotient_lucas_digit_choose_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_digit_choose_table_row_step)) * bcf_previous_scale_lucas_digit_choose_table) + (bcf_left_lucas_digit_choose_table_row_step))) /\ ((((exists bcf_height_lucas_digit_choose_table_row_step_previous_right. bcf_height_lucas_digit_choose_table_row_step_previous_right + S (bcf_right_lucas_digit_choose_table_row_step) = S ((S (S (bcf_predecessor_lucas_digit_choose_table_row_step))) * bcf_previous_scale_lucas_digit_choose_table)) /\ exists bcf_quotient_lucas_digit_choose_table_row_step_previous_right. bcf_previous_code_lucas_digit_choose_table = bcf_quotient_lucas_digit_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_digit_choose_table_row_step))) * bcf_previous_scale_lucas_digit_choose_table) + (bcf_right_lucas_digit_choose_table_row_step))) /\ bcf_value_lucas_digit_choose_table_row_step = bcf_left_lucas_digit_choose_table_row_step + bcf_right_lucas_digit_choose_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_digit_choose_decoded_row_code. bcf_height_lucas_digit_choose_decoded_row_code + S (bcf_row_code_lucas_digit_choose) = S ((S (a + b)) * bcf_row_code_scale_lucas_digit_choose)) /\ exists bcf_quotient_lucas_digit_choose_decoded_row_code. bcf_row_code_code_lucas_digit_choose = bcf_quotient_lucas_digit_choose_decoded_row_code * S ((S (a + b)) * bcf_row_code_scale_lucas_digit_choose) + (bcf_row_code_lucas_digit_choose))) /\ ((((exists bcf_height_lucas_digit_choose_decoded_row_scale. bcf_height_lucas_digit_choose_decoded_row_scale + S (bcf_row_scale_lucas_digit_choose) = S ((S (a + b)) * bcf_row_scale_scale_lucas_digit_choose)) /\ exists bcf_quotient_lucas_digit_choose_decoded_row_scale. bcf_row_scale_code_lucas_digit_choose = bcf_quotient_lucas_digit_choose_decoded_row_scale * S ((S (a + b)) * bcf_row_scale_scale_lucas_digit_choose) + (bcf_row_scale_lucas_digit_choose))) /\ (((exists bcf_height_lucas_digit_choose_decoded_value. bcf_height_lucas_digit_choose_decoded_value + S (C) = S ((S (a)) * bcf_row_scale_lucas_digit_choose)) /\ exists bcf_quotient_lucas_digit_choose_decoded_value. bcf_row_code_lucas_digit_choose = bcf_quotient_lucas_digit_choose_decoded_value * S ((S (a)) * bcf_row_scale_lucas_digit_choose) + (C))))))))) -> ((((exists ldc_lt_no_carry. ldc_lt_no_carry + S (a + b) = p) -> (~(exists ldc_quotient_digit. C = p * ldc_quotient_digit))) /\ ((~(exists ldc_quotient_digit. C = p * ldc_quotient_digit)) -> (exists ldc_lt_no_carry. ldc_lt_no_carry + S (a + b) = p))))

Constructive proof overview

Generated structural guide

For two base-p digits, a carry-free sum is equivalent to constructive nondivisibility of their binomial coefficient.

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

LU0003 lucas_digit_carry_iff_prime_divides lt_not_le Stable theorem; checked-use authorized le_or_lt Stable theorem; checked-use authorized

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This dependency-curried candidate body does not grant checked theorem use or Stable membership.

Read the argument

Proof checkpoints

37 script commands · 9 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 (1)
lucas digit carry iff prime divides
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro C
  5. L5
    intro hp
  6. L6
    intro ha
  7. L7
    intro hb
  8. L8
    intro hchoose
02Establish hclassificationL9–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas digit carry iff prime divides.

  1. L9
    have hclassification : (((exists ldc_le_carry. ldc_le_carry + (p) = a + b) -> (exists ldc_quotient_digit. C = p * ldc_quotient_digit)) /\ ((exists ldc_quotient_digit. C = p * ldc_quotient_digit) -> (exists ldc_le_carry. ldc_le_carry + (p) = a + b)))
  2. L10
    specialize lucas_digit_carry_iff_prime_divides p
  3. L11
    specialize lucas_digit_carry_iff_prime_divides a
  4. L12
    specialize lucas_digit_carry_iff_prime_divides b
  5. L13
    specialize lucas_digit_carry_iff_prime_divides C
  6. L14
    apply lucas_digit_carry_iff_prime_divides
  7. L15
    exact hp
  8. L16
    exact ha
  9. L17
    exact hb
  10. L18
    exact hchoose
03Separate the logical casesL19–20

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

  1. L19
    cases hclassification
  2. L20
    split
04Fix variables and assumptionsL21–22

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

  1. L21
    intro hnocarrry
  2. L22
    intro hdivides
05Use earlier factsL23–28

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

  1. L23
    specialize lt_not_le (a + b)
  2. L24
    specialize lt_not_le p
  3. L25
    apply lt_not_le
  4. L26
    exact hnocarrry
  5. L27
    apply hclassification_right
  6. L28
    exact hdivides
06Fix variables and assumptionsL29–29

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

  1. L29
    intro hnotdivides
07Use earlier factsL30–31

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

  1. L30
    specialize le_or_lt p
  2. L31
    specialize le_or_lt (a + b)
08Separate the logical casesL32–33

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

  1. L32
    cases le_or_lt
  2. L33
    exfalso
09Use earlier factsL34–37

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

  1. L34
    apply hnotdivides
  2. L35
    apply hclassification_left
  3. L36
    exact le_or_lt_left
  4. L37
    exact le_or_lt_right

Library-wide reading audit

Original exact command ledger · 37 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro b
  4. 0004intro C
  5. 0005intro hp
  6. 0006intro ha
  7. 0007intro hb
  8. 0008intro hchoose
  9. 0009have hclassification : (((exists ldc_le_carry. ldc_le_carry + (p) = a + b) -> (exists ldc_quotient_digit. C = p * ldc_quotient_digit)) /\ ((exists ldc_quotient_digit. C = p * ldc_quotient_digit) -> (exists ldc_le_carry. ldc_le_carry + (p) = a + b)))
  10. 0010specialize lucas_digit_carry_iff_prime_divides p
  11. 0011specialize lucas_digit_carry_iff_prime_divides a
  12. 0012specialize lucas_digit_carry_iff_prime_divides b
  13. 0013specialize lucas_digit_carry_iff_prime_divides C
  14. 0014apply lucas_digit_carry_iff_prime_divides
  15. 0015exact hp
  16. 0016exact ha
  17. 0017exact hb
  18. 0018exact hchoose
  19. 0019cases hclassification
  20. 0020split
  21. 0021intro hnocarrry
  22. 0022intro hdivides
  23. 0023specialize lt_not_le (a + b)
  24. 0024specialize lt_not_le p
  25. 0025apply lt_not_le
  26. 0026exact hnocarrry
  27. 0027apply hclassification_right
  28. 0028exact hdivides
  29. 0029intro hnotdivides
  30. 0030specialize le_or_lt p
  31. 0031specialize le_or_lt (a + b)
  32. 0032cases le_or_lt
  33. 0033exfalso
  34. 0034apply hnotdivides
  35. 0035apply hclassification_left
  36. 0036exact le_or_lt_left
  37. 0037exact le_or_lt_right