LU001K · theorem body

lucas_prime_digit_nonzero_quotient_strict

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

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

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. ∀ n. ∀ q. ∀ d. Prime(p) → ¬q = 0 → n = p · q + d → Lt(q,n)

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 PD0004 Prime

In local proof propositions

PD0001 Le PD0002 Lt
Exact expanded first-order 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))

Proof neighborhood

Direct theorem prerequisites

prime_two_le · Alpha closed succ_le_mul_of_two_le_right · Alpha closed le_add_right · Stable closed mul_comm · Stable closed le_trans · Stable closed

Direct theorem dependents

LU001L lucas_prime_digit_chain_nonzero_index_bound

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

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.

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–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
  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 : Lt(q,q · p)Definitions: Lt(q,q · p)Original native command in the exact edition
  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 : Le(q · p,n)Definitions: Le(q · p,n)Original native command in the exact edition
  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 defined 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 : Lt(1,p)
    Exact native replay linehave htwo : exists gap. gap + 2 = p
  9. 0009specialize prime_two_le p
  10. 0010apply prime_two_le
  11. 0011exact hprime
  12. 0012have hscaled : Lt(q,q · p)
    Exact native replay linehave 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 : Le(q · p,n)
    Exact native replay linehave 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