LU001L · theorem body

lucas_prime_digit_chain_nonzero_index_bound

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

Any nonzero quotient at chain position i obeys the constructive global bound q+i<=n.

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

∀ i. ∀ p. ∀ n. ∀ qb. ∀ qc. ∀ db. ∀ dc. ∀ l. ∀ q. Le(i,l) → Prime(p) → BetaAt(qb,qc,0,n) ∧ (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ m. BetaAt(qb,qc,x,y) ∧ (BetaAt(qb,qc,S x,z) ∧ (BetaAt(db,dc,x,m) ∧ DivRem(y,p,z,m)))) → BetaAt(qb,qc,i,q) → ¬q = 0 → Le(q + i,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

PD0001 Le PD0002 Lt PD0004 Prime PD0007 DivRem PD0013 BetaAt

In local proof propositions

PD0001 Le PD0002 Lt PD0007 DivRem PD0013 BetaAt
Exact expanded first-order statement
forall i p n qb qc db dc l q. (exists lmd_le_gap_index_domain. lmd_le_gap_index_domain + (i) = (l)) -> ((~(p = 1) /\ forall frm_prime_left_lmd_index_prime frm_prime_right_lmd_index_prime. p = frm_prime_left_lmd_index_prime * frm_prime_right_lmd_index_prime -> frm_prime_left_lmd_index_prime = 1 \/ frm_prime_right_lmd_index_prime = 1)) -> (((((exists ff_h_lmd_index_chain_initial. ff_h_lmd_index_chain_initial + S (n) = S ((S (0)) * qc)) /\ exists ff_q_lmd_index_chain_initial. qb = ff_q_lmd_index_chain_initial * S ((S (0)) * qc) + (n))) /\ forall lmd_index_index_chain. (exists lmd_gap_index_chain_index. lmd_gap_index_chain_index + S (lmd_index_index_chain) = (l)) -> exists lmd_current_index_chain lmd_successor_index_chain lmd_digit_index_chain. ((((exists ff_h_lmd_index_chain_current. ff_h_lmd_index_chain_current + S (lmd_current_index_chain) = S ((S (lmd_index_index_chain)) * qc)) /\ exists ff_q_lmd_index_chain_current. qb = ff_q_lmd_index_chain_current * S ((S (lmd_index_index_chain)) * qc) + (lmd_current_index_chain))) /\ ((((exists ff_h_lmd_index_chain_successor. ff_h_lmd_index_chain_successor + S (lmd_successor_index_chain) = S ((S (S lmd_index_index_chain)) * qc)) /\ exists ff_q_lmd_index_chain_successor. qb = ff_q_lmd_index_chain_successor * S ((S (S lmd_index_index_chain)) * qc) + (lmd_successor_index_chain))) /\ ((((exists ff_h_lmd_index_chain_digit. ff_h_lmd_index_chain_digit + S (lmd_digit_index_chain) = S ((S (lmd_index_index_chain)) * dc)) /\ exists ff_q_lmd_index_chain_digit. db = ff_q_lmd_index_chain_digit * S ((S (lmd_index_index_chain)) * dc) + (lmd_digit_index_chain))) /\ ((lmd_current_index_chain = (p) * (lmd_successor_index_chain) + (lmd_digit_index_chain)) /\ (exists lmd_gap_index_chain_digit_bound. lmd_gap_index_chain_digit_bound + S (lmd_digit_index_chain) = (p)))))))) -> (((exists ff_h_lmd_index_entry. ff_h_lmd_index_entry + S (q) = S ((S (i)) * qc)) /\ exists ff_q_lmd_index_entry. qb = ff_q_lmd_index_entry * S ((S (i)) * qc) + (q))) -> ~(q = 0) -> (exists lmd_le_gap_index_bound_result. lmd_le_gap_index_bound_result + (q + i) = (n))

Proof neighborhood

Direct theorem prerequisites

beta_at_unique · Stable closed zero_add · Stable closed le_succ_self · Stable closed le_trans · Stable closed LU001K lucas_prime_digit_nonzero_quotient_strict add_le_add_right · Stable closed add_succ_left · Stable closed

Direct theorem dependents

LU001M lucas_prime_digit_chain_terminal_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

133 script commands · 31 reading checkpoints · 10 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 prime digit nonzero quotient strict
01Fix variables and assumptionsL1–1

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

  1. L1
    intro i
02Induction on iL2–11

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction i
  2. L3
    intro p
  3. L4
    intro n
  4. L5
    intro qb
  5. L6
    intro qc
  6. L7
    intro db
  7. L8
    intro dc
  8. L9
    intro l
  9. L10
    intro q
  10. L11
    intro hdomain
03Fix variables and assumptionsL12–15

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

  1. L12
    intro hprime
  2. L13
    intro hchain
  3. L14
    intro hentry
  4. L15
    intro hnonzero
04Separate the logical casesL16–16

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L16
    cases hchain
05Establish hequalL17–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L17
    have hequal : n = q
  2. L18
    specialize beta_at_unique qb
  3. L19
    specialize beta_at_unique qc
  4. L20
    specialize beta_at_unique 0
  5. L21
    specialize beta_at_unique n
  6. L22
    specialize beta_at_unique q
  7. L23
    apply beta_at_unique
  8. L24
    exact hchain_left
  9. L25
    exact hentry
06Construct an explicit witnessL26–26

Supply the displayed value, then prove that it has the required property.

  1. L26
    exists 0
07Calculate and transport equalitiesL27–28

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L27
    trans q
  2. L28
    trans q + 0
08Use earlier factsL29–30

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

  1. L29
    apply zero_add
  2. L30
    apply PA3
09Calculate and transport equalitiesL31–31

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L31
    symm
10Use earlier factsL32–32

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

  1. L32
    exact hequal
11Fix variables and assumptionsL33–42

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

  1. L33
    intro p
  2. L34
    intro n
  3. L35
    intro qb
  4. L36
    intro qc
  5. L37
    intro db
  6. L38
    intro dc
  7. L39
    intro l
  8. L40
    intro q
  9. L41
    intro hdomain
  10. L42
    intro hprime
12Fix variables and assumptionsL43–45

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

  1. L43
    intro hchain
  2. L44
    intro hentry
  3. L45
    intro hnonzero
13Separate the logical casesL46–46

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L46
    cases hchain
14Establish hpreviousL47–50

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

  1. L47
    have hprevious : ∃ a. ∃ Q. ∃ d. BetaAt(qb,qc,i,a) ∧ (BetaAt(qb,qc,S i,Q) ∧ (BetaAt(db,dc,i,d) ∧ DivRem(a,p,Q,d)))Definitions: BetaAt(qb,qc,i,a)BetaAt(qb,qc,S i,Q)BetaAt(db,dc,i,d)DivRem(a,p,Q,d)Original native command in the exact edition
  2. L48
    specialize hchain_right i
  3. L49
    apply hchain_right
  4. L50
    exact hdomain
15Separate the logical casesL51–57

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L51
    cases hprevious
  2. L52
    cases hprevious_witness
  3. L53
    cases hprevious_witness_witness
  4. L54
    cases hprevious_witness_witness_witness
  5. L55
    cases hprevious_witness_witness_witness_right
  6. L56
    cases hprevious_witness_witness_witness_right_right
  7. L57
    cases hprevious_witness_witness_witness_right_right_right
16Establish hquotientL58–66

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L58
    have hquotient : x1 = q
  2. L59
    specialize beta_at_unique qb
  3. L60
    specialize beta_at_unique qc
  4. L61
    specialize beta_at_unique (S i)
  5. L62
    specialize beta_at_unique x1
  6. L63
    specialize beta_at_unique q
  7. L64
    apply beta_at_unique
  8. L65
    exact hprevious_witness_witness_witness_right_left
  9. L66
    exact hentry
17Establish hqnonzeroL67–73

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

  1. L67
    have hqnonzero : ~(x1 = 0)
  2. L68
    intro hzero
  3. L69
    apply hnonzero
  4. L70
    trans x1
  5. L71
    symm
  6. L72
    exact hquotient
  7. L73
    exact hzero
18Establish hstrictL74–82

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas prime digit nonzero quotient strict.

  1. L74
    have hstrict : Lt(x1,x)Definitions: Lt(x1,x)Original native command in the exact edition
  2. L75
    specialize lucas_prime_digit_nonzero_quotient_strict p
  3. L76
    specialize lucas_prime_digit_nonzero_quotient_strict x
  4. L77
    specialize lucas_prime_digit_nonzero_quotient_strict x1
  5. L78
    specialize lucas_prime_digit_nonzero_quotient_strict x2
  6. L79
    apply lucas_prime_digit_nonzero_quotient_strict
  7. L80
    exact hprime
  8. L81
    exact hqnonzero
  9. L82
    exact hprevious_witness_witness_witness_right_right_right_left
19Establish hprevious_nonzeroL83–85

Establish this local claim before using it. It is not an additional assumption.

  1. L83
    have hprevious_nonzero : ~(x = 0)
  2. L84
    intro hzero
  3. L85
    rewrite hzero at hstrict
20Separate the logical casesL86–86

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L86
    cases hstrict
21Calculate and transport equalitiesL87–87

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L87
    rewrite PA4 at hstrict_witness
22Use earlier factsL88–89

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

  1. L88
    apply PA1
  2. L89
    exact hstrict_witness
23Establish hprevious_domainL90–97

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

  1. L90
    have hprevious_domain : Le(i,l)Definitions: Le(i,l)Original native command in the exact edition
  2. L91
    specialize le_trans i
  3. L92
    specialize le_trans (S i)
  4. L93
    specialize le_trans l
  5. L94
    apply le_trans
  6. L95
    specialize le_succ_self i
  7. L96
    exact le_succ_self
  8. L97
    exact hdomain
24Establish hprevious_boundL98–107

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

  1. L98
    have hprevious_bound : Le(x + i,n)Definitions: Le(x + i,n)Original native command in the exact edition
  2. L99
    specialize IH p
  3. L100
    specialize IH n
  4. L101
    specialize IH qb
  5. L102
    specialize IH qc
  6. L103
    specialize IH db
  7. L104
    specialize IH dc
  8. L105
    specialize IH l
  9. L106
    specialize IH x
  10. L107
    apply IH
25Use earlier factsL108–109

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

  1. L108
    exact hprevious_domain
  2. L109
    exact hprime
26Separate the logical casesL110–110

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L110
    split
27Use earlier factsL111–114

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

  1. L111
    exact hchain_left
  2. L112
    exact hchain_right
  3. L113
    exact hprevious_witness_witness_witness_left
  4. L114
    exact hprevious_nonzero
28Calculate and transport equalitiesL115–115

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L115
    rewrite hquotient at hstrict
29Establish haddedL116–121

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

  1. L116
    have hadded : Le(S q + i,x + i)Definitions: Le(S q + i,x + i)Original native command in the exact edition
  2. L117
    specialize add_le_add_right (S q)
  3. L118
    specialize add_le_add_right x
  4. L119
    specialize add_le_add_right i
  5. L120
    apply add_le_add_right
  6. L121
    exact hstrict
30Establish hswapL122–131

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add succ left.

  1. L122
    have hswap : S q + i = q + S i
  2. L123
    trans S (q + i)
  3. L124
    apply add_succ_left
  4. L125
    symm
  5. L126
    apply PA4
  6. L127
    rewrite hswap at hadded
  7. L128
    specialize le_trans (q + S i)
  8. L129
    specialize le_trans (x + i)
  9. L130
    specialize le_trans n
  10. L131
    apply le_trans
31Use earlier factsL132–133

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

  1. L132
    exact hadded
  2. L133
    exact hprevious_bound

Library-wide reading audit

Original defined command ledger · 133 lines
  1. 0001intro i
  2. 0002induction i
  3. 0003intro p
  4. 0004intro n
  5. 0005intro qb
  6. 0006intro qc
  7. 0007intro db
  8. 0008intro dc
  9. 0009intro l
  10. 0010intro q
  11. 0011intro hdomain
  12. 0012intro hprime
  13. 0013intro hchain
  14. 0014intro hentry
  15. 0015intro hnonzero
  16. 0016cases hchain
  17. 0017have hequal : n = q
  18. 0018specialize beta_at_unique qb
  19. 0019specialize beta_at_unique qc
  20. 0020specialize beta_at_unique 0
  21. 0021specialize beta_at_unique n
  22. 0022specialize beta_at_unique q
  23. 0023apply beta_at_unique
  24. 0024exact hchain_left
  25. 0025exact hentry
  26. 0026exists 0
  27. 0027trans q
  28. 0028trans q + 0
  29. 0029apply zero_add
  30. 0030apply PA3
  31. 0031symm
  32. 0032exact hequal
  33. 0033intro p
  34. 0034intro n
  35. 0035intro qb
  36. 0036intro qc
  37. 0037intro db
  38. 0038intro dc
  39. 0039intro l
  40. 0040intro q
  41. 0041intro hdomain
  42. 0042intro hprime
  43. 0043intro hchain
  44. 0044intro hentry
  45. 0045intro hnonzero
  46. 0046cases hchain
  47. 0047have hprevious : ∃ a. ∃ Q. ∃ d. BetaAt(qb,qc,i,a) ∧ (BetaAt(qb,qc,S i,Q) ∧ (BetaAt(db,dc,i,d) ∧ DivRem(a,p,Q,d)))
    Exact native replay linehave hprevious : exists a Q d. ((((exists ff_h_lmd_index_previous. ff_h_lmd_index_previous + S (a) = S ((S (i)) * qc)) /\ exists ff_q_lmd_index_previous. qb = ff_q_lmd_index_previous * S ((S (i)) * qc) + (a))) /\ ((((exists ff_h_lmd_index_successor. ff_h_lmd_index_successor + S (Q) = S ((S (S i)) * qc)) /\ exists ff_q_lmd_index_successor. qb = ff_q_lmd_index_successor * S ((S (S i)) * qc) + (Q))) /\ ((((exists ff_h_lmd_index_digit. ff_h_lmd_index_digit + S (d) = S ((S (i)) * dc)) /\ exists ff_q_lmd_index_digit. db = ff_q_lmd_index_digit * S ((S (i)) * dc) + (d))) /\ ((a = p * Q + d) /\ (exists lmd_gap_index_digit_bound. lmd_gap_index_digit_bound + S (d) = (p))))))
  48. 0048specialize hchain_right i
  49. 0049apply hchain_right
  50. 0050exact hdomain
  51. 0051cases hprevious
  52. 0052cases hprevious_witness
  53. 0053cases hprevious_witness_witness
  54. 0054cases hprevious_witness_witness_witness
  55. 0055cases hprevious_witness_witness_witness_right
  56. 0056cases hprevious_witness_witness_witness_right_right
  57. 0057cases hprevious_witness_witness_witness_right_right_right
  58. 0058have hquotient : x1 = q
  59. 0059specialize beta_at_unique qb
  60. 0060specialize beta_at_unique qc
  61. 0061specialize beta_at_unique (S i)
  62. 0062specialize beta_at_unique x1
  63. 0063specialize beta_at_unique q
  64. 0064apply beta_at_unique
  65. 0065exact hprevious_witness_witness_witness_right_left
  66. 0066exact hentry
  67. 0067have hqnonzero : ~(x1 = 0)
  68. 0068intro hzero
  69. 0069apply hnonzero
  70. 0070trans x1
  71. 0071symm
  72. 0072exact hquotient
  73. 0073exact hzero
  74. 0074have hstrict : Lt(x1,x)
    Exact native replay linehave hstrict : exists gap. gap + S x1 = x
  75. 0075specialize lucas_prime_digit_nonzero_quotient_strict p
  76. 0076specialize lucas_prime_digit_nonzero_quotient_strict x
  77. 0077specialize lucas_prime_digit_nonzero_quotient_strict x1
  78. 0078specialize lucas_prime_digit_nonzero_quotient_strict x2
  79. 0079apply lucas_prime_digit_nonzero_quotient_strict
  80. 0080exact hprime
  81. 0081exact hqnonzero
  82. 0082exact hprevious_witness_witness_witness_right_right_right_left
  83. 0083have hprevious_nonzero : ~(x = 0)
  84. 0084intro hzero
  85. 0085rewrite hzero at hstrict
  86. 0086cases hstrict
  87. 0087rewrite PA4 at hstrict_witness
  88. 0088apply PA1
  89. 0089exact hstrict_witness
  90. 0090have hprevious_domain : Le(i,l)
    Exact native replay linehave hprevious_domain : exists gap. gap + i = l
  91. 0091specialize le_trans i
  92. 0092specialize le_trans (S i)
  93. 0093specialize le_trans l
  94. 0094apply le_trans
  95. 0095specialize le_succ_self i
  96. 0096exact le_succ_self
  97. 0097exact hdomain
  98. 0098have hprevious_bound : Le(x + i,n)
    Exact native replay linehave hprevious_bound : exists gap. gap + (x + i) = n
  99. 0099specialize IH p
  100. 0100specialize IH n
  101. 0101specialize IH qb
  102. 0102specialize IH qc
  103. 0103specialize IH db
  104. 0104specialize IH dc
  105. 0105specialize IH l
  106. 0106specialize IH x
  107. 0107apply IH
  108. 0108exact hprevious_domain
  109. 0109exact hprime
  110. 0110split
  111. 0111exact hchain_left
  112. 0112exact hchain_right
  113. 0113exact hprevious_witness_witness_witness_left
  114. 0114exact hprevious_nonzero
  115. 0115rewrite hquotient at hstrict
  116. 0116have hadded : Le(S q + i,x + i)
    Exact native replay linehave hadded : exists gap. gap + (S q + i) = x + i
  117. 0117specialize add_le_add_right (S q)
  118. 0118specialize add_le_add_right x
  119. 0119specialize add_le_add_right i
  120. 0120apply add_le_add_right
  121. 0121exact hstrict
  122. 0122have hswap : S q + i = q + S i
  123. 0123trans S (q + i)
  124. 0124apply add_succ_left
  125. 0125symm
  126. 0126apply PA4
  127. 0127rewrite hswap at hadded
  128. 0128specialize le_trans (q + S i)
  129. 0129specialize le_trans (x + i)
  130. 0130specialize le_trans n
  131. 0131apply le_trans
  132. 0132exact hadded
  133. 0133exact hprevious_bound