BE0002

binary_digit_prefix_restrict

Every valid successor-length binary digit prefix has a valid predecessor prefix.

Alpha v34 checked-use · first admitted v22 · 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.

G102 was OPEN at this family's Alpha-v22 first admission: complete execution was proved only for a supplied valid beta-coded digit prefix. G102 is now CLOSED in Alpha v23 for every arbitrary exponent, with actual canonical digits and operations≤3*BitLen(e)+2.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ l. BinaryDigitPrefix(b,c,S l) → BinaryDigitPrefix(b,c,l)

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

Definition DAG

BinaryDigitPrefix(d,s,n) · 2

Actual proof prerequisites

le_succ · checked external prerequisite
Original expanded first-order statement 
forall b c l. (forall ff_index_be_prefix_next ff_digit_be_prefix_next. (exists ff_lt_be_prefix_next_bound. ff_lt_be_prefix_next_bound + S ff_index_be_prefix_next = S l) -> (((exists ff_h_be_prefix_next_digit. ff_h_be_prefix_next_digit + S (ff_digit_be_prefix_next) = S ((S (ff_index_be_prefix_next)) * c)) /\ exists ff_q_be_prefix_next_digit. b = ff_q_be_prefix_next_digit * S ((S (ff_index_be_prefix_next)) * c) + (ff_digit_be_prefix_next))) -> (ff_digit_be_prefix_next = 0 \/ ff_digit_be_prefix_next = 1)) -> (forall ff_index_be_prefix ff_digit_be_prefix. (exists ff_lt_be_prefix_bound. ff_lt_be_prefix_bound + S ff_index_be_prefix = l) -> (((exists ff_h_be_prefix_digit. ff_h_be_prefix_digit + S (ff_digit_be_prefix) = S ((S (ff_index_be_prefix)) * c)) /\ exists ff_q_be_prefix_digit. b = ff_q_be_prefix_digit * S ((S (ff_index_be_prefix)) * c) + (ff_digit_be_prefix))) -> (ff_digit_be_prefix = 0 \/ ff_digit_be_prefix = 1))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

16 script commands · 2 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.

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 hnext
  5. L5
    intro i
  6. L6
    intro d
  7. L7
    intro hi
  8. L8
    intro hat
02Use earlier factsL9–16

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

  1. L9
    specialize hnext i
  2. L10
    specialize hnext d
  3. L11
    apply hnext
  4. L12
    specialize le_succ (S i)
  5. L13
    specialize le_succ l
  6. L14
    apply le_succ
  7. L15
    exact hi
  8. L16
    exact hat

Library-wide reading audit

Original defined command ledger · 16 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro hnext
  5. 0005intro i
  6. 0006intro d
  7. 0007intro hi
  8. 0008intro hat
  9. 0009specialize hnext i
  10. 0010specialize hnext d
  11. 0011apply hnext
  12. 0012specialize le_succ (S i)
  13. 0013specialize le_succ l
  14. 0014apply le_succ
  15. 0015exact hi
  16. 0016exact hat