SL000M · theorem body

doubling_gauss_count_shape_from_initial_segment_complement

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

The existing initial-segment count and complementary BitCount theorems prove the exact doubling reflection-count shape once pointwise complementarity of the actual signs is supplied.

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

∀ h. ∀ k. ∀ sb. ∀ sc. ∀ ib. ∀ ic. ∀ e. h = 2 · k ∨ h = 2 · k + 1 → (∀ x. Lt(x,h) → ∃ y. BetaAt(ib,ic,x,y) ∧ (y = 1 ∧ Lt(x,k) ∨ y = 0 ∧ Lt(k,S x))) → BitCount(sb,sc,h,e) → (∀ x. ∀ y. ∀ z. Lt(x,h) → BetaAt(sb,sc,x,y) → BetaAt(ib,ic,x,z) → y = 0 ∧ z = 1 ∨ y = 1 ∧ z = 0) → h = 2 · e ∨ (∃ x. h = 2 · x + 1 ∧ e = S x)

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 PD0017 BitCount

In local proof propositions

PD0001 Le PD0017 BitCount
Exact expanded first-order statement
forall h k sb sc ib ic e. (((h = 2 * k) \/ (h = 2 * k + 1))) -> (forall eis_index_qst_initial_prefix. (exists eis_lt_gap_qst_initial_prefix_bound. eis_lt_gap_qst_initial_prefix_bound + S (eis_index_qst_initial_prefix) = h) -> exists eis_bit_qst_initial_prefix. ((((exists ff_h_eis_qst_initial_prefix_decoded. ff_h_eis_qst_initial_prefix_decoded + S (eis_bit_qst_initial_prefix) = S ((S (eis_index_qst_initial_prefix)) * ic)) /\ exists ff_q_eis_qst_initial_prefix_decoded. ib = ff_q_eis_qst_initial_prefix_decoded * S ((S (eis_index_qst_initial_prefix)) * ic) + (eis_bit_qst_initial_prefix))) /\ (((eis_bit_qst_initial_prefix = 1 /\ (exists eis_le_gap_qst_initial_prefix_choice_inside. eis_le_gap_qst_initial_prefix_choice_inside + (S eis_index_qst_initial_prefix) = k)) \/ (eis_bit_qst_initial_prefix = 0 /\ (exists eis_lt_gap_qst_initial_prefix_choice_outside. eis_lt_gap_qst_initial_prefix_choice_outside + S (k) = S eis_index_qst_initial_prefix)))))) -> (((exists ff_u_qst_sign_count_sum ff_v_qst_sign_count_sum. ((((exists ff_h_qst_sign_count_sum_start. ff_h_qst_sign_count_sum_start + S (0) = S ((S (0)) * ff_v_qst_sign_count_sum)) /\ exists ff_q_qst_sign_count_sum_start. ff_u_qst_sign_count_sum = ff_q_qst_sign_count_sum_start * S ((S (0)) * ff_v_qst_sign_count_sum) + (0))) /\ ((((exists ff_h_qst_sign_count_sum_terminal. ff_h_qst_sign_count_sum_terminal + S (e) = S ((S (h)) * ff_v_qst_sign_count_sum)) /\ exists ff_q_qst_sign_count_sum_terminal. ff_u_qst_sign_count_sum = ff_q_qst_sign_count_sum_terminal * S ((S (h)) * ff_v_qst_sign_count_sum) + (e))) /\ forall ff_i_qst_sign_count_sum. (exists ff_lt_qst_sign_count_sum_bound. ff_lt_qst_sign_count_sum_bound + S ff_i_qst_sign_count_sum = h) -> exists ff_a_qst_sign_count_sum ff_r_qst_sign_count_sum ff_s_qst_sign_count_sum. ((((exists ff_h_qst_sign_count_sum_summand. ff_h_qst_sign_count_sum_summand + S (ff_a_qst_sign_count_sum) = S ((S (ff_i_qst_sign_count_sum)) * sc)) /\ exists ff_q_qst_sign_count_sum_summand. sb = ff_q_qst_sign_count_sum_summand * S ((S (ff_i_qst_sign_count_sum)) * sc) + (ff_a_qst_sign_count_sum))) /\ ((((exists ff_h_qst_sign_count_sum_partial. ff_h_qst_sign_count_sum_partial + S (ff_r_qst_sign_count_sum) = S ((S (ff_i_qst_sign_count_sum)) * ff_v_qst_sign_count_sum)) /\ exists ff_q_qst_sign_count_sum_partial. ff_u_qst_sign_count_sum = ff_q_qst_sign_count_sum_partial * S ((S (ff_i_qst_sign_count_sum)) * ff_v_qst_sign_count_sum) + (ff_r_qst_sign_count_sum))) /\ ((((exists ff_h_qst_sign_count_sum_successor. ff_h_qst_sign_count_sum_successor + S (ff_s_qst_sign_count_sum) = S ((S (S ff_i_qst_sign_count_sum)) * ff_v_qst_sign_count_sum)) /\ exists ff_q_qst_sign_count_sum_successor. ff_u_qst_sign_count_sum = ff_q_qst_sign_count_sum_successor * S ((S (S ff_i_qst_sign_count_sum)) * ff_v_qst_sign_count_sum) + (ff_s_qst_sign_count_sum))) /\ ff_s_qst_sign_count_sum = ff_r_qst_sign_count_sum + ff_a_qst_sign_count_sum)))))) /\ (forall ff_i_qst_sign_count_bits. (exists ff_lt_qst_sign_count_bits_bound. ff_lt_qst_sign_count_bits_bound + S ff_i_qst_sign_count_bits = h) -> exists ff_bit_qst_sign_count_bits. ((((exists ff_h_qst_sign_count_bits_decoded. ff_h_qst_sign_count_bits_decoded + S (ff_bit_qst_sign_count_bits) = S ((S (ff_i_qst_sign_count_bits)) * sc)) /\ exists ff_q_qst_sign_count_bits_decoded. sb = ff_q_qst_sign_count_bits_decoded * S ((S (ff_i_qst_sign_count_bits)) * sc) + (ff_bit_qst_sign_count_bits))) /\ (ff_bit_qst_sign_count_bits = 0 \/ ff_bit_qst_sign_count_bits = 1))))) -> (forall i s t. (exists qst_complement_gap_count. qst_complement_gap_count + S i = h) -> (((exists ff_h_qst_count_sign. ff_h_qst_count_sign + S (s) = S ((S (i)) * sc)) /\ exists ff_q_qst_count_sign. sb = ff_q_qst_count_sign * S ((S (i)) * sc) + (s))) -> (((exists ff_h_qst_count_indicator. ff_h_qst_count_indicator + S (t) = S ((S (i)) * ic)) /\ exists ff_q_qst_count_indicator. ib = ff_q_qst_count_indicator * S ((S (i)) * ic) + (t))) -> ((s = 0 /\ t = 1) \/ (s = 1 /\ t = 0))) -> (((h = 2 * e) \/ (exists qst_count_half_shape. h = 2 * qst_count_half_shape + 1 /\ e = S qst_count_half_shape)))

