LU0006

lucas_prime_base_digit_total

Dependency-curried candidate body; not Alpha-enrolled; no checked-use authority

Every prime base constructively provides a quotient and canonical least-significant digit 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. ((~(p = 1) /\ forall frm_prime_left_lucas_digit_total_prime frm_prime_right_lucas_digit_total_prime. p = frm_prime_left_lucas_digit_total_prime * frm_prime_right_lucas_digit_total_prime -> frm_prime_left_lucas_digit_total_prime = 1 \/ frm_prime_right_lucas_digit_total_prime = 1)) -> exists q d. (((n) = (p) * (q) + (d)) /\ (exists ldc_lt_native_bound. ldc_lt_native_bound + S (d) = p))

Constructive proof overview

Generated structural guide

Every prime base constructively provides a quotient and canonical least-significant digit 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

Proof neighborhood

Direct dependencies

prime_nonzero Stable theorem; checked-use authorized LU0005 lucas_base_p_digit_total

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This dependency-curried candidate body does not grant checked theorem use or Stable membership.

Read the argument

Proof checkpoints

11 script commands · 4 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 (1)
lucas base p digit total
01Fix variables and assumptionsL1–3

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro hprime
02Use earlier factsL4–6

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

  1. L4
    specialize lucas_base_p_digit_total p
  2. L5
    specialize lucas_base_p_digit_total n
  3. L6
    apply lucas_base_p_digit_total
03Fix variables and assumptionsL7–7

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

  1. L7
    intro hzero
04Use earlier factsL8–11

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

  1. L8
    specialize prime_nonzero p
  2. L9
    apply prime_nonzero
  3. L10
    exact hprime
  4. L11
    exact hzero

Library-wide reading audit

Original exact command ledger · 11 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro hprime
  4. 0004specialize lucas_base_p_digit_total p
  5. 0005specialize lucas_base_p_digit_total n
  6. 0006apply lucas_base_p_digit_total
  7. 0007intro hzero
  8. 0008specialize prime_nonzero p
  9. 0009apply prime_nonzero
  10. 0010exact hprime
  11. 0011exact hzero