LU000C · theorem body

lucas_base_p_digit_prefix_point

dependency-curried kernel-checked candidate body; not enrolled in Alpha or Stable

At every source beta index, the quotient and digit beta prefixes expose the unique actual quotient/digit witnesses of that source value.

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. ∀ b. ∀ c. ∀ qb. ∀ qc. ∀ db. ∀ dc. ∀ l. ∀ i. ∀ n. DivisionPrefix(p,b,c,qb,qc,db,dc,l) → Lt(i,l) → BetaAt(b,c,i,n) → ∃ x. ∃ y. BetaAt(qb,qc,i,x) ∧ (BetaAt(db,dc,i,y) ∧ DivRem(n,p,x,y))

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 PD0007 DivRem PD0013 BetaAt PD0040 DivisionPrefix

In local proof propositions

PD0007 DivRem PD0013 BetaAt
Exact expanded first-order statement
forall p b c qb qc db dc l i n. (forall fdp_index_lucas_digits. (exists gsp_lt_gap_lucas_digits_index_bound. gsp_lt_gap_lucas_digits_index_bound + S fdp_index_lucas_digits = l) -> exists fdp_value_lucas_digits fdp_quotient_lucas_digits fdp_remainder_lucas_digits. (((exists ff_h_fdp_lucas_digits_source. ff_h_fdp_lucas_digits_source + S (fdp_value_lucas_digits) = S ((S (fdp_index_lucas_digits)) * c)) /\ exists ff_q_fdp_lucas_digits_source. b = ff_q_fdp_lucas_digits_source * S ((S (fdp_index_lucas_digits)) * c) + (fdp_value_lucas_digits))) /\ ((((exists ff_h_fdp_lucas_digits_quotient_entry. ff_h_fdp_lucas_digits_quotient_entry + S (fdp_quotient_lucas_digits) = S ((S (fdp_index_lucas_digits)) * qc)) /\ exists ff_q_fdp_lucas_digits_quotient_entry. qb = ff_q_fdp_lucas_digits_quotient_entry * S ((S (fdp_index_lucas_digits)) * qc) + (fdp_quotient_lucas_digits))) /\ ((((exists ff_h_fdp_lucas_digits_remainder_entry. ff_h_fdp_lucas_digits_remainder_entry + S (fdp_remainder_lucas_digits) = S ((S (fdp_index_lucas_digits)) * dc)) /\ exists ff_q_fdp_lucas_digits_remainder_entry. db = ff_q_fdp_lucas_digits_remainder_entry * S ((S (fdp_index_lucas_digits)) * dc) + (fdp_remainder_lucas_digits))) /\ (fdp_value_lucas_digits = p * fdp_quotient_lucas_digits + fdp_remainder_lucas_digits /\ (exists gsp_lt_gap_lucas_digits_remainder_bound. gsp_lt_gap_lucas_digits_remainder_bound + S fdp_remainder_lucas_digits = p))))) -> (exists ldc_lt_prefix_index. ldc_lt_prefix_index + S (i) = l) -> (((exists ff_h_lucas_source. ff_h_lucas_source + S (n) = S ((S (i)) * c)) /\ exists ff_q_lucas_source. b = ff_q_lucas_source * S ((S (i)) * c) + (n))) -> (exists q d. ((((exists ff_h_lucas_quotient. ff_h_lucas_quotient + S (q) = S ((S (i)) * qc)) /\ exists ff_q_lucas_quotient. qb = ff_q_lucas_quotient * S ((S (i)) * qc) + (q))) /\ ((((exists ff_h_lucas_digit. ff_h_lucas_digit + S (d) = S ((S (i)) * dc)) /\ exists ff_q_lucas_digit. db = ff_q_lucas_digit * S ((S (i)) * dc) + (d))) /\ (((n) = (p) * (q) + (d)) /\ (exists ldc_lt_native_bound. ldc_lt_native_bound + S (d) = p)))))

Proof neighborhood

Direct theorem prerequisites

beta_at_unique · Stable closed

Direct theorem dependents

none

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

43 script commands · 14 reading checkpoints · 2 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–10

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

  1. L1
    intro p
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro qb
  5. L5
    intro qc
  6. L6
    intro db
  7. L7
    intro dc
  8. L8
    intro l
  9. L9
    intro i
  10. L10
    intro n
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hprefix
  2. L12
    intro hbound
  3. L13
    intro hsource
03Use earlier factsL14–14

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

  1. L14
    specialize hprefix i
04Establish hpointL15–17

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

  1. L15
    have hpoint : ∃ value. ∃ quotient. ∃ remainder. BetaAt(b,c,i,value) ∧ (BetaAt(qb,qc,i,quotient) ∧ (BetaAt(db,dc,i,remainder) ∧ DivRem(value,p,quotient,remainder)))Definitions: BetaAt(b,c,i,value)BetaAt(qb,qc,i,quotient)BetaAt(db,dc,i,remainder)DivRem(value,p,quotient,remainder)Original native command in the exact edition
  2. L16
    apply hprefix
  3. L17
    exact hbound
