SL000K · theorem body

doubling_gauss_initial_segment_complement

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

For multiplication by two, every actual Gauss sign bit is exactly complementary to the floor-half initial-segment bit.

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

∀ p. ∀ h. ∀ a. ∀ b. ∀ c. ∀ mb. ∀ mc. ∀ sb. ∀ sc. ∀ ib. ∀ ic. ∀ k. p = 2 · h + 1 → a = 2 → h = 2 · k ∨ h = 2 · k + 1 → Range(b,c,1,h) → (∀ x. Lt(x,h) → ∃ y. ∃ z. ∃ n. BetaAt(b,c,x,y) ∧ (BetaAt(mb,mc,x,z) ∧ (BetaAt(sb,sc,x,n) ∧ (Lt(0,z) ∧ (Le(z,h) ∧ ((n = 0 ∨ n = 1) ∧ (n = 0 ∧ ModEq(p,a · y,z) ∨ n = 1 ∧ ModEq(p,a · y,2 · h · z)))))))) → (∀ x. Lt(x,h) → ∃ y. BetaAt(ib,ic,x,y) ∧ (y = 1 ∧ Lt(x,k) ∨ y = 0 ∧ Lt(k,S x))) → ∀ x. ∀ y. ∀ z. Lt(x,h) → BetaAt(sb,sc,x,y) → BetaAt(ib,ic,x,z) → y = 0 ∧ z = 1 ∨ y = 1 ∧ z = 0

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

PD0001 Le PD0002 Lt PD0008 ModEq PD0013 BetaAt PD0018 Range

In local proof propositions

