BT00T3

beta_pascal_zero_row_exists

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

Every finite width has a beta-coded Pascal zero row.

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 PA statement

forall w. exists b c. (forall bcf_index_bpzrx_result. (exists bcf_lt_gap_bpzrx_result_bound. bcf_lt_gap_bpzrx_result_bound + S (bcf_index_bpzrx_result) = w) -> exists bcf_value_bpzrx_result. ((((exists bcf_height_bpzrx_result_entry. bcf_height_bpzrx_result_entry + S (bcf_value_bpzrx_result) = S ((S (bcf_index_bpzrx_result)) * c)) /\ exists bcf_quotient_bpzrx_result_entry. b = bcf_quotient_bpzrx_result_entry * S ((S (bcf_index_bpzrx_result)) * c) + (bcf_value_bpzrx_result))) /\ ((bcf_index_bpzrx_result = 0 /\ bcf_value_bpzrx_result = 1) \/ exists bcf_predecessor_bpzrx_result. bcf_index_bpzrx_result = S bcf_predecessor_bpzrx_result /\ bcf_value_bpzrx_result = 0)))

Structural proof guide

Every finite width has a beta-coded Pascal zero row.

Direct prerequisites: add_eq_zero_right, succ_ne_zero, beta_pascal_zero_row_extend. The authored body proceeds by structural induction (1), case analysis (3), intermediate claims (3).

Proof neighborhood

Direct dependencies

BT000L add_eq_zero_right BT000C succ_ne_zero BT00T2 beta_pascal_zero_row_extend

Direct dependents

BT00T6 beta_pascal_table_prefix_extend

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

26 script commands · 8 reading checkpoints · 3 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.

Named ingredients (3)
add eq zero rightsucc ne zerobeta pascal zero row extend

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.

01Induction on wL1–1

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L1
    induction w
02Construct an explicit witnessL2–3

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

  1. L2
    exists 0
  2. L3
    exists 0
03Fix variables and assumptionsL4–5

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

  1. L4
    intro i
  2. L5
    intro hi
04Separate the logical casesL6–7

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

  1. L6
    exfalso
  2. L7
    cases hi
05Establish hsiL8–15

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

  1. L8
    have hsi : S i = 0
  2. L9
    specialize add_eq_zero_right x
  3. L10
    specialize add_eq_zero_right (S i)
  4. L11
    apply add_eq_zero_right
  5. L12
    exact hi_witness
  6. L13
    specialize succ_ne_zero i
  7. L14
    apply succ_ne_zero
  8. L15
    exact hsi
06Establish hpreviousL16–17

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

  1. L16
    have hprevious : ∃ b. ∃ c. ∀ x. Lt(x,w) → ∃ y. BetaAt(b,c,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))Definitions: LtBetaAt
  2. L17
    exact IH
07Separate the logical casesL18–19

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

  1. L18
    cases hprevious
  2. L19
    cases hprevious_witness
08Establish hnextL20–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta pascal zero row extend.

  1. L20
    have hnext : ∃ b. ∃ c. ∀ x. Lt(x,S w) → ∃ y. BetaAt(b,c,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))Definitions: LtBetaAt
  2. L21
    specialize beta_pascal_zero_row_extend x
  3. L22
    specialize beta_pascal_zero_row_extend x1
  4. L23
    specialize beta_pascal_zero_row_extend w
  5. L24
    apply beta_pascal_zero_row_extend
  6. L25
    exact hprevious_witness_witness
  7. L26
    exact hnext

Library-wide reading audit

Original exact command ledger · 26 lines
  1. 0001induction w
  2. 0002exists 0
  3. 0003exists 0
  4. 0004intro i
  5. 0005intro hi
  6. 0006exfalso
  7. 0007cases hi
  8. 0008have hsi : S i = 0
  9. 0009specialize add_eq_zero_right x
  10. 0010specialize add_eq_zero_right (S i)
  11. 0011apply add_eq_zero_right
  12. 0012exact hi_witness
  13. 0013specialize succ_ne_zero i
  14. 0014apply succ_ne_zero
  15. 0015exact hsi
  16. 0016have hprevious : exists b c. (forall bcf_index_bpzrx_previous. (exists bcf_lt_gap_bpzrx_previous_bound. bcf_lt_gap_bpzrx_previous_bound + S (bcf_index_bpzrx_previous) = w) -> exists bcf_value_bpzrx_previous. ((((exists bcf_height_bpzrx_previous_entry. bcf_height_bpzrx_previous_entry + S (bcf_value_bpzrx_previous) = S ((S (bcf_index_bpzrx_previous)) * c)) /\ exists bcf_quotient_bpzrx_previous_entry. b = bcf_quotient_bpzrx_previous_entry * S ((S (bcf_index_bpzrx_previous)) * c) + (bcf_value_bpzrx_previous))) /\ ((bcf_index_bpzrx_previous = 0 /\ bcf_value_bpzrx_previous = 1) \/ exists bcf_predecessor_bpzrx_previous. bcf_index_bpzrx_previous = S bcf_predecessor_bpzrx_previous /\ bcf_value_bpzrx_previous = 0)))
  17. 0017exact IH
  18. 0018cases hprevious
  19. 0019cases hprevious_witness
  20. 0020have hnext : exists b c. (forall bcf_index_bpzrx_successor. (exists bcf_lt_gap_bpzrx_successor_bound. bcf_lt_gap_bpzrx_successor_bound + S (bcf_index_bpzrx_successor) = S (w)) -> exists bcf_value_bpzrx_successor. ((((exists bcf_height_bpzrx_successor_entry. bcf_height_bpzrx_successor_entry + S (bcf_value_bpzrx_successor) = S ((S (bcf_index_bpzrx_successor)) * c)) /\ exists bcf_quotient_bpzrx_successor_entry. b = bcf_quotient_bpzrx_successor_entry * S ((S (bcf_index_bpzrx_successor)) * c) + (bcf_value_bpzrx_successor))) /\ ((bcf_index_bpzrx_successor = 0 /\ bcf_value_bpzrx_successor = 1) \/ exists bcf_predecessor_bpzrx_successor. bcf_index_bpzrx_successor = S bcf_predecessor_bpzrx_successor /\ bcf_value_bpzrx_successor = 0)))
  21. 0021specialize beta_pascal_zero_row_extend x
  22. 0022specialize beta_pascal_zero_row_extend x1
  23. 0023specialize beta_pascal_zero_row_extend w
  24. 0024apply beta_pascal_zero_row_extend
  25. 0025exact hprevious_witness_witness
  26. 0026exact hnext