05Separate the logical casesL18–24

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

  1. L18
    cases hpoint
  2. L19
    cases hpoint_witness
  3. L20
    cases hpoint_witness_witness
  4. L21
    cases hpoint_witness_witness_witness
  5. L22
    cases hpoint_witness_witness_witness_right
  6. L23
    cases hpoint_witness_witness_witness_right_right
  7. L24
    cases hpoint_witness_witness_witness_right_right_right
06Establish hvalueL25–33

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

  1. L25
    have hvalue : x = n
  2. L26
    specialize beta_at_unique b
  3. L27
    specialize beta_at_unique c
  4. L28
    specialize beta_at_unique i
  5. L29
    specialize beta_at_unique x
  6. L30
    specialize beta_at_unique n
  7. L31
    apply beta_at_unique
  8. L32
    exact hpoint_witness_witness_witness_left
  9. L33
    exact hsource
07Construct an explicit witnessL34–35

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

  1. L34
    exists x1
  2. L35
    exists x2
08Separate the logical casesL36–36

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

  1. L36
    split
09Use earlier factsL37–37

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

  1. L37
    exact hpoint_witness_witness_witness_right_left
10Separate the logical casesL38–38

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

  1. L38
    split
11Use earlier factsL39–39

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

  1. L39
    exact hpoint_witness_witness_witness_right_right_left
12Separate the logical casesL40–40

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

  1. L40
    split
13Calculate and transport equalitiesL41–41

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

  1. L41
    rewrite <- hvalue
14Use earlier factsL42–43

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

  1. L42
    exact hpoint_witness_witness_witness_right_right_right_left
  2. L43
    exact hpoint_witness_witness_witness_right_right_right_right

Library-wide reading audit

Original defined command ledger · 43 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro qb
  5. 0005intro qc
  6. 0006intro db
  7. 0007intro dc
  8. 0008intro l
  9. 0009intro i
  10. 0010intro n
  11. 0011intro hprefix
  12. 0012intro hbound
  13. 0013intro hsource
  14. 0014specialize hprefix i
  15. 0015have hpoint : ∃ value. ∃ quotient. ∃ remainder. BetaAt(b,c,i,value) ∧ (BetaAt(qb,qc,i,quotient) ∧ (BetaAt(db,dc,i,remainder) ∧ DivRem(value,p,quotient,remainder)))
    Exact native replay linehave hpoint : exists value quotient remainder. (((exists ff_h_lucas_point_source. ff_h_lucas_point_source + S (value) = S ((S (i)) * c)) /\ exists ff_q_lucas_point_source. b = ff_q_lucas_point_source * S ((S (i)) * c) + (value))) /\ ((((exists ff_h_lucas_point_quotient. ff_h_lucas_point_quotient + S (quotient) = S ((S (i)) * qc)) /\ exists ff_q_lucas_point_quotient. qb = ff_q_lucas_point_quotient * S ((S (i)) * qc) + (quotient))) /\ ((((exists ff_h_lucas_point_remainder. ff_h_lucas_point_remainder + S (remainder) = S ((S (i)) * dc)) /\ exists ff_q_lucas_point_remainder. db = ff_q_lucas_point_remainder * S ((S (i)) * dc) + (remainder))) /\ (value = p * quotient + remainder /\ (exists ldc_lt_point_digit_bound. ldc_lt_point_digit_bound + S (remainder) = p))))
  16. 0016apply hprefix
  17. 0017exact hbound
  18. 0018cases hpoint
  19. 0019cases hpoint_witness
  20. 0020cases hpoint_witness_witness
  21. 0021cases hpoint_witness_witness_witness
  22. 0022cases hpoint_witness_witness_witness_right
  23. 0023cases hpoint_witness_witness_witness_right_right
  24. 0024cases hpoint_witness_witness_witness_right_right_right
  25. 0025have hvalue : x = n
  26. 0026specialize beta_at_unique b
  27. 0027specialize beta_at_unique c
  28. 0028specialize beta_at_unique i
  29. 0029specialize beta_at_unique x
  30. 0030specialize beta_at_unique n
  31. 0031apply beta_at_unique
  32. 0032exact hpoint_witness_witness_witness_left
  33. 0033exact hsource
  34. 0034exists x1
  35. 0035exists x2
  36. 0036split
  37. 0037exact hpoint_witness_witness_witness_right_left
  38. 0038split
  39. 0039exact hpoint_witness_witness_witness_right_right_left
  40. 0040split
  41. 0041rewrite <- hvalue
  42. 0042exact hpoint_witness_witness_witness_right_right_right_left
  43. 0043exact hpoint_witness_witness_witness_right_right_right_right