Proof neighborhood

Direct theorem prerequisites

SL000L doubling_half_decomposition_lower_bound eisenstein_initial_segment_bit_count_exact · Alpha closed complementary_bit_counts_add_length · Alpha closed mul_comm · Stable closed zero_add · Stable closed add_succ_left · Stable closed add_right_cancel · Stable closed

Direct theorem dependents

SL000N doubling_gauss_reflection_count_shape

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

80 script commands · 20 reading checkpoints · 7 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)
doubling half decomposition lower bound
01Fix variables and assumptionsL1–10

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

  1. L1
    intro h
  2. L2
    intro k
  3. L3
    intro sb
  4. L4
    intro sc
  5. L5
    intro ib
  6. L6
    intro ic
  7. L7
    intro e
  8. L8
    intro hhalf
  9. L9
    intro hinitial
  10. L10
    intro hsigncount
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hcomplement
03Establish hboundL12–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply doubling half decomposition lower bound.

  1. L12
    have hbound : Le(k,h)Definitions: Le(k,h)Original native command in the exact edition
  2. L13
    specialize doubling_half_decomposition_lower_bound h
  3. L14
    specialize doubling_half_decomposition_lower_bound k
  4. L15
    apply doubling_half_decomposition_lower_bound
  5. L16
    exact hhalf
