BD0002

binary_digit_prefix_recode

Recoding that preserves every earlier beta entry preserves its actual zero-or-one digit invariant.

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 G102 milestone is fully proved for every natural exponent and every modulus greater than one, including actual canonical digits, a beta-coded accumulator execution, modular-power correctness, and the formal bound k≤3·BitLen(e)+2. The independent T13 determinant/rank/integer-span substrate is now closed in the separate Alpha-v27 integer-linear-algebra branch. Full T13 proof · Alpha v27

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ z. ∀ e. ∀ l. BinaryDigitPrefix(b,c,l) → (∀ x. ∀ y. Lt(x,l) → Beta(b,c,x,y) → Beta(z,e,x,y)) → BinaryDigitPrefix(z,e,l)

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

Definition DAG

Beta(b,c,i,x) · 2BinaryDigitPrefix(d,s,n) · 2Lt(a,b) · 1

Actual proof prerequisites

beta_at_exists · checked external prerequisitebeta_at_unique · checked external prerequisite
Original expanded first-order statement 
forall b c z e l. (forall ff_index_be_bd_old ff_digit_be_bd_old. (exists ff_lt_be_bd_old_bound. ff_lt_be_bd_old_bound + S ff_index_be_bd_old = l) -> (((exists ff_h_be_bd_old_digit. ff_h_be_bd_old_digit + S (ff_digit_be_bd_old) = S ((S (ff_index_be_bd_old)) * c)) /\ exists ff_q_be_bd_old_digit. b = ff_q_be_bd_old_digit * S ((S (ff_index_be_bd_old)) * c) + (ff_digit_be_bd_old))) -> (ff_digit_be_bd_old = 0 \/ ff_digit_be_bd_old = 1)) -> (forall bd_index_recode bd_value_recode. (exists bd_gap_recode. bd_gap_recode + S bd_index_recode = l) -> (((exists ff_h_bd_recode_old. ff_h_bd_recode_old + S (bd_value_recode) = S ((S (bd_index_recode)) * c)) /\ exists ff_q_bd_recode_old. b = ff_q_bd_recode_old * S ((S (bd_index_recode)) * c) + (bd_value_recode))) -> (((exists ff_h_bd_recode_new. ff_h_bd_recode_new + S (bd_value_recode) = S ((S (bd_index_recode)) * e)) /\ exists ff_q_bd_recode_new. z = ff_q_bd_recode_new * S ((S (bd_index_recode)) * e) + (bd_value_recode)))) -> (forall ff_index_be_bd_new ff_digit_be_bd_new. (exists ff_lt_be_bd_new_bound. ff_lt_be_bd_new_bound + S ff_index_be_bd_new = l) -> (((exists ff_h_be_bd_new_digit. ff_h_be_bd_new_digit + S (ff_digit_be_bd_new) = S ((S (ff_index_be_bd_new)) * e)) /\ exists ff_q_be_bd_new_digit. z = ff_q_be_bd_new_digit * S ((S (ff_index_be_bd_new)) * e) + (ff_digit_be_bd_new))) -> (ff_digit_be_bd_new = 0 \/ ff_digit_be_bd_new = 1))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

41 script commands · 7 reading checkpoints · 4 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 b
  2. L2
    intro c
  3. L3
    intro z
  4. L4
    intro e
  5. L5
    intro l
  6. L6
    intro hold
  7. L7
    intro hpreserve
  8. L8
    intro i
  9. L9
    intro d
  10. L10
    intro hbound
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hnew
03Establish hsourceL12–16

Establish this local claim before using it. It is not an additional assumption.

  1. L12
    have hsource : exists value. (((exists ff_h_bd_recode_source. ff_h_bd_recode_source + S (value) = S ((S (i)) * c)) /\ exists ff_q_bd_recode_source. b = ff_q_bd_recode_source * S ((S (i)) * c) + (value)))
  2. L13
    specialize beta_at_exists b
  3. L14
    specialize beta_at_exists c
  4. L15
    specialize beta_at_exists i
  5. L16
    exact beta_at_exists
04Separate the logical casesL17–17

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

  1. L17
    cases hsource
05Establish htransportL18–23

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

  1. L18
    have htransport : (((exists ff_h_bd_recode_transport. ff_h_bd_recode_transport + S (x) = S ((S (i)) * e)) /\ exists ff_q_bd_recode_transport. z = ff_q_bd_recode_transport * S ((S (i)) * e) + (x)))
  2. L19
    specialize hpreserve i
  3. L20
    specialize hpreserve x
  4. L21
    apply hpreserve
  5. L22
    exact hbound
  6. L23
    exact hsource_witness
06Establish hequalL24–32

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

  1. L24
    have hequal : x = d
  2. L25
    specialize beta_at_unique z
  3. L26
    specialize beta_at_unique e
  4. L27
    specialize beta_at_unique i
  5. L28
    specialize beta_at_unique x
  6. L29
    specialize beta_at_unique d
  7. L30
    apply beta_at_unique
  8. L31
    exact htransport
  9. L32
    exact hnew
07Establish hbitL33–41

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

  1. L33
    have hbit : x = 0 \/ x = 1
  2. L34
    specialize hold i
  3. L35
    specialize hold x
  4. L36
    apply hold
  5. L37
    exact hbound
  6. L38
    exact hsource_witness
  7. L39
    rewrite hequal at hbit
  8. L40
    rewrite hequal at hbit
  9. L41
    exact hbit

Library-wide reading audit

Original defined command ledger · 41 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro z
  4. 0004intro e
  5. 0005intro l
  6. 0006intro hold
  7. 0007intro hpreserve
  8. 0008intro i
  9. 0009intro d
  10. 0010intro hbound
  11. 0011intro hnew
  12. 0012have hsource : exists value. (((exists ff_h_bd_recode_source. ff_h_bd_recode_source + S (value) = S ((S (i)) * c)) /\ exists ff_q_bd_recode_source. b = ff_q_bd_recode_source * S ((S (i)) * c) + (value)))
  13. 0013specialize beta_at_exists b
  14. 0014specialize beta_at_exists c
  15. 0015specialize beta_at_exists i
  16. 0016exact beta_at_exists
  17. 0017cases hsource
  18. 0018have htransport : (((exists ff_h_bd_recode_transport. ff_h_bd_recode_transport + S (x) = S ((S (i)) * e)) /\ exists ff_q_bd_recode_transport. z = ff_q_bd_recode_transport * S ((S (i)) * e) + (x)))
  19. 0019specialize hpreserve i
  20. 0020specialize hpreserve x
  21. 0021apply hpreserve
  22. 0022exact hbound
  23. 0023exact hsource_witness
  24. 0024have hequal : x = d
  25. 0025specialize beta_at_unique z
  26. 0026specialize beta_at_unique e
  27. 0027specialize beta_at_unique i
  28. 0028specialize beta_at_unique x
  29. 0029specialize beta_at_unique d
  30. 0030apply beta_at_unique
  31. 0031exact htransport
  32. 0032exact hnew
  33. 0033have hbit : x = 0 \/ x = 1
  34. 0034specialize hold i
  35. 0035specialize hold x
  36. 0036apply hold
  37. 0037exact hbound
  38. 0038exact hsource_witness
  39. 0039rewrite hequal at hbit
  40. 0040rewrite hequal at hbit
  41. 0041exact hbit