BD0002

binary_digit_prefix_recode

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 41 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_at_exists Stable theorem; checked-use authorized beta_at_unique Stable theorem; checked-use authorized

Direct dependents

none

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

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.

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

Separate complete second-wave branches: Full T13 proof · Alpha v27.