PD0001 Le PD0002 Lt PD0008 ModEq PD0013 BetaAt
Exact expanded first-order statement
forall p h a b c mb mc sb sc ib ic k. p = 2 * h + 1 -> a = 2 -> ((h = 2 * k) \/ (h = 2 * k + 1)) -> (forall gsp_range_index_qst_goal_half. (exists gsp_lt_gap_qst_goal_half_range_bound. gsp_lt_gap_qst_goal_half_range_bound + S gsp_range_index_qst_goal_half = h) -> (((exists gsp_beta_height_qst_goal_half_range_entry. gsp_beta_height_qst_goal_half_range_entry + S (1 + gsp_range_index_qst_goal_half) = S ((S (gsp_range_index_qst_goal_half)) * c)) /\ exists gsp_beta_quotient_qst_goal_half_range_entry. b = gsp_beta_quotient_qst_goal_half_range_entry * S ((S (gsp_range_index_qst_goal_half)) * c) + (1 + gsp_range_index_qst_goal_half)))) -> (forall gsp_index_qst_goal_signed. (exists gsp_lt_gap_qst_goal_signed_index_bound. gsp_lt_gap_qst_goal_signed_index_bound + S gsp_index_qst_goal_signed = h) -> (exists gsp_value_qst_goal_signed_entry gsp_magnitude_qst_goal_signed_entry gsp_sign_qst_goal_signed_entry. (((exists ff_h_gsp_qst_goal_signed_entry_source. ff_h_gsp_qst_goal_signed_entry_source + S (gsp_value_qst_goal_signed_entry) = S ((S (gsp_index_qst_goal_signed)) * c)) /\ exists ff_q_gsp_qst_goal_signed_entry_source. b = ff_q_gsp_qst_goal_signed_entry_source * S ((S (gsp_index_qst_goal_signed)) * c) + (gsp_value_qst_goal_signed_entry))) /\ ((((exists ff_h_gsp_qst_goal_signed_entry_magnitude. ff_h_gsp_qst_goal_signed_entry_magnitude + S (gsp_magnitude_qst_goal_signed_entry) = S ((S (gsp_index_qst_goal_signed)) * mc)) /\ exists ff_q_gsp_qst_goal_signed_entry_magnitude. mb = ff_q_gsp_qst_goal_signed_entry_magnitude * S ((S (gsp_index_qst_goal_signed)) * mc) + (gsp_magnitude_qst_goal_signed_entry))) /\ ((((exists ff_h_gsp_qst_goal_signed_entry_sign. ff_h_gsp_qst_goal_signed_entry_sign + S (gsp_sign_qst_goal_signed_entry) = S ((S (gsp_index_qst_goal_signed)) * sc)) /\ exists ff_q_gsp_qst_goal_signed_entry_sign. sb = ff_q_gsp_qst_goal_signed_entry_sign * S ((S (gsp_index_qst_goal_signed)) * sc) + (gsp_sign_qst_goal_signed_entry))) /\ ((exists gsp_lt_gap_qst_goal_signed_entry_positive. gsp_lt_gap_qst_goal_signed_entry_positive + S 0 = gsp_magnitude_qst_goal_signed_entry) /\ ((exists gsp_le_gap_qst_goal_signed_entry_bounded. gsp_le_gap_qst_goal_signed_entry_bounded + gsp_magnitude_qst_goal_signed_entry = h) /\ ((gsp_sign_qst_goal_signed_entry = 0 \/ gsp_sign_qst_goal_signed_entry = 1) /\ (((gsp_sign_qst_goal_signed_entry = 0 /\ (exists gsp_mod_left_qst_goal_signed_entry_lower gsp_mod_right_qst_goal_signed_entry_lower. (a * gsp_value_qst_goal_signed_entry) + p * gsp_mod_left_qst_goal_signed_entry_lower = (gsp_magnitude_qst_goal_signed_entry) + p * gsp_mod_right_qst_goal_signed_entry_lower)) \/ (gsp_sign_qst_goal_signed_entry = 1 /\ (exists gsp_mod_left_qst_goal_signed_entry_reflected gsp_mod_right_qst_goal_signed_entry_reflected. (a * gsp_value_qst_goal_signed_entry) + p * gsp_mod_left_qst_goal_signed_entry_reflected = ((2 * h) * gsp_magnitude_qst_goal_signed_entry) + p * gsp_mod_right_qst_goal_signed_entry_reflected))))))))))) -> (forall eis_index_qst_goal_initial. (exists eis_lt_gap_qst_goal_initial_bound. eis_lt_gap_qst_goal_initial_bound + S (eis_index_qst_goal_initial) = h) -> exists eis_bit_qst_goal_initial. ((((exists ff_h_eis_qst_goal_initial_decoded. ff_h_eis_qst_goal_initial_decoded + S (eis_bit_qst_goal_initial) = S ((S (eis_index_qst_goal_initial)) * ic)) /\ exists ff_q_eis_qst_goal_initial_decoded. ib = ff_q_eis_qst_goal_initial_decoded * S ((S (eis_index_qst_goal_initial)) * ic) + (eis_bit_qst_goal_initial))) /\ (((eis_bit_qst_goal_initial = 1 /\ (exists eis_le_gap_qst_goal_initial_choice_inside. eis_le_gap_qst_goal_initial_choice_inside + (S eis_index_qst_goal_initial) = k)) \/ (eis_bit_qst_goal_initial = 0 /\ (exists eis_lt_gap_qst_goal_initial_choice_outside. eis_lt_gap_qst_goal_initial_choice_outside + S (k) = S eis_index_qst_goal_initial)))))) -> (forall i s t. (exists qst_complement_gap_goal. qst_complement_gap_goal + S i = h) -> (((exists ff_h_qst_goal_sign. ff_h_qst_goal_sign + S (s) = S ((S (i)) * sc)) /\ exists ff_q_qst_goal_sign. sb = ff_q_qst_goal_sign * S ((S (i)) * sc) + (s))) -> (((exists ff_h_qst_goal_indicator. ff_h_qst_goal_indicator + S (t) = S ((S (i)) * ic)) /\ exists ff_q_qst_goal_indicator. ib = ff_q_qst_goal_indicator * S ((S (i)) * ic) + (t))) -> ((s = 0 /\ t = 1) \/ (s = 1 /\ t = 0)))

Proof neighborhood

Direct theorem prerequisites

