BD0004

binary_digit_prefix_append

Every valid beta-coded binary prefix can append a real zero-or-one digit without changing any older entry.

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. ∀ l. ∀ d. BinaryDigitPrefix(b,c,l) → d = 0 ∨ d = 1 → ∃ x. ∃ y. Beta(x,y,l,d) ∧ (BinaryDigitPrefix(x,y,S l) ∧ (∀ z. ∀ n. Lt(z,l) → Beta(b,c,z,n) → Beta(x,y,z,n)))

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

Definition DAG

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

Actual proof prerequisites

binary_digit_code_recode_existsfinite_lt_succ_eq_or_lt · checked external prerequisitebeta_at_exists · checked external prerequisitebeta_at_unique · checked external prerequisite
Original expanded first-order statement 
forall b c l d. (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)) -> (d = 0 \/ d = 1) -> (exists z e. ((((exists ff_h_bd_append_terminal. ff_h_bd_append_terminal + S (d) = S ((S (l)) * e)) /\ exists ff_q_bd_append_terminal. z = ff_q_bd_append_terminal * S ((S (l)) * e) + (d))) /\ ((forall ff_index_be_bd_append ff_digit_be_bd_append. (exists ff_lt_be_bd_append_bound. ff_lt_be_bd_append_bound + S ff_index_be_bd_append = S l) -> (((exists ff_h_be_bd_append_digit. ff_h_be_bd_append_digit + S (ff_digit_be_bd_append) = S ((S (ff_index_be_bd_append)) * e)) /\ exists ff_q_be_bd_append_digit. z = ff_q_be_bd_append_digit * S ((S (ff_index_be_bd_append)) * e) + (ff_digit_be_bd_append))) -> (ff_digit_be_bd_append = 0 \/ ff_digit_be_bd_append = 1)) /\ (forall bd_index_append_recode bd_value_append_recode. (exists bd_gap_append_recode. bd_gap_append_recode + S bd_index_append_recode = l) -> (((exists ff_h_bd_append_recode_old. ff_h_bd_append_recode_old + S (bd_value_append_recode) = S ((S (bd_index_append_recode)) * c)) /\ exists ff_q_bd_append_recode_old. b = ff_q_bd_append_recode_old * S ((S (bd_index_append_recode)) * c) + (bd_value_append_recode))) -> (((exists ff_h_bd_append_recode_new. ff_h_bd_append_recode_new + S (bd_value_append_recode) = S ((S (bd_index_append_recode)) * e)) /\ exists ff_q_bd_append_recode_new. z = ff_q_bd_append_recode_new * S ((S (bd_index_append_recode)) * e) + (bd_value_append_recode)))))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

77 script commands · 18 reading checkpoints · 8 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.

Named ingredients (1)
binary digit code recode exists

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–6

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 d
  5. L5
    intro hdigits
  6. L6
    intro hdigit
02Establish hcodeL7–12

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

  1. L7
    have hcode : ∃ z. ∃ e. Beta(z,e,l,d) ∧ (∀ x. ∀ y. Lt(x,l) → Beta(b,c,x,y) → Beta(z,e,x,y))Definitions: BetaLtOriginal native command in the exact edition
  2. L8
    specialize binary_digit_code_recode_exists b
  3. L9
    specialize binary_digit_code_recode_exists c
  4. L10
    specialize binary_digit_code_recode_exists l
  5. L11
    specialize binary_digit_code_recode_exists d
  6. L12
    exact binary_digit_code_recode_exists
03Separate the logical casesL13–15

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

  1. L13
    cases hcode
  2. L14
    cases hcode_witness
  3. L15
    cases hcode_witness_witness
04Construct an explicit witnessL16–17

Supply the displayed value, then prove that it has the required property.

  1. L16
    exists x
  2. L17
    exists x1
05Separate the logical casesL18–18

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

  1. L18
    split
06Use earlier factsL19–19

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

  1. L19
    exact hcode_witness_witness_left
07Separate the logical casesL20–20

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

  1. L20
    split
08Fix variables and assumptionsL21–24

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

  1. L21
    intro i
  2. L22
    intro a
  3. L23
    intro hbound
  4. L24
    intro hentry
09Establish hcasesL25–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L25
    have hcases : i = l \/ exists gap. gap + S i = l
  2. L26
    specialize finite_lt_succ_eq_or_lt l
  3. L27
    specialize finite_lt_succ_eq_or_lt i
  4. L28
    apply finite_lt_succ_eq_or_lt
  5. L29
    exact hbound
10Separate the logical casesL30–30

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

  1. L30
    cases hcases
11Calculate and transport equalitiesL31–32

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

  1. L31
    rewrite hcases_left at hentry
  2. L32
    rewrite hcases_left at hentry
12Establish hlastL33–41

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

  1. L33
    have hlast : d = a
  2. L34
    specialize beta_at_unique x
  3. L35
    specialize beta_at_unique x1
  4. L36
    specialize beta_at_unique l
  5. L37
    specialize beta_at_unique d
  6. L38
    specialize beta_at_unique a
  7. L39
    apply beta_at_unique
  8. L40
    exact hcode_witness_witness_left
  9. L41
    exact hentry
13Establish hlastbitL42–46

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

  1. L42
    have hlastbit : d = 0 \/ d = 1
  2. L43
    exact hdigit
  3. L44
    rewrite hlast at hlastbit
  4. L45
    rewrite hlast at hlastbit
  5. L46
    exact hlastbit
14Establish hsourceL47–51

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

  1. L47
    have hsource : exists value. (((exists ff_h_bd_append_source. ff_h_bd_append_source + S (value) = S ((S (i)) * c)) /\ exists ff_q_bd_append_source. b = ff_q_bd_append_source * S ((S (i)) * c) + (value)))
  2. L48
    specialize beta_at_exists b
  3. L49
    specialize beta_at_exists c
  4. L50
    specialize beta_at_exists i
  5. L51
    exact beta_at_exists
15Separate the logical casesL52–52

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

  1. L52
    cases hsource
16Establish htransportL53–58

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

  1. L53
    have htransport : (((exists ff_h_bd_append_transport. ff_h_bd_append_transport + S (x2) = S ((S (i)) * x1)) /\ exists ff_q_bd_append_transport. x = ff_q_bd_append_transport * S ((S (i)) * x1) + (x2)))
  2. L54
    specialize hcode_witness_witness_right i
  3. L55
    specialize hcode_witness_witness_right x2
  4. L56
    apply hcode_witness_witness_right
  5. L57
    exact hcases_right
  6. L58
    exact hsource_witness
17Establish holdvalueL59–67

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

  1. L59
    have holdvalue : x2 = a
  2. L60
    specialize beta_at_unique x
  3. L61
    specialize beta_at_unique x1
  4. L62
    specialize beta_at_unique i
  5. L63
    specialize beta_at_unique x2
  6. L64
    specialize beta_at_unique a
  7. L65
    apply beta_at_unique
  8. L66
    exact htransport
  9. L67
    exact hentry
18Establish holdbitL68–77

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

  1. L68
    have holdbit : x2 = 0 \/ x2 = 1
  2. L69
    specialize hdigits i
  3. L70
    specialize hdigits x2
  4. L71
    apply hdigits
  5. L72
    exact hcases_right
  6. L73
    exact hsource_witness
  7. L74
    rewrite holdvalue at holdbit
  8. L75
    rewrite holdvalue at holdbit
  9. L76
    exact holdbit
  10. L77
    exact hcode_witness_witness_right

Library-wide reading audit

Original defined command ledger · 77 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro d
  5. 0005intro hdigits
  6. 0006intro hdigit
  7. 0007have hcode : exists z e. ((((exists ff_h_bd_recode_terminal. ff_h_bd_recode_terminal + S (d) = S ((S (l)) * e)) /\ exists ff_q_bd_recode_terminal. z = ff_q_bd_recode_terminal * S ((S (l)) * e) + (d))) /\ (forall bd_index_recode_result bd_value_recode_result. (exists bd_gap_recode_result. bd_gap_recode_result + S bd_index_recode_result = l) -> (((exists ff_h_bd_recode_result_old. ff_h_bd_recode_result_old + S (bd_value_recode_result) = S ((S (bd_index_recode_result)) * c)) /\ exists ff_q_bd_recode_result_old. b = ff_q_bd_recode_result_old * S ((S (bd_index_recode_result)) * c) + (bd_value_recode_result))) -> (((exists ff_h_bd_recode_result_new. ff_h_bd_recode_result_new + S (bd_value_recode_result) = S ((S (bd_index_recode_result)) * e)) /\ exists ff_q_bd_recode_result_new. z = ff_q_bd_recode_result_new * S ((S (bd_index_recode_result)) * e) + (bd_value_recode_result)))))
  8. 0008specialize binary_digit_code_recode_exists b
  9. 0009specialize binary_digit_code_recode_exists c
  10. 0010specialize binary_digit_code_recode_exists l
  11. 0011specialize binary_digit_code_recode_exists d
  12. 0012exact binary_digit_code_recode_exists
  13. 0013cases hcode
  14. 0014cases hcode_witness
  15. 0015cases hcode_witness_witness
  16. 0016exists x
  17. 0017exists x1
  18. 0018split
  19. 0019exact hcode_witness_witness_left
  20. 0020split
  21. 0021intro i
  22. 0022intro a
  23. 0023intro hbound
  24. 0024intro hentry
  25. 0025have hcases : i = l \/ exists gap. gap + S i = l
  26. 0026specialize finite_lt_succ_eq_or_lt l
  27. 0027specialize finite_lt_succ_eq_or_lt i
  28. 0028apply finite_lt_succ_eq_or_lt
  29. 0029exact hbound
  30. 0030cases hcases
  31. 0031rewrite hcases_left at hentry
  32. 0032rewrite hcases_left at hentry
  33. 0033have hlast : d = a
  34. 0034specialize beta_at_unique x
  35. 0035specialize beta_at_unique x1
  36. 0036specialize beta_at_unique l
  37. 0037specialize beta_at_unique d
  38. 0038specialize beta_at_unique a
  39. 0039apply beta_at_unique
  40. 0040exact hcode_witness_witness_left
  41. 0041exact hentry
  42. 0042have hlastbit : d = 0 \/ d = 1
  43. 0043exact hdigit
  44. 0044rewrite hlast at hlastbit
  45. 0045rewrite hlast at hlastbit
  46. 0046exact hlastbit
  47. 0047have hsource : exists value. (((exists ff_h_bd_append_source. ff_h_bd_append_source + S (value) = S ((S (i)) * c)) /\ exists ff_q_bd_append_source. b = ff_q_bd_append_source * S ((S (i)) * c) + (value)))
  48. 0048specialize beta_at_exists b
  49. 0049specialize beta_at_exists c
  50. 0050specialize beta_at_exists i
  51. 0051exact beta_at_exists
  52. 0052cases hsource
  53. 0053have htransport : (((exists ff_h_bd_append_transport. ff_h_bd_append_transport + S (x2) = S ((S (i)) * x1)) /\ exists ff_q_bd_append_transport. x = ff_q_bd_append_transport * S ((S (i)) * x1) + (x2)))
  54. 0054specialize hcode_witness_witness_right i
  55. 0055specialize hcode_witness_witness_right x2
  56. 0056apply hcode_witness_witness_right
  57. 0057exact hcases_right
  58. 0058exact hsource_witness
  59. 0059have holdvalue : x2 = a
  60. 0060specialize beta_at_unique x
  61. 0061specialize beta_at_unique x1
  62. 0062specialize beta_at_unique i
  63. 0063specialize beta_at_unique x2
  64. 0064specialize beta_at_unique a
  65. 0065apply beta_at_unique
  66. 0066exact htransport
  67. 0067exact hentry
  68. 0068have holdbit : x2 = 0 \/ x2 = 1
  69. 0069specialize hdigits i
  70. 0070specialize hdigits x2
  71. 0071apply hdigits
  72. 0072exact hcases_right
  73. 0073exact hsource_witness
  74. 0074rewrite holdvalue at holdbit
  75. 0075rewrite holdvalue at holdbit
  76. 0076exact holdbit
  77. 0077exact hcode_witness_witness_right