KU0009 · theorem body

add_quotient_carry_prefix_all_bits

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

Every value decoded from a general additive 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

∀ lb. ∀ lc. ∀ rb. ∀ rc. ∀ tb. ∀ tc. ∀ cb. ∀ cc. ∀ l. (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. ∃ m. BetaAt(lb,lc,x,y) ∧ (BetaAt(rb,rc,x,z) ∧ (BetaAt(tb,tc,x,n) ∧ (BetaAt(cb,cc,x,m) ∧ (m = 0 ∧ n = y + z ∨ m = 1 ∧ n = S (y + z)))))) → AllBits(cb,cc,l)

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt PD0016 AllBits

In local proof propositions

PD0013 BetaAt
Exact expanded first-order statement
forall lb lc rb rc tb tc cb cc l. (forall kmc_index_kmcpab_source. (exists bcf_lt_gap_kmcpab_source_bound. bcf_lt_gap_kmcpab_source_bound + S (kmc_index_kmcpab_source) = l) -> exists kmc_left_kmcpab_source kmc_right_kmcpab_source kmc_total_kmcpab_source kmc_bit_kmcpab_source. (((exists fs_h_kmcpab_source_left. fs_h_kmcpab_source_left + S (kmc_left_kmcpab_source) = S ((S (kmc_index_kmcpab_source)) * lc)) /\ exists fs_q_kmcpab_source_left. lb = fs_q_kmcpab_source_left * S ((S (kmc_index_kmcpab_source)) * lc) + (kmc_left_kmcpab_source))) /\ ((((exists fs_h_kmcpab_source_right. fs_h_kmcpab_source_right + S (kmc_right_kmcpab_source) = S ((S (kmc_index_kmcpab_source)) * rc)) /\ exists fs_q_kmcpab_source_right. rb = fs_q_kmcpab_source_right * S ((S (kmc_index_kmcpab_source)) * rc) + (kmc_right_kmcpab_source))) /\ ((((exists fs_h_kmcpab_source_total. fs_h_kmcpab_source_total + S (kmc_total_kmcpab_source) = S ((S (kmc_index_kmcpab_source)) * tc)) /\ exists fs_q_kmcpab_source_total. tb = fs_q_kmcpab_source_total * S ((S (kmc_index_kmcpab_source)) * tc) + (kmc_total_kmcpab_source))) /\ ((((exists fs_h_kmcpab_source_bit. fs_h_kmcpab_source_bit + S (kmc_bit_kmcpab_source) = S ((S (kmc_index_kmcpab_source)) * cc)) /\ exists fs_q_kmcpab_source_bit. cb = fs_q_kmcpab_source_bit * S ((S (kmc_index_kmcpab_source)) * cc) + (kmc_bit_kmcpab_source))) /\ (((kmc_bit_kmcpab_source = 0 /\ kmc_total_kmcpab_source = kmc_left_kmcpab_source + kmc_right_kmcpab_source) \/ (kmc_bit_kmcpab_source = 1 /\ kmc_total_kmcpab_source = S (kmc_left_kmcpab_source + kmc_right_kmcpab_source)))))))) -> (forall ff_i_kmcpab_result. (exists ff_lt_kmcpab_result_bound. ff_lt_kmcpab_result_bound + S ff_i_kmcpab_result = l) -> exists ff_bit_kmcpab_result. ((((exists ff_h_kmcpab_result_decoded. ff_h_kmcpab_result_decoded + S (ff_bit_kmcpab_result) = S ((S (ff_i_kmcpab_result)) * cc)) /\ exists ff_q_kmcpab_result_decoded. cb = ff_q_kmcpab_result_decoded * S ((S (ff_i_kmcpab_result)) * cc) + (ff_bit_kmcpab_result))) /\ (ff_bit_kmcpab_result = 0 \/ ff_bit_kmcpab_result = 1)))

Proof neighborhood

Direct theorem prerequisites

none

Direct theorem dependents

KU000C kummer_binomial_carry_bit_count

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

34 script commands · 11 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 lb
  2. L2
    intro lc
  3. L3
    intro rb
  4. L4
    intro rc
  5. L5
    intro tb
  6. L6
    intro tc
  7. L7
    intro cb
  8. L8
    intro cc
  9. L9
    intro l
  10. L10
    intro hprefix
02Fix variables and assumptionsL11–12

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

  1. L11
    intro i
  2. L12
    intro hi
03Establish hpointL13–16

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

  1. L13
    have hpoint : ∃ q. ∃ s. ∃ Q. ∃ bit. BetaAt(lb,lc,i,q) ∧ (BetaAt(rb,rc,i,s) ∧ (BetaAt(tb,tc,i,Q) ∧ (BetaAt(cb,cc,i,bit) ∧ (bit = 0 ∧ Q = q + s ∨ bit = 1 ∧ Q = S (q + s)))))Definitions: BetaAt(lb,lc,i,q)BetaAt(rb,rc,i,s)BetaAt(tb,tc,i,Q)BetaAt(cb,cc,i,bit)Original native command in the exact edition
  2. L14
    specialize hprefix i
  3. L15
    apply hprefix
  4. L16
    exact hi
