CD0004

finite_bit_subset_pointwise_le

Actual subset inclusion gives pointwise monotonicity of the characteristic bits.

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

Sets are complete characteristic-bit codes with actual finite cardinality witnesses. The proof constructs translations and the sumset; no finite-choice oracle, supplied cardinality conclusion, or unproved polynomial-method premise is used.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ d. ∀ e. ∀ l. AllBits(b,c,l) → ModularSetSubset(b,c,d,e,l) → ∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(d,e,x,z) → Le(y,z)

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

Definition DAG

ModularSetSubset(b,c,d,e,p) · 1Le(a,b) · 1Lt(a,b) · 1BetaAt(b,c,i,x) · 3AllBits(b,c,l) · 1

Actual proof prerequisites

finite_bit_entry_casesbeta_at_unique · checked external prerequisitele_refl · checked external prerequisite
Original expanded first-order statement 
forall b c d e l. (forall ff_i_fms_bits. (exists ff_lt_fms_bits_bound. ff_lt_fms_bits_bound + S ff_i_fms_bits = (l)) -> exists ff_bit_fms_bits. ((((exists ff_h_fms_bits_decoded. ff_h_fms_bits_decoded + S (ff_bit_fms_bits) = S ((S (ff_i_fms_bits)) * (c))) /\ exists ff_q_fms_bits_decoded. (b) = ff_q_fms_bits_decoded * S ((S (ff_i_fms_bits)) * (c)) + (ff_bit_fms_bits))) /\ (ff_bit_fms_bits = 0 \/ ff_bit_fms_bits = 1))) -> (forall fms_i_subset. (exists fms_gap_subset. fms_gap_subset + S (fms_i_subset) = (l)) -> (((exists fs_h_fms_subset_left. fs_h_fms_subset_left + S (1) = S ((S (fms_i_subset)) * c)) /\ exists fs_q_fms_subset_left. b = fs_q_fms_subset_left * S ((S (fms_i_subset)) * c) + (1))) -> (((exists fs_h_fms_subset_right. fs_h_fms_subset_right + S (1) = S ((S (fms_i_subset)) * e)) /\ exists fs_q_fms_subset_right. d = fs_q_fms_subset_right * S ((S (fms_i_subset)) * e) + (1)))) -> (forall fms_i_le fms_a_le fms_v_le. (exists fms_gap_le. fms_gap_le + S (fms_i_le) = (l)) -> (((exists fs_h_fms_le_left. fs_h_fms_le_left + S (fms_a_le) = S ((S (fms_i_le)) * c)) /\ exists fs_q_fms_le_left. b = fs_q_fms_le_left * S ((S (fms_i_le)) * c) + (fms_a_le))) -> (((exists fs_h_fms_le_right. fs_h_fms_le_right + S (fms_v_le) = S ((S (fms_i_le)) * e)) /\ exists fs_q_fms_le_right. d = fs_q_fms_le_right * S ((S (fms_i_le)) * e) + (fms_v_le))) -> (exists fms_gap_le. fms_gap_le + (fms_a_le) = (fms_v_le)))

Complete tactic proof in conservative notation

All 47 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

47 script commands · 11 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.

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)
finite bit entry cases
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 l
  6. L6
    intro hbits
  7. L7
    intro hsub
  8. L8
    intro i
  9. L9
    intro a
  10. L10
    intro v
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hi
  2. L12
    intro ha
  3. L13
    intro hv
03Establish hcaseL14–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite bit entry cases.

  1. L14
    have hcase : a=0 \/ a=1
  2. L15
    specialize finite_bit_entry_cases b
  3. L16
    specialize finite_bit_entry_cases c
  4. L17
    specialize finite_bit_entry_cases l
  5. L18
    specialize finite_bit_entry_cases i
  6. L19
    specialize finite_bit_entry_cases a
  7. L20
    apply finite_bit_entry_cases
  8. L21
    exact hbits
  9. L22
    exact hi
  10. L23
    exact ha
04Separate the logical casesL24–24

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

  1. L24
    cases hcase
05Calculate and transport equalitiesL25–25

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

  1. L25
    rewrite hcase_left
06Construct an explicit witnessL26–26

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

  1. L26
    exists v
07Calculate and transport equalitiesL27–27

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

  1. L27
    simp
08Establish honeL28–34

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

  1. L28
    have hone : BetaAt(d,e,i,1)Definitions: BetaAt(d,e,i,1)Original native command in the exact edition
  2. L29
    specialize hsub i
  3. L30
    apply hsub
  4. L31
    exact hi
  5. L32
    rewrite hcase_right at ha
  6. L33
    rewrite hcase_right at ha
  7. L34
    exact ha
09Establish heqL35–44

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

  1. L35
    have heq : v=1
  2. L36
    specialize beta_at_unique d
  3. L37
    specialize beta_at_unique e
  4. L38
    specialize beta_at_unique i
  5. L39
    specialize beta_at_unique v
  6. L40
    specialize beta_at_unique 1
  7. L41
    apply beta_at_unique
  8. L42
    exact hv
  9. L43
    exact hone
  10. L44
    rewrite hcase_right
10Calculate and transport equalitiesL45–45

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

  1. L45
    rewrite heq
11Use earlier factsL46–47

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

  1. L46
    specialize le_refl 1
  2. L47
    apply le_refl

Library-wide reading audit

Original defined command ledger · 47 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro l
  6. 0006intro hbits
  7. 0007intro hsub
  8. 0008intro i
  9. 0009intro a
  10. 0010intro v
  11. 0011intro hi
  12. 0012intro ha
  13. 0013intro hv
  14. 0014have hcase : a=0 \/ a=1
  15. 0015specialize finite_bit_entry_cases b
  16. 0016specialize finite_bit_entry_cases c
  17. 0017specialize finite_bit_entry_cases l
  18. 0018specialize finite_bit_entry_cases i
  19. 0019specialize finite_bit_entry_cases a
  20. 0020apply finite_bit_entry_cases
  21. 0021exact hbits
  22. 0022exact hi
  23. 0023exact ha
  24. 0024cases hcase
  25. 0025rewrite hcase_left
  26. 0026exists v
  27. 0027simp
  28. 0028have hone : BetaAt(d,e,i,1)
  29. 0029specialize hsub i
  30. 0030apply hsub
  31. 0031exact hi
  32. 0032rewrite hcase_right at ha
  33. 0033rewrite hcase_right at ha
  34. 0034exact ha
  35. 0035have heq : v=1
  36. 0036specialize beta_at_unique d
  37. 0037specialize beta_at_unique e
  38. 0038specialize beta_at_unique i
  39. 0039specialize beta_at_unique v
  40. 0040specialize beta_at_unique 1
  41. 0041apply beta_at_unique
  42. 0042exact hv
  43. 0043exact hone
  44. 0044rewrite hcase_right
  45. 0045rewrite heq
  46. 0046specialize le_refl 1
  47. 0047apply le_refl