TF0004

beta_all_prime_entry_is_prime

Every concrete decoded entry in the canonical all-prime prefix is prime, by uniqueness of beta decoding.

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

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.

The exact G025 progression-prime milestone is fully proved in unchanged constructive arithmetic; Mod4Three deliberately reuses its existing Quadratic Reciprocity definition PD0012. The much stronger full Dirichlet progression-prime milestone G030 remains open.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ l. ∀ i. ∀ p. AllPrime(b,c,l) → Lt(i,l) → BetaAt(b,c,i,p) → Prime(p)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

Lt(a,b) · 1Prime(p) · 1BetaAt(b,c,i,x) · 1AllPrime(b,c,l) · 1

Actual proof prerequisites

beta_at_unique · checked external prerequisite
Original expanded first-order statement 
forall b c l i p. (forall ftsf_index_all_prime_source. (exists ftsf_gap_all_prime_source_bound. ftsf_gap_all_prime_source_bound + S ftsf_index_all_prime_source = (l)) -> exists ftsf_factor_all_prime_source. ((((exists ff_h_ftsf_all_prime_source_entry. ff_h_ftsf_all_prime_source_entry + S (ftsf_factor_all_prime_source) = S ((S (ftsf_index_all_prime_source)) * c)) /\ exists ff_q_ftsf_all_prime_source_entry. b = ff_q_ftsf_all_prime_source_entry * S ((S (ftsf_index_all_prime_source)) * c) + (ftsf_factor_all_prime_source))) /\ ((~(ftsf_factor_all_prime_source = 1) /\ forall frm_prime_left_ftsf_all_prime_source_prime frm_prime_right_ftsf_all_prime_source_prime. ftsf_factor_all_prime_source = frm_prime_left_ftsf_all_prime_source_prime * frm_prime_right_ftsf_all_prime_source_prime -> frm_prime_left_ftsf_all_prime_source_prime = 1 \/ frm_prime_right_ftsf_all_prime_source_prime = 1)))) -> (exists ftsf_gap_all_prime_entry. ftsf_gap_all_prime_entry + S i = (l)) -> (((exists ff_h_ftsf_selected_entry. ff_h_ftsf_selected_entry + S (p) = S ((S (i)) * c)) /\ exists ff_q_ftsf_selected_entry. b = ff_q_ftsf_selected_entry * S ((S (i)) * c) + (p))) -> ((~(p = 1) /\ forall frm_prime_left_ftsf_selected_prime frm_prime_right_ftsf_selected_prime. p = frm_prime_left_ftsf_selected_prime * frm_prime_right_ftsf_selected_prime -> frm_prime_left_ftsf_selected_prime = 1 \/ frm_prime_right_ftsf_selected_prime = 1))

Complete unchanged native tactic proof

All 26 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

26 script commands · 7 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–8

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro i
  5. L5
    intro p
  6. L6
    intro hall
  7. L7
    intro hi
  8. L8
    intro hp
02Use earlier factsL9–9

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

  1. L9
    specialize hall i
03Establish hentryL10–12

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

  1. L10
    have hentry : exists a. ((((exists ff_h_ftsf_prime_local. ff_h_ftsf_prime_local + S (a) = S ((S (i)) * c)) /\ exists ff_q_ftsf_prime_local. b = ff_q_ftsf_prime_local * S ((S (i)) * c) + (a))) /\ ((~(a = 1) /\ forall frm_prime_left_ftsf_prime_local frm_prime_right_ftsf_prime_local. a = frm_prime_left_ftsf_prime_local * frm_prime_right_ftsf_prime_local -> frm_prime_left_ftsf_prime_local = 1 \/ frm_prime_right_ftsf_prime_local = 1)))
  2. L11
    apply hall
  3. L12
    exact hi
04Separate the logical casesL13–14

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

  1. L13
    cases hentry
  2. L14
    cases hentry_witness
05Establish hequalL15–24

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

  1. L15
    have hequal : p = x
  2. L16
    specialize beta_at_unique b
  3. L17
    specialize beta_at_unique c
  4. L18
    specialize beta_at_unique i
  5. L19
    specialize beta_at_unique p
  6. L20
    specialize beta_at_unique x
  7. L21
    apply beta_at_unique
  8. L22
    exact hp
  9. L23
    exact hentry_witness_left
  10. L24
    rewrite hequal
06Calculate and transport equalitiesL25–25

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

  1. L25
    rewrite hequal
07Use earlier factsL26–26

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

  1. L26
    exact hentry_witness_right

Library-wide reading audit

Original defined command ledger · 26 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro i
  5. 0005intro p
  6. 0006intro hall
  7. 0007intro hi
  8. 0008intro hp
  9. 0009specialize hall i
  10. 0010have hentry : exists a. ((((exists ff_h_ftsf_prime_local. ff_h_ftsf_prime_local + S (a) = S ((S (i)) * c)) /\ exists ff_q_ftsf_prime_local. b = ff_q_ftsf_prime_local * S ((S (i)) * c) + (a))) /\ ((~(a = 1) /\ forall frm_prime_left_ftsf_prime_local frm_prime_right_ftsf_prime_local. a = frm_prime_left_ftsf_prime_local * frm_prime_right_ftsf_prime_local -> frm_prime_left_ftsf_prime_local = 1 \/ frm_prime_right_ftsf_prime_local = 1)))
  11. 0011apply hall
  12. 0012exact hi
  13. 0013cases hentry
  14. 0014cases hentry_witness
  15. 0015have hequal : p = x
  16. 0016specialize beta_at_unique b
  17. 0017specialize beta_at_unique c
  18. 0018specialize beta_at_unique i
  19. 0019specialize beta_at_unique p
  20. 0020specialize beta_at_unique x
  21. 0021apply beta_at_unique
  22. 0022exact hp
  23. 0023exact hentry_witness_left
  24. 0024rewrite hequal
  25. 0025rewrite hequal
  26. 0026exact hentry_witness_right