BT00XY · Bertrand theorem

double_quotient_carry_prefix_all_bits

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

Every value in a carry prefix is zero or one.

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.

Statement with defined notation

∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ l. (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. BetaAt(b,c,x,y) ∧ (BetaAt(d,e,x,z) ∧ (BetaAt(f,g,x,n) ∧ (n = 0 ∧ z = y + y ∨ n = 1 ∧ z = S (y + y))))) → AllBits(f,g,l)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt PD0016 AllBits

5 occurrences

In local proof propositions

PD0013 BetaAt

3 occurrences

Exact expanded native-PA statement
forall b c d e f g l. (forall b5cc_index_b5ccpab_source. (exists bcf_lt_gap_b5ccpab_source_bound. bcf_lt_gap_b5ccpab_source_bound + S (b5cc_index_b5ccpab_source) = l) -> exists b5cc_left_b5ccpab_source b5cc_right_b5ccpab_source b5cc_bit_b5ccpab_source. (((exists fs_h_b5cc_b5ccpab_source_left. fs_h_b5cc_b5ccpab_source_left + S (b5cc_left_b5ccpab_source) = S ((S (b5cc_index_b5ccpab_source)) * c)) /\ exists fs_q_b5cc_b5ccpab_source_left. b = fs_q_b5cc_b5ccpab_source_left * S ((S (b5cc_index_b5ccpab_source)) * c) + (b5cc_left_b5ccpab_source))) /\ ((((exists fs_h_b5cc_b5ccpab_source_right. fs_h_b5cc_b5ccpab_source_right + S (b5cc_right_b5ccpab_source) = S ((S (b5cc_index_b5ccpab_source)) * e)) /\ exists fs_q_b5cc_b5ccpab_source_right. d = fs_q_b5cc_b5ccpab_source_right * S ((S (b5cc_index_b5ccpab_source)) * e) + (b5cc_right_b5ccpab_source))) /\ ((((exists fs_h_b5cc_b5ccpab_source_bit. fs_h_b5cc_b5ccpab_source_bit + S (b5cc_bit_b5ccpab_source) = S ((S (b5cc_index_b5ccpab_source)) * g)) /\ exists fs_q_b5cc_b5ccpab_source_bit. f = fs_q_b5cc_b5ccpab_source_bit * S ((S (b5cc_index_b5ccpab_source)) * g) + (b5cc_bit_b5ccpab_source))) /\ (((b5cc_bit_b5ccpab_source = 0 /\ b5cc_right_b5ccpab_source = b5cc_left_b5ccpab_source + b5cc_left_b5ccpab_source) \/ (b5cc_bit_b5ccpab_source = 1 /\ b5cc_right_b5ccpab_source = S (b5cc_left_b5ccpab_source + b5cc_left_b5ccpab_source))))))) -> (forall ff_i_b5ccpab_result. (exists ff_lt_b5ccpab_result_bound. ff_lt_b5ccpab_result_bound + S ff_i_b5ccpab_result = l) -> exists ff_bit_b5ccpab_result. ((((exists ff_h_b5ccpab_result_decoded. ff_h_b5ccpab_result_decoded + S (ff_bit_b5ccpab_result) = S ((S (ff_i_b5ccpab_result)) * g)) /\ exists ff_q_b5ccpab_result_decoded. f = ff_q_b5ccpab_result_decoded * S ((S (ff_i_b5ccpab_result)) * g) + (ff_bit_b5ccpab_result))) /\ (ff_bit_b5ccpab_result = 0 \/ ff_bit_b5ccpab_result = 1)))

Proof neighborhood

Direct theorem prerequisites

none

Direct theorem dependents

BT00Y4 central_binom_carry_bit_count

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

30 script commands · 10 reading checkpoints · 1 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 d
  4. L4
    intro e
  5. L5
    intro f
  6. L6
    intro g
  7. L7
    intro l
  8. L8
    intro hprefix
  9. L9
    intro i
  10. L10
    intro hi
