LU000J

lucas_positive_lower_quotient_exceeds_upper_digit

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

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

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 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))

Constructive proof overview

Generated structural guide

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

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

one_le_of_ne_zero Stable theorem; checked-use authorized le_mul_of_one_le_right Alpha theorem; checked-use authorized le_add_right Stable theorem; checked-use authorized le_trans Stable theorem; checked-use authorized

Direct dependents

LU000K lucas_positive_lower_quotient_digit_coefficient_zero

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

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.

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
    have hone : exists h. h + 1 = r
  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 : exists h. h + p = p * r
  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 : exists h. h + S d = p * r
  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 : exists h. h + (p * r) = p * r + e
  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 exact 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 : 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 : 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 : 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 : 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