beta_range_entry_eq · Stable closed beta_at_unique · Stable closed eisenstein_initial_segment_decoded_choice · Alpha closed SL000I doubling_half_range_below_odd_modulus odd_signed_division_branch_exact · Alpha closed SL000H doubling_floor_above_implies_double_above_half SL000G doubling_floor_below_implies_double_at_most_half SL000J reflected_double_above_odd_half lt_not_le · Stable closed zero_add · Stable closed add_succ_left · 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

167 script commands · 31 reading checkpoints · 12 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 (4)
doubling half range below odd modulusdoubling floor above implies double above halfdoubling floor below implies double at most halfreflected double above odd half
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro a
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro mb
  7. L7
    intro mc
  8. L8
    intro sb
  9. L9
    intro sc
  10. L10
    intro ib
02Fix variables and assumptionsL11–20

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

  1. L11
    intro ic
  2. L12
    intro k
  3. L13
    intro hpodd
  4. L14
    intro hatwo
  5. L15
    intro hhalf
  6. L16
    intro hrange
  7. L17
    intro hsigned
  8. L18
    intro hinitial
  9. L19
    intro i
  10. L20
    intro s
03Fix variables and assumptionsL21–24

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

  1. L21
    intro t
  2. L22
    intro hibound
  3. L23
    intro hsign
  4. L24
    intro hindicator
04Establish hentryL25–28

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

  1. L25
    have hentry : ∃ gsp_value_qst_alignment. ∃ gsp_magnitude_qst_alignment. ∃ gsp_sign_qst_alignment. BetaAt(b,c,i,gsp_value_qst_alignment) ∧ (BetaAt(mb,mc,i,gsp_magnitude_qst_alignment) ∧ (BetaAt(sb,sc,i,gsp_sign_qst_alignment) ∧ (Lt(0,gsp_magnitude_qst_alignment) ∧ (Le(gsp_magnitude_qst_alignment,h) ∧ ((gsp_sign_qst_alignment = 0 ∨ gsp_sign_qst_alignment = 1) ∧ (gsp_sign_qst_alignment = 0 ∧ ModEq(p,a · gsp_value_qst_alignment,gsp_magnitude_qst_alignment) ∨ gsp_sign_qst_alignment = 1 ∧ ModEq(p,a · gsp_value_qst_alignment,2 · h · gsp_magnitude_qst_alignment)))))))Definitions: BetaAt(b,c,i,gsp_value_qst_alignment)BetaAt(mb,mc,i,gsp_magnitude_qst_alignment)BetaAt(sb,sc,i,gsp_sign_qst_alignment)Lt(0,gsp_magnitude_qst_alignment)Le(gsp_magnitude_qst_alignment,h)ModEq(p,a · gsp_value_qst_alignment,gsp_magnitude_qst_alignment)ModEq(p,a · gsp_value_qst_alignment,2 · h · gsp_magnitude_qst_alignment)Original native command in the exact edition
  2. L26
    specialize hsigned i
  3. L27
    apply hsigned
  4. L28
    exact hibound
05Separate the logical casesL29–37

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

  1. L29
    cases hentry
  2. L30
    cases hentry_witness
  3. L31
    cases hentry_witness_witness
  4. L32
    cases hentry_witness_witness_witness
  5. L33
    cases hentry_witness_witness_witness_right
  6. L34
    cases hentry_witness_witness_witness_right_right
  7. L35
    cases hentry_witness_witness_witness_right_right_right
  8. L36
    cases hentry_witness_witness_witness_right_right_right_right
  9. L37
    cases hentry_witness_witness_witness_right_right_right_right_right
06Establish hsourceL38–47

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

  1. L38
    have hsource : x = 1 + i
  2. L39
    specialize beta_range_entry_eq b
  3. L40
    specialize beta_range_entry_eq c
  4. L41
    specialize beta_range_entry_eq 1
  5. L42
    specialize beta_range_entry_eq h
  6. L43
    specialize beta_range_entry_eq i
  7. L44
    specialize beta_range_entry_eq x
  8. L45
    apply beta_range_entry_eq
  9. L46
    exact hrange
  10. L47
    exact hibound
