LU000J · theorem body

lucas_positive_lower_quotient_exceeds_upper_digit

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

A positive lower base quotient makes its full index strictly greater than every bounded upper digit.

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

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

In local proof propositions

PD0001 Le PD0002 Lt
Exact expanded first-order statement
forall p r d e. (exists lbd_gap_upper_digit. lbd_gap_upper_digit + S (d) = (p)) -> ~(r = 0) -> (exists lbd_gap_high_column. lbd_gap_high_column + S (d) = (p * r + e))

Proof neighborhood

Direct theorem prerequisites

one_le_of_ne_zero · Stable closed le_mul_of_one_le_right · Alpha closed le_add_right · Stable closed le_trans · Stable closed

Direct theorem dependents

LU000K lucas_positive_lower_quotient_digit_coefficient_zero

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

32 script commands · 5 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–6

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

  1. L1
    intro p
  2. L2
    intro r
  3. L3
    intro d
  4. L4
    intro e
  5. L5
    intro hdigit
  6. L6
    intro hpositive
02Establish honeL7–10

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

  1. L7
  2. L8
    specialize one_le_of_ne_zero r
  3. L9
    apply one_le_of_ne_zero
  4. L10
    exact hpositive
03Establish hscaledL11–15

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

  1. L11
    have hscaled : Le(p,p · r)Definitions: Le(p,p · r)Original native command in the exact edition
  2. L12
    specialize le_mul_of_one_le_right p
  3. L13
    specialize le_mul_of_one_le_right r
  4. L14
    apply le_mul_of_one_le_right
  5. L15
    exact hone
04Establish hprefixL16–22

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

  1. L16
    have hprefix : Lt(d,p · r)Definitions: Lt(d,p · r)Original native command in the exact edition
  2. L17
    specialize le_trans (S d)
  3. L18
    specialize le_trans p
  4. L19
    specialize le_trans (p * r)
  5. L20
    apply le_trans
  6. L21
    exact hdigit
  7. L22
    exact hscaled
05Establish htailL23–32

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

  1. L23
    have htail : Le(p · r,p · r + e)Definitions: Le(p · r,p · r + e)Original native command in the exact edition
  2. L24
    specialize le_add_right (p * r)
  3. L25
    specialize le_add_right e
  4. L26
    exact le_add_right
  5. L27
    specialize le_trans (S d)
  6. L28
    specialize le_trans (p * r)
  7. L29
    specialize le_trans (p * r + e)
  8. L30
    apply le_trans
  9. L31
    exact hprefix
  10. L32
    exact htail

Library-wide reading audit

Original defined command ledger · 32 lines
  1. 0001intro p
  2. 0002intro r
  3. 0003intro d
  4. 0004intro e
  5. 0005intro hdigit
  6. 0006intro hpositive
  7. 0007have hone : Lt(0,r)
    Exact native replay linehave hone : exists h. h + 1 = r
  8. 0008specialize one_le_of_ne_zero r
  9. 0009apply one_le_of_ne_zero
  10. 0010exact hpositive
  11. 0011have hscaled : Le(p,p · r)
    Exact native replay linehave hscaled : exists h. h + p = p * r
  12. 0012specialize le_mul_of_one_le_right p
  13. 0013specialize le_mul_of_one_le_right r
  14. 0014apply le_mul_of_one_le_right
  15. 0015exact hone
  16. 0016have hprefix : Lt(d,p · r)
    Exact native replay linehave hprefix : exists h. h + S d = p * r
  17. 0017specialize le_trans (S d)
  18. 0018specialize le_trans p
  19. 0019specialize le_trans (p * r)
  20. 0020apply le_trans
  21. 0021exact hdigit
  22. 0022exact hscaled
  23. 0023have htail : Le(p · r,p · r + e)
    Exact native replay linehave htail : exists h. h + (p * r) = p * r + e
  24. 0024specialize le_add_right (p * r)
  25. 0025specialize le_add_right e
  26. 0026exact le_add_right
  27. 0027specialize le_trans (S d)
  28. 0028specialize le_trans (p * r)
  29. 0029specialize le_trans (p * r + e)
  30. 0030apply le_trans
  31. 0031exact hprefix
  32. 0032exact htail