LU001K

lucas_prime_digit_nonzero_quotient_strict

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

For a prime base every nonzero successive digit quotient is strictly below its predecessor natural.

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 n q d. ((~(p = 1) /\ forall frm_prime_left_lmd_strict_prime frm_prime_right_lmd_strict_prime. p = frm_prime_left_lmd_strict_prime * frm_prime_right_lmd_strict_prime -> frm_prime_left_lmd_strict_prime = 1 \/ frm_prime_right_lmd_strict_prime = 1)) -> ~(q = 0) -> n = p * q + d -> (exists lmd_gap_strict_result. lmd_gap_strict_result + S (q) = (n))

Constructive proof overview

Generated structural guide

For a prime base every nonzero successive digit quotient is strictly below its predecessor natural.

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

prime_two_le Alpha theorem; checked-use authorized succ_le_mul_of_two_le_right Alpha theorem; checked-use authorized le_add_right Stable theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized le_trans Stable theorem; checked-use authorized

Direct dependents

LU001L lucas_prime_digit_chain_nonzero_index_bound

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

34 script commands · 6 reading checkpoints · 4 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–7

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro q
  4. L4
    intro d
  5. L5
    intro hprime
  6. L6
    intro hnonzero
  7. L7
    intro hdivision
02Establish htwoL8–11

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime two le.

  1. L8
    have htwo : exists gap. gap + 2 = p
  2. L9
    specialize prime_two_le p
  3. L10
    apply prime_two_le
  4. L11
    exact hprime
03Establish hscaledL12–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply succ le mul of two le right.

  1. L12
    have hscaled : exists gap. gap + S q = q * p
  2. L13
    specialize succ_le_mul_of_two_le_right q
  3. L14
    specialize succ_le_mul_of_two_le_right p
  4. L15
    apply succ_le_mul_of_two_le_right
  5. L16
    exact hnonzero
  6. L17
    exact htwo
04Establish horderedL18–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul comm.

  1. L18
    have hordered : n = q * p + d
  2. L19
    trans p * q + d
  3. L20
    exact hdivision
  4. L21
    congr
  5. L22
    apply mul_comm
  6. L23
    refl
05Establish hupperL24–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le trans.

  1. L24
    have hupper : exists gap. gap + (q * p) = n
  2. L25
    specialize le_add_right (q * p)
  3. L26
    specialize le_add_right d
  4. L27
    rewrite <- hordered at le_add_right
  5. L28
    exact le_add_right
  6. L29
    specialize le_trans (S q)
  7. L30
    specialize le_trans (q * p)
  8. L31
    specialize le_trans n
  9. L32
    apply le_trans
  10. L33
    exact hscaled
06Use earlier factsL34–34

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

  1. L34
    exact hupper

Library-wide reading audit

Original exact command ledger · 34 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro q
  4. 0004intro d
  5. 0005intro hprime
  6. 0006intro hnonzero
  7. 0007intro hdivision
  8. 0008have htwo : exists gap. gap + 2 = p
  9. 0009specialize prime_two_le p
  10. 0010apply prime_two_le
  11. 0011exact hprime
  12. 0012have hscaled : exists gap. gap + S q = q * p
  13. 0013specialize succ_le_mul_of_two_le_right q
  14. 0014specialize succ_le_mul_of_two_le_right p
  15. 0015apply succ_le_mul_of_two_le_right
  16. 0016exact hnonzero
  17. 0017exact htwo
  18. 0018have hordered : n = q * p + d
  19. 0019trans p * q + d
  20. 0020exact hdivision
  21. 0021congr
  22. 0022apply mul_comm
  23. 0023refl
  24. 0024have hupper : exists gap. gap + (q * p) = n
  25. 0025specialize le_add_right (q * p)
  26. 0026specialize le_add_right d
  27. 0027rewrite <- hordered at le_add_right
  28. 0028exact le_add_right
  29. 0029specialize le_trans (S q)
  30. 0030specialize le_trans (q * p)
  31. 0031specialize le_trans n
  32. 0032apply le_trans
  33. 0033exact hscaled
  34. 0034exact hupper