LU0004 · theorem body

lucas_digit_no_carry_iff_not_divides

dependency-curried kernel-checked candidate body; not enrolled in Alpha or Stable

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.

Statement with defined notation

∀ p. ∀ a. ∀ b. ∀ C. Prime(p) → Lt(a,p) → Lt(b,p) → Choose(a + b,a,C) → (Lt(a + b,p) → ¬Dvd(p,C)) ∧ (¬Dvd(p,C) → Lt(a + b,p))

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

PD0001 Le PD0003 Dvd
Exact expanded first-order 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))))

Proof neighborhood

Direct theorem prerequisites

LU0003 lucas_digit_carry_iff_prime_divides lt_not_le · Stable closed le_or_lt · Stable closed

Direct theorem dependents

none

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

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.

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 (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 : (Le(p,a + b) → Dvd(p,C)) ∧ (Dvd(p,C) → Le(p,a + b))Definitions: Le(p,a + b)Dvd(p,C)Original native command in the exact edition
  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 defined 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 : (Le(p,a + b) → Dvd(p,C)) ∧ (Dvd(p,C) → Le(p,a + b))
    Exact native replay linehave 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