07Use earlier factsL48–48

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

  1. L48
    exact hentry_witness_witness_witness_left
08Establish hsource_succL49–55

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

  1. L49
    have hsource_succ : x = S i
  2. L50
    trans 1 + i
  3. L51
    exact hsource
  4. L52
    trans S (0 + i)
  5. L53
    apply add_succ_left
  6. L54
    congr
  7. L55
    apply zero_add
09Establish hsource_boundL56–58

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

  1. L56
    have hsource_bound : Le(x,h)Definitions: Le(x,h)Original native command in the exact edition
  2. L57
    rewrite hsource_succ
  3. L58
    exact hibound
10Establish hdoubled_boundL59–65

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply doubling half range below odd modulus.

  1. L59
    have hdoubled_bound : Lt(2 · x,p)Definitions: Lt(2 · x,p)Original native command in the exact edition
  2. L60
    specialize doubling_half_range_below_odd_modulus p
  3. L61
    specialize doubling_half_range_below_odd_modulus h
  4. L62
    specialize doubling_half_range_below_odd_modulus x
  5. L63
    apply doubling_half_range_below_odd_modulus
  6. L64
    exact hpodd
  7. L65
    exact hsource_bound
11Establish hsame_signL66–74

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

  1. L66
    have hsame_sign : x2 = s
  2. L67
    specialize beta_at_unique sb
  3. L68
    specialize beta_at_unique sc
  4. L69
    specialize beta_at_unique i
  5. L70
    specialize beta_at_unique x2
  6. L71
    specialize beta_at_unique s
  7. L72
    apply beta_at_unique
  8. L73
    exact hentry_witness_witness_witness_right_right_left
  9. L74
    exact hsign
12Establish hchoiceL75–84

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

  1. L75
    have hchoice : t = 1 ∧ Lt(i,k) ∨ t = 0 ∧ Lt(k,S i)Definitions: Lt(i,k)Lt(k,S i)Original native command in the exact edition
  2. L76
    specialize eisenstein_initial_segment_decoded_choice k
  3. L77
    specialize eisenstein_initial_segment_decoded_choice ib
  4. L78
    specialize eisenstein_initial_segment_decoded_choice ic
  5. L79
    specialize eisenstein_initial_segment_decoded_choice h
  6. L80
    specialize eisenstein_initial_segment_decoded_choice i
  7. L81
    specialize eisenstein_initial_segment_decoded_choice t
  8. L82
    apply eisenstein_initial_segment_decoded_choice
  9. L83
    exact hinitial
  10. L84
    exact hibound
13Use earlier factsL85–85

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

  1. L85
    exact hindicator
14Establish hexactL86–95

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd signed division branch exact.

  1. L86
    have hexact : ((x2 = 0 /\ 2 * x = x1) \/ (x2 = 1 /\ 2 * x + x1 = p))
  2. L87
    specialize odd_signed_division_branch_exact p
  3. L88
    specialize odd_signed_division_branch_exact h
  4. L89
    specialize odd_signed_division_branch_exact (2 * x)
  5. L90
    specialize odd_signed_division_branch_exact 0
  6. L91
    specialize odd_signed_division_branch_exact (2 * x)
  7. L92
    specialize odd_signed_division_branch_exact x1
  8. L93
    specialize odd_signed_division_branch_exact x2
  9. L94
    apply odd_signed_division_branch_exact
  10. L95
    exact hpodd
15Calculate and transport equalitiesL96–97

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

  1. L96
    simp
  2. L97
    symm
16Use earlier factsL98–101

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

  1. L98
    apply zero_add
  2. L99
    exact hdoubled_bound
  3. L100
    exact hentry_witness_witness_witness_right_right_right_left
  4. L101
    exact hentry_witness_witness_witness_right_right_right_right_left
17Calculate and transport equalitiesL102–103

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

  1. L102
    rewrite hatwo at hentry_witness_witness_witness_right_right_right_right_right_right
  2. L103
    rewrite hatwo at hentry_witness_witness_witness_right_right_right_right_right_right