02Establish hpointL11–14

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

  1. L11
    have hpoint : ∃ q. ∃ Q. ∃ bit. BetaAt(b,c,i,q) ∧ (BetaAt(d,e,i,Q) ∧ (BetaAt(f,g,i,bit) ∧ (bit = 0 ∧ Q = q + q ∨ bit = 1 ∧ Q = S (q + q))))Definitions: BetaAt(b,c,i,q)BetaAt(d,e,i,Q)BetaAt(f,g,i,bit)Original native command in the exact edition
  2. L12
    specialize hprefix i
  3. L13
    apply hprefix
  4. L14
    exact hi
03Separate the logical casesL15–20

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

  1. L15
    cases hpoint
  2. L16
    cases hpoint_witness
  3. L17
    cases hpoint_witness_witness
  4. L18
    cases hpoint_witness_witness_witness
  5. L19
    cases hpoint_witness_witness_witness_right
  6. L20
    cases hpoint_witness_witness_witness_right_right
04Construct an explicit witnessL21–21

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

  1. L21
    exists x2
05Separate the logical casesL22–22

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

  1. L22
    split
06Use earlier factsL23–23

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

  1. L23
    exact hpoint_witness_witness_witness_right_right_left
07Separate the logical casesL24–26

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

  1. L24
    cases hpoint_witness_witness_witness_right_right_right
  2. L25
    cases hpoint_witness_witness_witness_right_right_right_left
  3. L26
    left
08Use earlier factsL27–27

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

  1. L27
    exact hpoint_witness_witness_witness_right_right_right_left_left
09Separate the logical casesL28–29

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

  1. L28
    cases hpoint_witness_witness_witness_right_right_right_right
  2. L29
    right
10Use earlier factsL30–30

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

  1. L30
    exact hpoint_witness_witness_witness_right_right_right_right_left

Library-wide reading audit

Original defined command ledger · 30 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro f
  6. 0006intro g
  7. 0007intro l
  8. 0008intro hprefix
  9. 0009intro i
  10. 0010intro hi
  11. 0011have hpoint : ∃ q. ∃ Q. ∃ bit. BetaAt(b,c,i,q) ∧ (BetaAt(d,e,i,Q) ∧ (BetaAt(f,g,i,bit) ∧ (bit = 0 ∧ Q = q + q ∨ bit = 1 ∧ Q = S (q + q))))
    Exact native replay linehave hpoint : exists q Q bit. (((exists fs_h_b5ccpab_point_left. fs_h_b5ccpab_point_left + S (q) = S ((S (i)) * c)) /\ exists fs_q_b5ccpab_point_left. b = fs_q_b5ccpab_point_left * S ((S (i)) * c) + (q))) /\ ((((exists fs_h_b5ccpab_point_right. fs_h_b5ccpab_point_right + S (Q) = S ((S (i)) * e)) /\ exists fs_q_b5ccpab_point_right. d = fs_q_b5ccpab_point_right * S ((S (i)) * e) + (Q))) /\ ((((exists fs_h_b5ccpab_point_bit. fs_h_b5ccpab_point_bit + S (bit) = S ((S (i)) * g)) /\ exists fs_q_b5ccpab_point_bit. f = fs_q_b5ccpab_point_bit * S ((S (i)) * g) + (bit))) /\ (((bit = 0 /\ Q = q + q) \/ (bit = 1 /\ Q = S (q + q))))))
  12. 0012specialize hprefix i
  13. 0013apply hprefix
  14. 0014exact hi
  15. 0015cases hpoint
  16. 0016cases hpoint_witness
  17. 0017cases hpoint_witness_witness
  18. 0018cases hpoint_witness_witness_witness
  19. 0019cases hpoint_witness_witness_witness_right
  20. 0020cases hpoint_witness_witness_witness_right_right
  21. 0021exists x2
  22. 0022split
  23. 0023exact hpoint_witness_witness_witness_right_right_left
  24. 0024cases hpoint_witness_witness_witness_right_right_right
  25. 0025cases hpoint_witness_witness_witness_right_right_right_left
  26. 0026left
  27. 0027exact hpoint_witness_witness_witness_right_right_right_left_left
  28. 0028cases hpoint_witness_witness_witness_right_right_right_right
  29. 0029right
  30. 0030exact hpoint_witness_witness_witness_right_right_right_right_left