04Separate the logical casesL17–24

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

  1. L17
    cases hpoint
  2. L18
    cases hpoint_witness
  3. L19
    cases hpoint_witness_witness
  4. L20
    cases hpoint_witness_witness_witness
  5. L21
    cases hpoint_witness_witness_witness_witness
  6. L22
    cases hpoint_witness_witness_witness_witness_right
  7. L23
    cases hpoint_witness_witness_witness_witness_right_right
  8. L24
    cases hpoint_witness_witness_witness_witness_right_right_right
05Construct an explicit witnessL25–25

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

  1. L25
    exists x3
06Separate the logical casesL26–26

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

  1. L26
    split
07Use earlier factsL27–27

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

  1. L27
    exact hpoint_witness_witness_witness_witness_right_right_right_left
08Separate the logical casesL28–30

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

  1. L28
    cases hpoint_witness_witness_witness_witness_right_right_right_right
  2. L29
    cases hpoint_witness_witness_witness_witness_right_right_right_right_left
  3. L30
    left
09Use earlier factsL31–31

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

  1. L31
    exact hpoint_witness_witness_witness_witness_right_right_right_right_left_left
10Separate the logical casesL32–33

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

  1. L32
    cases hpoint_witness_witness_witness_witness_right_right_right_right_right
  2. L33
    right
11Use earlier factsL34–34

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

  1. L34
    exact hpoint_witness_witness_witness_witness_right_right_right_right_right_left

Library-wide reading audit

Original defined command ledger · 34 lines
  1. 0001intro lb
  2. 0002intro lc
  3. 0003intro rb
  4. 0004intro rc
  5. 0005intro tb
  6. 0006intro tc
  7. 0007intro cb
  8. 0008intro cc
  9. 0009intro l
  10. 0010intro hprefix
  11. 0011intro i
  12. 0012intro hi
  13. 0013have hpoint : ∃ q. ∃ s. ∃ Q. ∃ bit. BetaAt(lb,lc,i,q) ∧ (BetaAt(rb,rc,i,s) ∧ (BetaAt(tb,tc,i,Q) ∧ (BetaAt(cb,cc,i,bit) ∧ (bit = 0 ∧ Q = q + s ∨ bit = 1 ∧ Q = S (q + s)))))
    Exact native replay linehave hpoint : exists q s Q bit. (((exists fs_h_kmcpab_point_left. fs_h_kmcpab_point_left + S (q) = S ((S (i)) * lc)) /\ exists fs_q_kmcpab_point_left. lb = fs_q_kmcpab_point_left * S ((S (i)) * lc) + (q))) /\ ((((exists fs_h_kmcpab_point_right. fs_h_kmcpab_point_right + S (s) = S ((S (i)) * rc)) /\ exists fs_q_kmcpab_point_right. rb = fs_q_kmcpab_point_right * S ((S (i)) * rc) + (s))) /\ ((((exists fs_h_kmcpab_point_total. fs_h_kmcpab_point_total + S (Q) = S ((S (i)) * tc)) /\ exists fs_q_kmcpab_point_total. tb = fs_q_kmcpab_point_total * S ((S (i)) * tc) + (Q))) /\ ((((exists fs_h_kmcpab_point_bit. fs_h_kmcpab_point_bit + S (bit) = S ((S (i)) * cc)) /\ exists fs_q_kmcpab_point_bit. cb = fs_q_kmcpab_point_bit * S ((S (i)) * cc) + (bit))) /\ (((bit = 0 /\ Q = q + s) \/ (bit = 1 /\ Q = S (q + s)))))))
  14. 0014specialize hprefix i
  15. 0015apply hprefix
  16. 0016exact hi
  17. 0017cases hpoint
  18. 0018cases hpoint_witness
  19. 0019cases hpoint_witness_witness
  20. 0020cases hpoint_witness_witness_witness
  21. 0021cases hpoint_witness_witness_witness_witness
  22. 0022cases hpoint_witness_witness_witness_witness_right
  23. 0023cases hpoint_witness_witness_witness_witness_right_right
  24. 0024cases hpoint_witness_witness_witness_witness_right_right_right
  25. 0025exists x3
  26. 0026split
  27. 0027exact hpoint_witness_witness_witness_witness_right_right_right_left
  28. 0028cases hpoint_witness_witness_witness_witness_right_right_right_right
  29. 0029cases hpoint_witness_witness_witness_witness_right_right_right_right_left
  30. 0030left
  31. 0031exact hpoint_witness_witness_witness_witness_right_right_right_right_left_left
  32. 0032cases hpoint_witness_witness_witness_witness_right_right_right_right_right
  33. 0033right
  34. 0034exact hpoint_witness_witness_witness_witness_right_right_right_right_right_left