18Use earlier factsL104–104

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

  1. L104
    exact hentry_witness_witness_witness_right_right_right_right_right_right
19Separate the logical casesL105–110

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

  1. L105
    cases hexact
  2. L106
    cases hexact_left
  3. L107
    cases hchoice
  4. L108
    cases hchoice_left
  5. L109
    left
  6. L110
    split
20Calculate and transport equalitiesL111–112

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

  1. L111
    trans x2
  2. L112
    symm
21Use earlier factsL113–115

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

  1. L113
    exact hsame_sign
  2. L114
    exact hexact_left_left
  3. L115
    exact hchoice_left_left
22Separate the logical casesL116–117

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

  1. L116
    cases hchoice_right
  2. L117
    exfalso
23Establish haboveL118–125

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply doubling floor above implies double above half.

  1. L118
    have habove : Lt(h,2 · x)Definitions: Lt(h,2 · x)Original native command in the exact edition
  2. L119
    specialize doubling_floor_above_implies_double_above_half h
  3. L120
    specialize doubling_floor_above_implies_double_above_half k
  4. L121
    specialize doubling_floor_above_implies_double_above_half x
  5. L122
    apply doubling_floor_above_implies_double_above_half
  6. L123
    exact hhalf
  7. L124
    rewrite hsource_succ
  8. L125
    exact hchoice_right_right
24Establish hbelowL126–133

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

  1. L126
    have hbelow : Le(2 · x,h)Definitions: Le(2 · x,h)Original native command in the exact edition
  2. L127
    rewrite hexact_left_right
  3. L128
    exact hentry_witness_witness_witness_right_right_right_right_left
  4. L129
    specialize lt_not_le h
  5. L130
    specialize lt_not_le (2 * x)
  6. L131
    apply lt_not_le
  7. L132
    exact habove
  8. L133
    exact hbelow
25Separate the logical casesL134–137

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

  1. L134
    cases hexact_right
  2. L135
    cases hchoice
  3. L136
    cases hchoice_left
  4. L137
    exfalso
26Establish hbelowL138–145

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply doubling floor below implies double at most half.

  1. L138
    have hbelow : Le(2 · x,h)Definitions: Le(2 · x,h)Original native command in the exact edition
  2. L139
    specialize doubling_floor_below_implies_double_at_most_half h
  3. L140
    specialize doubling_floor_below_implies_double_at_most_half k
  4. L141
    specialize doubling_floor_below_implies_double_at_most_half x
  5. L142
    apply doubling_floor_below_implies_double_at_most_half
  6. L143
    exact hhalf
  7. L144
    rewrite hsource_succ
  8. L145
    exact hchoice_left_right
27Establish haboveL146–155

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply reflected double above odd half.

  1. L146
    have habove : Lt(h,2 · x)Definitions: Lt(h,2 · x)Original native command in the exact edition
  2. L147
    specialize reflected_double_above_odd_half p
  3. L148
    specialize reflected_double_above_odd_half h
  4. L149
    specialize reflected_double_above_odd_half x
  5. L150
    specialize reflected_double_above_odd_half x1
  6. L151
    apply reflected_double_above_odd_half
  7. L152
    exact hpodd
  8. L153
    exact hentry_witness_witness_witness_right_right_right_right_left
  9. L154
    exact hexact_right_right
  10. L155
    specialize lt_not_le h
28Use earlier factsL156–159

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

  1. L156
    specialize lt_not_le (2 * x)
  2. L157
    apply lt_not_le
  3. L158
    exact habove
  4. L159
    exact hbelow
29Separate the logical casesL160–162

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

  1. L160
    cases hchoice_right
  2. L161
    right
  3. L162
    split
30Calculate and transport equalitiesL163–164

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

  1. L163
    trans x2
  2. L164
    symm
31Use earlier factsL165–167

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

  1. L165
    exact hsame_sign
  2. L166
    exact hexact_right_left
  3. L167
    exact hchoice_right_left

Library-wide reading audit