04Establish hinitialcountL17–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein initial segment bit count exact.

  1. L17
    have hinitialcount : BitCount(ib,ic,h,k)Definitions: BitCount(ib,ic,h,k)Original native command in the exact edition
  2. L18
    specialize eisenstein_initial_segment_bit_count_exact k
  3. L19
    specialize eisenstein_initial_segment_bit_count_exact ib
  4. L20
    specialize eisenstein_initial_segment_bit_count_exact ic
  5. L21
    specialize eisenstein_initial_segment_bit_count_exact h
  6. L22
    apply eisenstein_initial_segment_bit_count_exact
  7. L23
    exact hinitial
  8. L24
    exact hbound
05Establish hsumL25–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply complementary bit counts add length.

  1. L25
    have hsum : e + k = h
  2. L26
    specialize complementary_bit_counts_add_length sb
  3. L27
    specialize complementary_bit_counts_add_length sc
  4. L28
    specialize complementary_bit_counts_add_length ib
  5. L29
    specialize complementary_bit_counts_add_length ic
  6. L30
    specialize complementary_bit_counts_add_length h
  7. L31
    specialize complementary_bit_counts_add_length e
  8. L32
    specialize complementary_bit_counts_add_length k
  9. L33
    apply complementary_bit_counts_add_length
  10. L34
    exact hsigncount
06Use earlier factsL35–36

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

  1. L35
    exact hinitialcount
  2. L36
    exact hcomplement
07Establish hdoubleL37–42

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

  1. L37
    have hdouble : k + k = 2 * k
  2. L38
    trans k * 2
  3. L39
    simp [zero_add]
  4. L40
    specialize mul_comm k
  5. L41
    specialize mul_comm 2
  6. L42
    apply mul_comm
08Separate the logical casesL43–43

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

  1. L43
    cases hhalf
09Establish heqL44–53

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

  1. L44
    have heq : e = k
  2. L45
    specialize add_right_cancel e
  3. L46
    specialize add_right_cancel k
  4. L47
    specialize add_right_cancel k
  5. L48
    apply add_right_cancel
  6. L49
    trans h
  7. L50
    exact hsum
  8. L51
    trans 2 * k
  9. L52
    exact hhalf_left
  10. L53
    symm
10Use earlier factsL54–54

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

  1. L54
    exact hdouble
11Separate the logical casesL55–55

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

  1. L55
    left
12Calculate and transport equalitiesL56–56

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

  1. L56
    rewrite heq
13Use earlier factsL57–57

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

  1. L57
    exact hhalf_left
14Establish hsuccessorL58–64

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

  1. L58
    have hsuccessor : S k + k = 2 * k + 1
  2. L59
    trans S (k + k)
  3. L60
    apply add_succ_left
  4. L61
    trans S (2 * k)
  5. L62
    congr
  6. L63
    exact hdouble
  7. L64
    simp
15Establish heqL65–74

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

  1. L65
    have heq : e = S k
  2. L66
    specialize add_right_cancel e
  3. L67
    specialize add_right_cancel (S k)
  4. L68
    specialize add_right_cancel k
  5. L69
    apply add_right_cancel
  6. L70
    trans h
  7. L71
    exact hsum
  8. L72
    trans 2 * k + 1
  9. L73
    exact hhalf_right
  10. L74
    symm
