LU0017

lucas_digit_chain_empty_exists

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

An actual initial quotient code and arbitrary empty digit code exist for every natural.

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

Constructive proof overview

Generated structural guide

An actual initial quotient code and arbitrary empty digit code exist for every natural.

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

LU0015 lucas_digit_chain_initial_code_exists LU0016 lucas_digit_chain_empty

Direct dependents

LU0019 lucas_digit_chain_exists

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

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.

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