Original defined command ledger · 167 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro a
  4. 0004intro b
  5. 0005intro c
  6. 0006intro mb
  7. 0007intro mc
  8. 0008intro sb
  9. 0009intro sc
  10. 0010intro ib
  11. 0011intro ic
  12. 0012intro k
  13. 0013intro hpodd
  14. 0014intro hatwo
  15. 0015intro hhalf
  16. 0016intro hrange
  17. 0017intro hsigned
  18. 0018intro hinitial
  19. 0019intro i
  20. 0020intro s
  21. 0021intro t
  22. 0022intro hibound
  23. 0023intro hsign
  24. 0024intro hindicator
  25. 0025have hentry : ∃ gsp_value_qst_alignment. ∃ gsp_magnitude_qst_alignment. ∃ gsp_sign_qst_alignment. BetaAt(b,c,i,gsp_value_qst_alignment) ∧ (BetaAt(mb,mc,i,gsp_magnitude_qst_alignment) ∧ (BetaAt(sb,sc,i,gsp_sign_qst_alignment) ∧ (Lt(0,gsp_magnitude_qst_alignment) ∧ (Le(gsp_magnitude_qst_alignment,h) ∧ ((gsp_sign_qst_alignment = 0 ∨ gsp_sign_qst_alignment = 1) ∧ (gsp_sign_qst_alignment = 0 ∧ ModEq(p,a · gsp_value_qst_alignment,gsp_magnitude_qst_alignment) ∨ gsp_sign_qst_alignment = 1 ∧ ModEq(p,a · gsp_value_qst_alignment,2 · h · gsp_magnitude_qst_alignment)))))))
    Exact native replay linehave hentry : exists gsp_value_qst_alignment gsp_magnitude_qst_alignment gsp_sign_qst_alignment. (((exists ff_h_gsp_qst_alignment_source. ff_h_gsp_qst_alignment_source + S (gsp_value_qst_alignment) = S ((S (i)) * c)) /\ exists ff_q_gsp_qst_alignment_source. b = ff_q_gsp_qst_alignment_source * S ((S (i)) * c) + (gsp_value_qst_alignment))) /\ ((((exists ff_h_gsp_qst_alignment_magnitude. ff_h_gsp_qst_alignment_magnitude + S (gsp_magnitude_qst_alignment) = S ((S (i)) * mc)) /\ exists ff_q_gsp_qst_alignment_magnitude. mb = ff_q_gsp_qst_alignment_magnitude * S ((S (i)) * mc) + (gsp_magnitude_qst_alignment))) /\ ((((exists ff_h_gsp_qst_alignment_sign. ff_h_gsp_qst_alignment_sign + S (gsp_sign_qst_alignment) = S ((S (i)) * sc)) /\ exists ff_q_gsp_qst_alignment_sign. sb = ff_q_gsp_qst_alignment_sign * S ((S (i)) * sc) + (gsp_sign_qst_alignment))) /\ ((exists gsp_lt_gap_qst_alignment_positive. gsp_lt_gap_qst_alignment_positive + S 0 = gsp_magnitude_qst_alignment) /\ ((exists gsp_le_gap_qst_alignment_bounded. gsp_le_gap_qst_alignment_bounded + gsp_magnitude_qst_alignment = h) /\ ((gsp_sign_qst_alignment = 0 \/ gsp_sign_qst_alignment = 1) /\ (((gsp_sign_qst_alignment = 0 /\ (exists gsp_mod_left_qst_alignment_lower gsp_mod_right_qst_alignment_lower. (a * gsp_value_qst_alignment) + p * gsp_mod_left_qst_alignment_lower = (gsp_magnitude_qst_alignment) + p * gsp_mod_right_qst_alignment_lower)) \/ (gsp_sign_qst_alignment = 1 /\ (exists gsp_mod_left_qst_alignment_reflected gsp_mod_right_qst_alignment_reflected. (a * gsp_value_qst_alignment) + p * gsp_mod_left_qst_alignment_reflected = ((2 * h) * gsp_magnitude_qst_alignment) + p * gsp_mod_right_qst_alignment_reflected)))))))))
  26. 0026specialize hsigned i
  27. 0027apply hsigned
  28. 0028exact hibound
  29. 0029cases hentry
  30. 0030cases hentry_witness
  31. 0031cases hentry_witness_witness
  32. 0032cases hentry_witness_witness_witness
  33. 0033cases hentry_witness_witness_witness_right
  34. 0034cases hentry_witness_witness_witness_right_right
  35. 0035cases hentry_witness_witness_witness_right_right_right
  36. 0036cases hentry_witness_witness_witness_right_right_right_right
  37. 0037cases hentry_witness_witness_witness_right_right_right_right_right
  38. 0038have hsource : x = 1 + i
  39. 0039specialize beta_range_entry_eq b
  40. 0040specialize beta_range_entry_eq c
  41. 0041specialize beta_range_entry_eq 1
  42. 0042specialize beta_range_entry_eq h
  43. 0043specialize beta_range_entry_eq i
  44. 0044specialize beta_range_entry_eq x
  45. 0045apply beta_range_entry_eq
  46. 0046exact hrange
  47. 0047exact hibound
  48. 0048exact hentry_witness_witness_witness_left
  49. 0049have hsource_succ : x = S i
  50. 0050trans 1 + i
  51. 0051exact hsource
  52. 0052trans S (0 + i)
  53. 0053apply add_succ_left
  54. 0054congr
  55. 0055apply zero_add
  56. 0056have hsource_bound : Le(x,h)
    Exact native replay linehave hsource_bound : exists gap. gap + x = h
  57. 0057rewrite hsource_succ
  58. 0058exact hibound
  59. 0059have hdoubled_bound : Lt(2 · x,p)
    Exact native replay linehave hdoubled_bound : exists gap. gap + S (2 * x) = p
  60. 0060specialize doubling_half_range_below_odd_modulus p
  61. 0061specialize doubling_half_range_below_odd_modulus h
  62. 0062specialize doubling_half_range_below_odd_modulus x
  63. 0063apply doubling_half_range_below_odd_modulus
  64. 0064exact hpodd
  65. 0065exact hsource_bound
  66. 0066have hsame_sign : x2 = s
  67. 0067specialize beta_at_unique sb
  68. 0068specialize beta_at_unique sc
  69. 0069specialize beta_at_unique i
  70. 0070specialize beta_at_unique x2
  71. 0071specialize beta_at_unique s
  72. 0072apply beta_at_unique
  73. 0073exact hentry_witness_witness_witness_right_right_left
  74. 0074exact hsign
  75. 0075have hchoice : t = 1 ∧ Lt(i,k) ∨ t = 0 ∧ Lt(k,S i)
    Exact native replay linehave hchoice : ((t = 1 /\ (exists eis_le_gap_qst_alignment_choice_inside. eis_le_gap_qst_alignment_choice_inside + (S i) = k)) \/ (t = 0 /\ (exists eis_lt_gap_qst_alignment_choice_outside. eis_lt_gap_qst_alignment_choice_outside + S (k) = S i)))
  76. 0076specialize eisenstein_initial_segment_decoded_choice k
  77. 0077specialize eisenstein_initial_segment_decoded_choice ib
  78. 0078specialize eisenstein_initial_segment_decoded_choice ic
  79. 0079specialize eisenstein_initial_segment_decoded_choice h
  80. 0080specialize eisenstein_initial_segment_decoded_choice i
  81. 0081specialize eisenstein_initial_segment_decoded_choice t
  82. 0082apply eisenstein_initial_segment_decoded_choice
  83. 0083exact hinitial
  84. 0084exact hibound
  85. 0085exact hindicator
  86. 0086have hexact : ((x2 = 0 /\ 2 * x = x1) \/ (x2 = 1 /\ 2 * x + x1 = p))
  87. 0087specialize odd_signed_division_branch_exact p
  88. 0088specialize odd_signed_division_branch_exact h
  89. 0089specialize odd_signed_division_branch_exact (2 * x)
  90. 0090specialize odd_signed_division_branch_exact 0
  91. 0091specialize odd_signed_division_branch_exact (2 * x)
  92. 0092specialize odd_signed_division_branch_exact x1
  93. 0093specialize odd_signed_division_branch_exact x2
  94. 0094apply odd_signed_division_branch_exact
  95. 0095exact hpodd
  96. 0096simp
  97. 0097symm
  98. 0098apply zero_add
  99. 0099exact hdoubled_bound
  100. 0100exact hentry_witness_witness_witness_right_right_right_left
  101. 0101exact hentry_witness_witness_witness_right_right_right_right_left
  102. 0102rewrite hatwo at hentry_witness_witness_witness_right_right_right_right_right_right
  103. 0103rewrite hatwo at hentry_witness_witness_witness_right_right_right_right_right_right
  104. 0104exact hentry_witness_witness_witness_right_right_right_right_right_right
  105. 0105cases hexact
  106. 0106cases hexact_left
  107. 0107cases hchoice
  108. 0108cases hchoice_left
  109. 0109left
  110. 0110split
  111. 0111trans x2
  112. 0112symm
  113. 0113exact hsame_sign
  114. 0114exact hexact_left_left
  115. 0115exact hchoice_left_left
  116. 0116cases hchoice_right
  117. 0117exfalso
  118. 0118have habove : Lt(h,2 · x)
    Exact native replay linehave habove : exists gap. gap + S h = 2 * x
  119. 0119specialize doubling_floor_above_implies_double_above_half h
  120. 0120specialize doubling_floor_above_implies_double_above_half k
  121. 0121specialize doubling_floor_above_implies_double_above_half x
  122. 0122apply doubling_floor_above_implies_double_above_half
  123. 0123exact hhalf
  124. 0124rewrite hsource_succ
  125. 0125exact hchoice_right_right
  126. 0126have hbelow : Le(2 · x,h)
    Exact native replay linehave hbelow : exists gap. gap + 2 * x = h
  127. 0127rewrite hexact_left_right
  128. 0128exact hentry_witness_witness_witness_right_right_right_right_left
  129. 0129specialize lt_not_le h
  130. 0130specialize lt_not_le (2 * x)
  131. 0131apply lt_not_le
  132. 0132exact habove
  133. 0133exact hbelow
  134. 0134cases hexact_right
  135. 0135cases hchoice
  136. 0136cases hchoice_left
  137. 0137exfalso
  138. 0138have hbelow : Le(2 · x,h)
    Exact native replay linehave hbelow : exists gap. gap + 2 * x = h
  139. 0139specialize doubling_floor_below_implies_double_at_most_half h
  140. 0140specialize doubling_floor_below_implies_double_at_most_half k
  141. 0141specialize doubling_floor_below_implies_double_at_most_half x
  142. 0142apply doubling_floor_below_implies_double_at_most_half
  143. 0143exact hhalf
  144. 0144rewrite hsource_succ
  145. 0145exact hchoice_left_right
  146. 0146have habove : Lt(h,2 · x)
    Exact native replay linehave habove : exists gap. gap + S h = 2 * x
  147. 0147specialize reflected_double_above_odd_half p
  148. 0148specialize reflected_double_above_odd_half h
  149. 0149specialize reflected_double_above_odd_half x
  150. 0150specialize reflected_double_above_odd_half x1
  151. 0151apply reflected_double_above_odd_half
  152. 0152exact hpodd
  153. 0153exact hentry_witness_witness_witness_right_right_right_right_left
  154. 0154exact hexact_right_right
  155. 0155specialize lt_not_le h
  156. 0156specialize lt_not_le (2 * x)
  157. 0157apply lt_not_le
  158. 0158exact habove
  159. 0159exact hbelow
  160. 0160cases hchoice_right
  161. 0161right
  162. 0162split
  163. 0163trans x2
  164. 0164symm
  165. 0165exact hsame_sign
  166. 0166exact hexact_right_left
  167. 0167exact hchoice_right_left