16Use earlier factsL75–75

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

  1. L75
    exact hsuccessor
17Separate the logical casesL76–76

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

  1. L76
    right
18Construct an explicit witnessL77–77

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

  1. L77
    exists k
19Separate the logical casesL78–78

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

  1. L78
    split
20Use earlier factsL79–80

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

  1. L79
    exact hhalf_right
  2. L80
    exact heq

Library-wide reading audit

Original defined command ledger · 80 lines
  1. 0001intro h
  2. 0002intro k
  3. 0003intro sb
  4. 0004intro sc
  5. 0005intro ib
  6. 0006intro ic
  7. 0007intro e
  8. 0008intro hhalf
  9. 0009intro hinitial
  10. 0010intro hsigncount
  11. 0011intro hcomplement
  12. 0012have hbound : Le(k,h)
    Exact native replay linehave hbound : exists gap. gap + k = h
  13. 0013specialize doubling_half_decomposition_lower_bound h
  14. 0014specialize doubling_half_decomposition_lower_bound k
  15. 0015apply doubling_half_decomposition_lower_bound
  16. 0016exact hhalf
  17. 0017have hinitialcount : BitCount(ib,ic,h,k)
    Exact native replay linehave hinitialcount : ((exists ff_u_qst_initial_count_sum ff_v_qst_initial_count_sum. ((((exists ff_h_qst_initial_count_sum_start. ff_h_qst_initial_count_sum_start + S (0) = S ((S (0)) * ff_v_qst_initial_count_sum)) /\ exists ff_q_qst_initial_count_sum_start. ff_u_qst_initial_count_sum = ff_q_qst_initial_count_sum_start * S ((S (0)) * ff_v_qst_initial_count_sum) + (0))) /\ ((((exists ff_h_qst_initial_count_sum_terminal. ff_h_qst_initial_count_sum_terminal + S (k) = S ((S (h)) * ff_v_qst_initial_count_sum)) /\ exists ff_q_qst_initial_count_sum_terminal. ff_u_qst_initial_count_sum = ff_q_qst_initial_count_sum_terminal * S ((S (h)) * ff_v_qst_initial_count_sum) + (k))) /\ forall ff_i_qst_initial_count_sum. (exists ff_lt_qst_initial_count_sum_bound. ff_lt_qst_initial_count_sum_bound + S ff_i_qst_initial_count_sum = h) -> exists ff_a_qst_initial_count_sum ff_r_qst_initial_count_sum ff_s_qst_initial_count_sum. ((((exists ff_h_qst_initial_count_sum_summand. ff_h_qst_initial_count_sum_summand + S (ff_a_qst_initial_count_sum) = S ((S (ff_i_qst_initial_count_sum)) * ic)) /\ exists ff_q_qst_initial_count_sum_summand. ib = ff_q_qst_initial_count_sum_summand * S ((S (ff_i_qst_initial_count_sum)) * ic) + (ff_a_qst_initial_count_sum))) /\ ((((exists ff_h_qst_initial_count_sum_partial. ff_h_qst_initial_count_sum_partial + S (ff_r_qst_initial_count_sum) = S ((S (ff_i_qst_initial_count_sum)) * ff_v_qst_initial_count_sum)) /\ exists ff_q_qst_initial_count_sum_partial. ff_u_qst_initial_count_sum = ff_q_qst_initial_count_sum_partial * S ((S (ff_i_qst_initial_count_sum)) * ff_v_qst_initial_count_sum) + (ff_r_qst_initial_count_sum))) /\ ((((exists ff_h_qst_initial_count_sum_successor. ff_h_qst_initial_count_sum_successor + S (ff_s_qst_initial_count_sum) = S ((S (S ff_i_qst_initial_count_sum)) * ff_v_qst_initial_count_sum)) /\ exists ff_q_qst_initial_count_sum_successor. ff_u_qst_initial_count_sum = ff_q_qst_initial_count_sum_successor * S ((S (S ff_i_qst_initial_count_sum)) * ff_v_qst_initial_count_sum) + (ff_s_qst_initial_count_sum))) /\ ff_s_qst_initial_count_sum = ff_r_qst_initial_count_sum + ff_a_qst_initial_count_sum)))))) /\ (forall ff_i_qst_initial_count_bits. (exists ff_lt_qst_initial_count_bits_bound. ff_lt_qst_initial_count_bits_bound + S ff_i_qst_initial_count_bits = h) -> exists ff_bit_qst_initial_count_bits. ((((exists ff_h_qst_initial_count_bits_decoded. ff_h_qst_initial_count_bits_decoded + S (ff_bit_qst_initial_count_bits) = S ((S (ff_i_qst_initial_count_bits)) * ic)) /\ exists ff_q_qst_initial_count_bits_decoded. ib = ff_q_qst_initial_count_bits_decoded * S ((S (ff_i_qst_initial_count_bits)) * ic) + (ff_bit_qst_initial_count_bits))) /\ (ff_bit_qst_initial_count_bits = 0 \/ ff_bit_qst_initial_count_bits = 1))))
  18. 0018specialize eisenstein_initial_segment_bit_count_exact k
  19. 0019specialize eisenstein_initial_segment_bit_count_exact ib
  20. 0020specialize eisenstein_initial_segment_bit_count_exact ic
  21. 0021specialize eisenstein_initial_segment_bit_count_exact h
  22. 0022apply eisenstein_initial_segment_bit_count_exact
  23. 0023exact hinitial
  24. 0024exact hbound
  25. 0025have hsum : e + k = h
  26. 0026specialize complementary_bit_counts_add_length sb
  27. 0027specialize complementary_bit_counts_add_length sc
  28. 0028specialize complementary_bit_counts_add_length ib
  29. 0029specialize complementary_bit_counts_add_length ic
  30. 0030specialize complementary_bit_counts_add_length h
  31. 0031specialize complementary_bit_counts_add_length e
  32. 0032specialize complementary_bit_counts_add_length k
  33. 0033apply complementary_bit_counts_add_length
  34. 0034exact hsigncount
  35. 0035exact hinitialcount
  36. 0036exact hcomplement
  37. 0037have hdouble : k + k = 2 * k
  38. 0038trans k * 2
  39. 0039simp [zero_add]
  40. 0040specialize mul_comm k
  41. 0041specialize mul_comm 2
  42. 0042apply mul_comm
  43. 0043cases hhalf
  44. 0044have heq : e = k
  45. 0045specialize add_right_cancel e
  46. 0046specialize add_right_cancel k
  47. 0047specialize add_right_cancel k
  48. 0048apply add_right_cancel
  49. 0049trans h
  50. 0050exact hsum
  51. 0051trans 2 * k
  52. 0052exact hhalf_left
  53. 0053symm
  54. 0054exact hdouble
  55. 0055left
  56. 0056rewrite heq
  57. 0057exact hhalf_left
  58. 0058have hsuccessor : S k + k = 2 * k + 1
  59. 0059trans S (k + k)
  60. 0060apply add_succ_left
  61. 0061trans S (2 * k)
  62. 0062congr
  63. 0063exact hdouble
  64. 0064simp
  65. 0065have heq : e = S k
  66. 0066specialize add_right_cancel e
  67. 0067specialize add_right_cancel (S k)
  68. 0068specialize add_right_cancel k
  69. 0069apply add_right_cancel
  70. 0070trans h
  71. 0071exact hsum
  72. 0072trans 2 * k + 1
  73. 0073exact hhalf_right
  74. 0074symm
  75. 0075exact hsuccessor
  76. 0076right
  77. 0077exists k
  78. 0078split
  79. 0079exact hhalf_right
  80. 0080exact heq