LU0017 · theorem body

lucas_digit_chain_empty_exists

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

An actual initial quotient code and arbitrary empty digit code exist for every 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. ∃ qb. ∃ qc. ∃ db. ∃ dc. BetaAt(qb,qc,0,n) ∧ (∀ x. Lt(x,0) → ∃ y. ∃ z. ∃ m. BetaAt(qb,qc,x,y) ∧ (BetaAt(qb,qc,S x,z) ∧ (BetaAt(db,dc,x,m) ∧ DivRem(y,p,z,m))))

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

In local proof propositions

none
Exact expanded first-order statement
forall p n. exists qb qc db dc. (((((exists ff_h_lmd_empty_initial. ff_h_lmd_empty_initial + S (n) = S ((S (0)) * qc)) /\ exists ff_q_lmd_empty_initial. qb = ff_q_lmd_empty_initial * S ((S (0)) * qc) + (n))) /\ forall lmd_index_empty. (exists lmd_gap_empty_index. lmd_gap_empty_index + S (lmd_index_empty) = (0)) -> exists lmd_current_empty lmd_successor_empty lmd_digit_empty. ((((exists ff_h_lmd_empty_current. ff_h_lmd_empty_current + S (lmd_current_empty) = S ((S (lmd_index_empty)) * qc)) /\ exists ff_q_lmd_empty_current. qb = ff_q_lmd_empty_current * S ((S (lmd_index_empty)) * qc) + (lmd_current_empty))) /\ ((((exists ff_h_lmd_empty_successor. ff_h_lmd_empty_successor + S (lmd_successor_empty) = S ((S (S lmd_index_empty)) * qc)) /\ exists ff_q_lmd_empty_successor. qb = ff_q_lmd_empty_successor * S ((S (S lmd_index_empty)) * qc) + (lmd_successor_empty))) /\ ((((exists ff_h_lmd_empty_digit. ff_h_lmd_empty_digit + S (lmd_digit_empty) = S ((S (lmd_index_empty)) * dc)) /\ exists ff_q_lmd_empty_digit. db = ff_q_lmd_empty_digit * S ((S (lmd_index_empty)) * dc) + (lmd_digit_empty))) /\ ((lmd_current_empty = (p) * (lmd_successor_empty) + (lmd_digit_empty)) /\ (exists lmd_gap_empty_digit_bound. lmd_gap_empty_digit_bound + S (lmd_digit_empty) = (p))))))))

Proof neighborhood

Direct theorem prerequisites

LU0015 lucas_digit_chain_initial_code_exists LU0016 lucas_digit_chain_empty

Direct theorem dependents

LU0019 lucas_digit_chain_exists

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

11 script commands · 5 reading checkpoints · 0 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 (2)
lucas digit chain initial code existslucas digit chain empty
01Fix variables and assumptionsL1–2

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

  1. L1
    intro p
  2. L2
    intro n
02Use earlier factsL3–3

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

  1. L3
    specialize lucas_digit_chain_initial_code_exists n
03Separate the logical casesL4–5

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

  1. L4
    cases lucas_digit_chain_initial_code_exists
  2. L5
    cases lucas_digit_chain_initial_code_exists_witness
04Construct an explicit witnessL6–9

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

  1. L6
    exists x
  2. L7
    exists x1
  3. L8
    exists 0
  4. L9
    exists 0
05Use earlier factsL10–11

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

  1. L10
    apply lucas_digit_chain_empty
  2. L11
    exact lucas_digit_chain_initial_code_exists_witness_witness

Library-wide reading audit

Original defined command ledger · 11 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003specialize lucas_digit_chain_initial_code_exists n
  4. 0004cases lucas_digit_chain_initial_code_exists
  5. 0005cases lucas_digit_chain_initial_code_exists_witness
  6. 0006exists x
  7. 0007exists x1
  8. 0008exists 0
  9. 0009exists 0
  10. 0010apply lucas_digit_chain_empty
  11. 0011exact lucas_digit_chain_initial_code_exists_witness_witness