PA00CP · theorem

gauss_eisenstein_prefix_pointwise_mod_two

Alpha v34 checked-use theorem · independently closed; not Stable

Aligned Gauss and Eisenstein prefixes satisfy x == q+m+s modulo two pointwise.

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. ∀ tb. ∀ tc. ∀ qb. ∀ qc. ∀ rb. ∀ rc. ∀ mb. ∀ mc. ∀ sb. ∀ sc. p = 2 · h + 1 → Odd(a) → Range(b,c,1,h) → (∀ x. ∀ y. Lt(x,h) → BetaAt(tb,tc,x,y) → y = a · (1 + x)) → DivisionPrefix(p,tb,tc,qb,qc,rb,rc,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. ∀ y. ∀ z. ∀ n. ∀ m. Lt(x,h) → BetaAt(b,c,x,y) → BetaAt(qb,qc,x,z) → BetaAt(mb,mc,x,n) → BetaAt(sb,sc,x,m) → ModEq(2,y,z + n + m)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0001 Le PD0002 Lt PD0008 ModEq PD0010 Odd PD0013 BetaAt PD0018 Range PD0040 DivisionPrefix

19 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0007 DivRem PD0008 ModEq PD0013 BetaAt

17 occurrences

Exact expanded native-PA statement
forall p h a b c tb tc qb qc rb rc mb mc sb sc. p = 2 * h + 1 -> (exists sdp_odd_gep_scale. a = 2 * sdp_odd_gep_scale + 1) -> (forall gsp_range_index_gep_half. (exists gsp_lt_gap_gep_half_range_bound. gsp_lt_gap_gep_half_range_bound + S gsp_range_index_gep_half = h) -> (((exists gsp_beta_height_gep_half_range_entry. gsp_beta_height_gep_half_range_entry + S (1 + gsp_range_index_gep_half) = S ((S (gsp_range_index_gep_half)) * c)) /\ exists gsp_beta_quotient_gep_half_range_entry. b = gsp_beta_quotient_gep_half_range_entry * S ((S (gsp_range_index_gep_half)) * c) + (1 + gsp_range_index_gep_half)))) -> (forall esd_index_gep_scaled esd_value_gep_scaled. (exists esd_gap_gep_scaled. esd_gap_gep_scaled + S esd_index_gep_scaled = h) -> (((exists ff_h_esd_gep_scaled_decoded. ff_h_esd_gep_scaled_decoded + S (esd_value_gep_scaled) = S ((S (esd_index_gep_scaled)) * tc)) /\ exists ff_q_esd_gep_scaled_decoded. tb = ff_q_esd_gep_scaled_decoded * S ((S (esd_index_gep_scaled)) * tc) + (esd_value_gep_scaled))) -> esd_value_gep_scaled = a * (1 + esd_index_gep_scaled)) -> (forall fdp_index_gep_division. (exists gsp_lt_gap_gep_division_index_bound. gsp_lt_gap_gep_division_index_bound + S fdp_index_gep_division = h) -> exists fdp_value_gep_division fdp_quotient_gep_division fdp_remainder_gep_division. (((exists ff_h_fdp_gep_division_source. ff_h_fdp_gep_division_source + S (fdp_value_gep_division) = S ((S (fdp_index_gep_division)) * tc)) /\ exists ff_q_fdp_gep_division_source. tb = ff_q_fdp_gep_division_source * S ((S (fdp_index_gep_division)) * tc) + (fdp_value_gep_division))) /\ ((((exists ff_h_fdp_gep_division_quotient_entry. ff_h_fdp_gep_division_quotient_entry + S (fdp_quotient_gep_division) = S ((S (fdp_index_gep_division)) * qc)) /\ exists ff_q_fdp_gep_division_quotient_entry. qb = ff_q_fdp_gep_division_quotient_entry * S ((S (fdp_index_gep_division)) * qc) + (fdp_quotient_gep_division))) /\ ((((exists ff_h_fdp_gep_division_remainder_entry. ff_h_fdp_gep_division_remainder_entry + S (fdp_remainder_gep_division) = S ((S (fdp_index_gep_division)) * rc)) /\ exists ff_q_fdp_gep_division_remainder_entry. rb = ff_q_fdp_gep_division_remainder_entry * S ((S (fdp_index_gep_division)) * rc) + (fdp_remainder_gep_division))) /\ (fdp_value_gep_division = p * fdp_quotient_gep_division + fdp_remainder_gep_division /\ (exists gsp_lt_gap_gep_division_remainder_bound. gsp_lt_gap_gep_division_remainder_bound + S fdp_remainder_gep_division = p))))) -> (forall gsp_index_gep_signed. (exists gsp_lt_gap_gep_signed_index_bound. gsp_lt_gap_gep_signed_index_bound + S gsp_index_gep_signed = h) -> (exists gsp_value_gep_signed_entry gsp_magnitude_gep_signed_entry gsp_sign_gep_signed_entry. (((exists ff_h_gsp_gep_signed_entry_source. ff_h_gsp_gep_signed_entry_source + S (gsp_value_gep_signed_entry) = S ((S (gsp_index_gep_signed)) * c)) /\ exists ff_q_gsp_gep_signed_entry_source. b = ff_q_gsp_gep_signed_entry_source * S ((S (gsp_index_gep_signed)) * c) + (gsp_value_gep_signed_entry))) /\ ((((exists ff_h_gsp_gep_signed_entry_magnitude. ff_h_gsp_gep_signed_entry_magnitude + S (gsp_magnitude_gep_signed_entry) = S ((S (gsp_index_gep_signed)) * mc)) /\ exists ff_q_gsp_gep_signed_entry_magnitude. mb = ff_q_gsp_gep_signed_entry_magnitude * S ((S (gsp_index_gep_signed)) * mc) + (gsp_magnitude_gep_signed_entry))) /\ ((((exists ff_h_gsp_gep_signed_entry_sign. ff_h_gsp_gep_signed_entry_sign + S (gsp_sign_gep_signed_entry) = S ((S (gsp_index_gep_signed)) * sc)) /\ exists ff_q_gsp_gep_signed_entry_sign. sb = ff_q_gsp_gep_signed_entry_sign * S ((S (gsp_index_gep_signed)) * sc) + (gsp_sign_gep_signed_entry))) /\ ((exists gsp_lt_gap_gep_signed_entry_positive. gsp_lt_gap_gep_signed_entry_positive + S 0 = gsp_magnitude_gep_signed_entry) /\ ((exists gsp_le_gap_gep_signed_entry_bounded. gsp_le_gap_gep_signed_entry_bounded + gsp_magnitude_gep_signed_entry = h) /\ ((gsp_sign_gep_signed_entry = 0 \/ gsp_sign_gep_signed_entry = 1) /\ (((gsp_sign_gep_signed_entry = 0 /\ (exists gsp_mod_left_gep_signed_entry_lower gsp_mod_right_gep_signed_entry_lower. (a * gsp_value_gep_signed_entry) + p * gsp_mod_left_gep_signed_entry_lower = (gsp_magnitude_gep_signed_entry) + p * gsp_mod_right_gep_signed_entry_lower)) \/ (gsp_sign_gep_signed_entry = 1 /\ (exists gsp_mod_left_gep_signed_entry_reflected gsp_mod_right_gep_signed_entry_reflected. (a * gsp_value_gep_signed_entry) + p * gsp_mod_left_gep_signed_entry_reflected = ((2 * h) * gsp_magnitude_gep_signed_entry) + p * gsp_mod_right_gep_signed_entry_reflected))))))))))) -> (forall i x q m s. (exists gsp_lt_gap_gep_index. gsp_lt_gap_gep_index + S i = h) -> (((exists ff_h_gep_source_entry. ff_h_gep_source_entry + S (x) = S ((S (i)) * c)) /\ exists ff_q_gep_source_entry. b = ff_q_gep_source_entry * S ((S (i)) * c) + (x))) -> (((exists ff_h_gep_quotient_entry. ff_h_gep_quotient_entry + S (q) = S ((S (i)) * qc)) /\ exists ff_q_gep_quotient_entry. qb = ff_q_gep_quotient_entry * S ((S (i)) * qc) + (q))) -> (((exists ff_h_gep_magnitude_entry. ff_h_gep_magnitude_entry + S (m) = S ((S (i)) * mc)) /\ exists ff_q_gep_magnitude_entry. mb = ff_q_gep_magnitude_entry * S ((S (i)) * mc) + (m))) -> (((exists ff_h_gep_sign_entry. ff_h_gep_sign_entry + S (s) = S ((S (i)) * sc)) /\ exists ff_q_gep_sign_entry. sb = ff_q_gep_sign_entry * S ((S (i)) * sc) + (s))) -> (exists sdp_u_gep_prefix_result sdp_v_gep_prefix_result. (x) + 2 * sdp_u_gep_prefix_result = (q + m + s) + 2 * sdp_v_gep_prefix_result))

Proof neighborhood

Direct theorem prerequisites

PA002F beta_at_unique PA00CO odd_signed_division_congruence_mod_two

Direct theorem dependents

PA00CR gauss_eisenstein_terminal_sums_mod_two

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

155 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 (2)
beta at uniqueodd signed division congruence mod two
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 tb
  7. L7
    intro tc
  8. L8
    intro qb
  9. L9
    intro qc
  10. L10
    intro rb
02Fix variables and assumptionsL11–20

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

  1. L11
    intro rc
  2. L12
    intro mb
  3. L13
    intro mc
  4. L14
    intro sb
  5. L15
    intro sc
  6. L16
    intro hp
  7. L17
    intro ha
  8. L18
    intro hhalf
  9. L19
    intro hscaled
  10. L20
    intro hdivision
03Fix variables and assumptionsL21–30

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

  1. L21
    intro hsigned
  2. L22
    intro i
  3. L23
    intro x
  4. L24
    intro q
  5. L25
    intro m
  6. L26
    intro s
  7. L27
    intro hi
  8. L28
    intro hx
  9. L29
    intro hq
  10. L30
    intro hm
04Fix variables and assumptionsL31–31

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

  1. L31
    intro hs
05Establish hcanonicalL32–35

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

  1. L32
    have hcanonical : BetaAt(b,c,i,1 + i)Definitions: BetaAt(b,c,i,1 + i)Original native command in the exact edition
  2. L33
    specialize hhalf i
  3. L34
    apply hhalf
  4. L35
    exact hi
06Establish hdivdataL36–39

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

  1. L36
    have hdivdata : ∃ x1. ∃ x2. ∃ x3. BetaAt(tb,tc,i,x1) ∧ (BetaAt(qb,qc,i,x2) ∧ (BetaAt(rb,rc,i,x3) ∧ DivRem(x1,p,x2,x3)))Definitions: BetaAt(tb,tc,i,x1)BetaAt(qb,qc,i,x2)BetaAt(rb,rc,i,x3)DivRem(x1,p,x2,x3)Original native command in the exact edition
  2. L37
    specialize hdivision i
  3. L38
    apply hdivision
  4. L39
    exact hi
07Separate the logical casesL40–46

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

  1. L40
    cases hdivdata
  2. L41
    cases hdivdata_witness
  3. L42
    cases hdivdata_witness_witness
  4. L43
    cases hdivdata_witness_witness_witness
  5. L44
    cases hdivdata_witness_witness_witness_right
  6. L45
    cases hdivdata_witness_witness_witness_right_right
  7. L46
    cases hdivdata_witness_witness_witness_right_right_right
08Establish hsigneddataL47–50

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

  1. L47
    have hsigneddata : ∃ x4. ∃ x5. ∃ x6. BetaAt(b,c,i,x4) ∧ (BetaAt(mb,mc,i,x5) ∧ (BetaAt(sb,sc,i,x6) ∧ (Lt(0,x5) ∧ (Le(x5,h) ∧ ((x6 = 0 ∨ x6 = 1) ∧ (x6 = 0 ∧ ModEq(p,a · x4,x5) ∨ x6 = 1 ∧ ModEq(p,a · x4,2 · h · x5)))))))Definitions: BetaAt(b,c,i,x4)BetaAt(mb,mc,i,x5)BetaAt(sb,sc,i,x6)Lt(0,x5)Le(x5,h)ModEq(p,a · x4,x5)ModEq(p,a · x4,2 · h · x5)Original native command in the exact edition
  2. L48
    specialize hsigned i
  3. L49
    apply hsigned
  4. L50
    exact hi
09Separate the logical casesL51–59

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

  1. L51
    cases hsigneddata
  2. L52
    cases hsigneddata_witness
  3. L53
    cases hsigneddata_witness_witness
  4. L54
    cases hsigneddata_witness_witness_witness
  5. L55
    cases hsigneddata_witness_witness_witness_right
  6. L56
    cases hsigneddata_witness_witness_witness_right_right
  7. L57
    cases hsigneddata_witness_witness_witness_right_right_right
  8. L58
    cases hsigneddata_witness_witness_witness_right_right_right_right
  9. L59
    cases hsigneddata_witness_witness_witness_right_right_right_right_right
10Establish hxcanonicalL60–68

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

  1. L60
    have hxcanonical : x4 = 1 + i
  2. L61
    specialize beta_at_unique b
  3. L62
    specialize beta_at_unique c
  4. L63
    specialize beta_at_unique i
  5. L64
    specialize beta_at_unique x4
  6. L65
    specialize beta_at_unique (1 + i)
  7. L66
    apply beta_at_unique
  8. L67
    exact hsigneddata_witness_witness_witness_left
  9. L68
    exact hcanonical
11Establish hnscaleL69–69

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

  1. L69
    have hnscale : x1 = a * x4
12Establish hscale_exactL70–79

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

  1. L70
    have hscale_exact : ∀ esd_index_gep_proof_scaled. ∀ esd_value_gep_proof_scaled. Lt(esd_index_gep_proof_scaled,h) → BetaAt(tb,tc,esd_index_gep_proof_scaled,esd_value_gep_proof_scaled) → esd_value_gep_proof_scaled = a · (1 + esd_index_gep_proof_scaled)Definitions: Lt(esd_index_gep_proof_scaled,h)BetaAt(tb,tc,esd_index_gep_proof_scaled,esd_value_gep_proof_scaled)Original native command in the exact edition
  2. L71
    exact hscaled
  3. L72
    trans a * (1 + i)
  4. L73
    specialize hscale_exact i
  5. L74
    specialize hscale_exact x1
  6. L75
    apply hscale_exact
  7. L76
    exact hi
  8. L77
    exact hdivdata_witness_witness_witness_left
  9. L78
    congr
  10. L79
    refl
13Calculate and transport equalitiesL80–80

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

  1. L80
    symm
14Use earlier factsL81–81

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

  1. L81
    exact hxcanonical
15Establish hsignednL82–82

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

  1. L82
    have hsignedn : x6 = 0 ∧ ModEq(p,x1,x5) ∨ x6 = 1 ∧ ModEq(p,x1,2 · h · x5)Definitions: ModEq(p,x1,x5)ModEq(p,x1,2 · h · x5)Original native command in the exact edition
16Separate the logical casesL83–86

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

  1. L83
    cases hsigneddata_witness_witness_witness_right_right_right_right_right_right
  2. L84
    left
  3. L85
    cases hsigneddata_witness_witness_witness_right_right_right_right_right_right_left
  4. L86
    split
17Use earlier factsL87–87

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

  1. L87
    exact hsigneddata_witness_witness_witness_right_right_right_right_right_right_left_left
18Calculate and transport equalitiesL88–88

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

  1. L88
    rewrite hnscale
19Use earlier factsL89–89

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

  1. L89
    exact hsigneddata_witness_witness_witness_right_right_right_right_right_right_left_right
20Separate the logical casesL90–92

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

  1. L90
    right
  2. L91
    cases hsigneddata_witness_witness_witness_right_right_right_right_right_right_right
  3. L92
    split
21Use earlier factsL93–93

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

  1. L93
    exact hsigneddata_witness_witness_witness_right_right_right_right_right_right_right_left
22Calculate and transport equalitiesL94–94

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

  1. L94
    rewrite hnscale
23Use earlier factsL95–95

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

  1. L95
    exact hsigneddata_witness_witness_witness_right_right_right_right_right_right_right_right
24Establish hlocalL96–105

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

  1. L96
    have hlocal : ModEq(2,x4,x2 + x5 + x6)Definitions: ModEq(2,x4,x2 + x5 + x6)Original native command in the exact edition
  2. L97
    specialize odd_signed_division_congruence_mod_two p
  3. L98
    specialize odd_signed_division_congruence_mod_two h
  4. L99
    specialize odd_signed_division_congruence_mod_two a
  5. L100
    specialize odd_signed_division_congruence_mod_two x4
  6. L101
    specialize odd_signed_division_congruence_mod_two x1
  7. L102
    specialize odd_signed_division_congruence_mod_two x2
  8. L103
    specialize odd_signed_division_congruence_mod_two x3
  9. L104
    specialize odd_signed_division_congruence_mod_two x5
  10. L105
    specialize odd_signed_division_congruence_mod_two x6
25Use earlier factsL106–114

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

  1. L106
    apply odd_signed_division_congruence_mod_two
  2. L107
    exact hp
  3. L108
    exact ha
  4. L109
    exact hnscale
  5. L110
    exact hdivdata_witness_witness_witness_right_right_right_left
  6. L111
    exact hdivdata_witness_witness_witness_right_right_right_right
  7. L112
    exact hsigneddata_witness_witness_witness_right_right_right_left
  8. L113
    exact hsigneddata_witness_witness_witness_right_right_right_right_left
  9. L114
    exact hsignedn
26Establish hxeqL115–123

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

  1. L115
    have hxeq : x = x4
  2. L116
    specialize beta_at_unique b
  3. L117
    specialize beta_at_unique c
  4. L118
    specialize beta_at_unique i
  5. L119
    specialize beta_at_unique x
  6. L120
    specialize beta_at_unique x4
  7. L121
    apply beta_at_unique
  8. L122
    exact hx
  9. L123
    exact hsigneddata_witness_witness_witness_left
27Establish hqeqL124–132

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

  1. L124
    have hqeq : q = x2
  2. L125
    specialize beta_at_unique qb
  3. L126
    specialize beta_at_unique qc
  4. L127
    specialize beta_at_unique i
  5. L128
    specialize beta_at_unique q
  6. L129
    specialize beta_at_unique x2
  7. L130
    apply beta_at_unique
  8. L131
    exact hq
  9. L132
    exact hdivdata_witness_witness_witness_right_left
28Establish hmeqL133–141

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

  1. L133
    have hmeq : m = x5
  2. L134
    specialize beta_at_unique mb
  3. L135
    specialize beta_at_unique mc
  4. L136
    specialize beta_at_unique i
  5. L137
    specialize beta_at_unique m
  6. L138
    specialize beta_at_unique x5
  7. L139
    apply beta_at_unique
  8. L140
    exact hm
  9. L141
    exact hsigneddata_witness_witness_witness_right_left
29Establish hseqL142–151

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

  1. L142
    have hseq : s = x6
  2. L143
    specialize beta_at_unique sb
  3. L144
    specialize beta_at_unique sc
  4. L145
    specialize beta_at_unique i
  5. L146
    specialize beta_at_unique s
  6. L147
    specialize beta_at_unique x6
  7. L148
    apply beta_at_unique
  8. L149
    exact hs
  9. L150
    exact hsigneddata_witness_witness_witness_right_right_left
  10. L151
    rewrite hxeq
30Calculate and transport equalitiesL152–154

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

  1. L152
    rewrite hqeq
  2. L153
    rewrite hmeq
  3. L154
    rewrite hseq
31Use earlier factsL155–155

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

  1. L155
    exact hlocal

Library-wide reading audit

Original defined command ledger · 155 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro a
  4. 0004intro b
  5. 0005intro c
  6. 0006intro tb
  7. 0007intro tc
  8. 0008intro qb
  9. 0009intro qc
  10. 0010intro rb
  11. 0011intro rc
  12. 0012intro mb
  13. 0013intro mc
  14. 0014intro sb
  15. 0015intro sc
  16. 0016intro hp
  17. 0017intro ha
  18. 0018intro hhalf
  19. 0019intro hscaled
  20. 0020intro hdivision
  21. 0021intro hsigned
  22. 0022intro i
  23. 0023intro x
  24. 0024intro q
  25. 0025intro m
  26. 0026intro s
  27. 0027intro hi
  28. 0028intro hx
  29. 0029intro hq
  30. 0030intro hm
  31. 0031intro hs
  32. 0032have hcanonical : BetaAt(b,c,i,1 + i)
    Exact native replay linehave hcanonical : ((exists gsp_beta_height_gep_proof_canonical. gsp_beta_height_gep_proof_canonical + S (1 + i) = S ((S (i)) * c)) /\ exists gsp_beta_quotient_gep_proof_canonical. b = gsp_beta_quotient_gep_proof_canonical * S ((S (i)) * c) + (1 + i))
  33. 0033specialize hhalf i
  34. 0034apply hhalf
  35. 0035exact hi
  36. 0036have hdivdata : ∃ x1. ∃ x2. ∃ x3. BetaAt(tb,tc,i,x1) ∧ (BetaAt(qb,qc,i,x2) ∧ (BetaAt(rb,rc,i,x3) ∧ DivRem(x1,p,x2,x3)))
    Exact native replay linehave hdivdata : exists x1 x2 x3. (((exists ff_h_gep_proof_div_source. ff_h_gep_proof_div_source + S (x1) = S ((S (i)) * tc)) /\ exists ff_q_gep_proof_div_source. tb = ff_q_gep_proof_div_source * S ((S (i)) * tc) + (x1))) /\ ((((exists ff_h_gep_proof_div_q. ff_h_gep_proof_div_q + S (x2) = S ((S (i)) * qc)) /\ exists ff_q_gep_proof_div_q. qb = ff_q_gep_proof_div_q * S ((S (i)) * qc) + (x2))) /\ ((((exists ff_h_gep_proof_div_r. ff_h_gep_proof_div_r + S (x3) = S ((S (i)) * rc)) /\ exists ff_q_gep_proof_div_r. rb = ff_q_gep_proof_div_r * S ((S (i)) * rc) + (x3))) /\ (x1 = p * x2 + x3 /\ (exists gsp_lt_gap_gep_proof_div_r_below. gsp_lt_gap_gep_proof_div_r_below + S x3 = p))))
  37. 0037specialize hdivision i
  38. 0038apply hdivision
  39. 0039exact hi
  40. 0040cases hdivdata
  41. 0041cases hdivdata_witness
  42. 0042cases hdivdata_witness_witness
  43. 0043cases hdivdata_witness_witness_witness
  44. 0044cases hdivdata_witness_witness_witness_right
  45. 0045cases hdivdata_witness_witness_witness_right_right
  46. 0046cases hdivdata_witness_witness_witness_right_right_right
  47. 0047have hsigneddata : ∃ x4. ∃ x5. ∃ x6. BetaAt(b,c,i,x4) ∧ (BetaAt(mb,mc,i,x5) ∧ (BetaAt(sb,sc,i,x6) ∧ (Lt(0,x5) ∧ (Le(x5,h) ∧ ((x6 = 0 ∨ x6 = 1) ∧ (x6 = 0 ∧ ModEq(p,a · x4,x5) ∨ x6 = 1 ∧ ModEq(p,a · x4,2 · h · x5)))))))
    Exact native replay linehave hsigneddata : exists x4 x5 x6. (((exists ff_h_gep_proof_signed_source. ff_h_gep_proof_signed_source + S (x4) = S ((S (i)) * c)) /\ exists ff_q_gep_proof_signed_source. b = ff_q_gep_proof_signed_source * S ((S (i)) * c) + (x4))) /\ ((((exists ff_h_gep_proof_signed_magnitude. ff_h_gep_proof_signed_magnitude + S (x5) = S ((S (i)) * mc)) /\ exists ff_q_gep_proof_signed_magnitude. mb = ff_q_gep_proof_signed_magnitude * S ((S (i)) * mc) + (x5))) /\ ((((exists ff_h_gep_proof_signed_sign. ff_h_gep_proof_signed_sign + S (x6) = S ((S (i)) * sc)) /\ exists ff_q_gep_proof_signed_sign. sb = ff_q_gep_proof_signed_sign * S ((S (i)) * sc) + (x6))) /\ ((exists gsp_lt_gap_gep_proof_signed_positive. gsp_lt_gap_gep_proof_signed_positive + S 0 = x5) /\ ((exists gsp_le_gap_gep_proof_signed_bounded. gsp_le_gap_gep_proof_signed_bounded + x5 = h) /\ ((x6 = 0 \/ x6 = 1) /\ (((x6 = 0 /\ (exists wpp_mod_left_gep_proof_signed_lower wpp_mod_right_gep_proof_signed_lower. (a * x4) + p * wpp_mod_left_gep_proof_signed_lower = (x5) + p * wpp_mod_right_gep_proof_signed_lower)) \/ (x6 = 1 /\ (exists wpp_mod_left_gep_proof_signed_upper wpp_mod_right_gep_proof_signed_upper. (a * x4) + p * wpp_mod_left_gep_proof_signed_upper = ((2 * h) * x5) + p * wpp_mod_right_gep_proof_signed_upper)))))))))
  48. 0048specialize hsigned i
  49. 0049apply hsigned
  50. 0050exact hi
  51. 0051cases hsigneddata
  52. 0052cases hsigneddata_witness
  53. 0053cases hsigneddata_witness_witness
  54. 0054cases hsigneddata_witness_witness_witness
  55. 0055cases hsigneddata_witness_witness_witness_right
  56. 0056cases hsigneddata_witness_witness_witness_right_right
  57. 0057cases hsigneddata_witness_witness_witness_right_right_right
  58. 0058cases hsigneddata_witness_witness_witness_right_right_right_right
  59. 0059cases hsigneddata_witness_witness_witness_right_right_right_right_right
  60. 0060have hxcanonical : x4 = 1 + i
  61. 0061specialize beta_at_unique b
  62. 0062specialize beta_at_unique c
  63. 0063specialize beta_at_unique i
  64. 0064specialize beta_at_unique x4
  65. 0065specialize beta_at_unique (1 + i)
  66. 0066apply beta_at_unique
  67. 0067exact hsigneddata_witness_witness_witness_left
  68. 0068exact hcanonical
  69. 0069have hnscale : x1 = a * x4
  70. 0070have hscale_exact : ∀ esd_index_gep_proof_scaled. ∀ esd_value_gep_proof_scaled. Lt(esd_index_gep_proof_scaled,h) → BetaAt(tb,tc,esd_index_gep_proof_scaled,esd_value_gep_proof_scaled) → esd_value_gep_proof_scaled = a · (1 + esd_index_gep_proof_scaled)
    Exact native replay linehave hscale_exact : forall esd_index_gep_proof_scaled esd_value_gep_proof_scaled. (exists esd_gap_gep_proof_scaled. esd_gap_gep_proof_scaled + S esd_index_gep_proof_scaled = h) -> (((exists ff_h_esd_gep_proof_scaled_decoded. ff_h_esd_gep_proof_scaled_decoded + S (esd_value_gep_proof_scaled) = S ((S (esd_index_gep_proof_scaled)) * tc)) /\ exists ff_q_esd_gep_proof_scaled_decoded. tb = ff_q_esd_gep_proof_scaled_decoded * S ((S (esd_index_gep_proof_scaled)) * tc) + (esd_value_gep_proof_scaled))) -> esd_value_gep_proof_scaled = a * (1 + esd_index_gep_proof_scaled)
  71. 0071exact hscaled
  72. 0072trans a * (1 + i)
  73. 0073specialize hscale_exact i
  74. 0074specialize hscale_exact x1
  75. 0075apply hscale_exact
  76. 0076exact hi
  77. 0077exact hdivdata_witness_witness_witness_left
  78. 0078congr
  79. 0079refl
  80. 0080symm
  81. 0081exact hxcanonical
  82. 0082have hsignedn : x6 = 0 ∧ ModEq(p,x1,x5) ∨ x6 = 1 ∧ ModEq(p,x1,2 · h · x5)
    Exact native replay linehave hsignedn : ((x6 = 0 /\ (exists wpp_mod_left_gep_proof_n_mod_m wpp_mod_right_gep_proof_n_mod_m. (x1) + p * wpp_mod_left_gep_proof_n_mod_m = (x5) + p * wpp_mod_right_gep_proof_n_mod_m)) \/ (x6 = 1 /\ (exists wpp_mod_left_gep_proof_n_mod_upper wpp_mod_right_gep_proof_n_mod_upper. (x1) + p * wpp_mod_left_gep_proof_n_mod_upper = ((2 * h) * x5) + p * wpp_mod_right_gep_proof_n_mod_upper)))
  83. 0083cases hsigneddata_witness_witness_witness_right_right_right_right_right_right
  84. 0084left
  85. 0085cases hsigneddata_witness_witness_witness_right_right_right_right_right_right_left
  86. 0086split
  87. 0087exact hsigneddata_witness_witness_witness_right_right_right_right_right_right_left_left
  88. 0088rewrite hnscale
  89. 0089exact hsigneddata_witness_witness_witness_right_right_right_right_right_right_left_right
  90. 0090right
  91. 0091cases hsigneddata_witness_witness_witness_right_right_right_right_right_right_right
  92. 0092split
  93. 0093exact hsigneddata_witness_witness_witness_right_right_right_right_right_right_right_left
  94. 0094rewrite hnscale
  95. 0095exact hsigneddata_witness_witness_witness_right_right_right_right_right_right_right_right
  96. 0096have hlocal : ModEq(2,x4,x2 + x5 + x6)
    Exact native replay linehave hlocal : exists sdp_u_gep_proof_final sdp_v_gep_proof_final. (x4) + 2 * sdp_u_gep_proof_final = (x2 + x5 + x6) + 2 * sdp_v_gep_proof_final
  97. 0097specialize odd_signed_division_congruence_mod_two p
  98. 0098specialize odd_signed_division_congruence_mod_two h
  99. 0099specialize odd_signed_division_congruence_mod_two a
  100. 0100specialize odd_signed_division_congruence_mod_two x4
  101. 0101specialize odd_signed_division_congruence_mod_two x1
  102. 0102specialize odd_signed_division_congruence_mod_two x2
  103. 0103specialize odd_signed_division_congruence_mod_two x3
  104. 0104specialize odd_signed_division_congruence_mod_two x5
  105. 0105specialize odd_signed_division_congruence_mod_two x6
  106. 0106apply odd_signed_division_congruence_mod_two
  107. 0107exact hp
  108. 0108exact ha
  109. 0109exact hnscale
  110. 0110exact hdivdata_witness_witness_witness_right_right_right_left
  111. 0111exact hdivdata_witness_witness_witness_right_right_right_right
  112. 0112exact hsigneddata_witness_witness_witness_right_right_right_left
  113. 0113exact hsigneddata_witness_witness_witness_right_right_right_right_left
  114. 0114exact hsignedn
  115. 0115have hxeq : x = x4
  116. 0116specialize beta_at_unique b
  117. 0117specialize beta_at_unique c
  118. 0118specialize beta_at_unique i
  119. 0119specialize beta_at_unique x
  120. 0120specialize beta_at_unique x4
  121. 0121apply beta_at_unique
  122. 0122exact hx
  123. 0123exact hsigneddata_witness_witness_witness_left
  124. 0124have hqeq : q = x2
  125. 0125specialize beta_at_unique qb
  126. 0126specialize beta_at_unique qc
  127. 0127specialize beta_at_unique i
  128. 0128specialize beta_at_unique q
  129. 0129specialize beta_at_unique x2
  130. 0130apply beta_at_unique
  131. 0131exact hq
  132. 0132exact hdivdata_witness_witness_witness_right_left
  133. 0133have hmeq : m = x5
  134. 0134specialize beta_at_unique mb
  135. 0135specialize beta_at_unique mc
  136. 0136specialize beta_at_unique i
  137. 0137specialize beta_at_unique m
  138. 0138specialize beta_at_unique x5
  139. 0139apply beta_at_unique
  140. 0140exact hm
  141. 0141exact hsigneddata_witness_witness_witness_right_left
  142. 0142have hseq : s = x6
  143. 0143specialize beta_at_unique sb
  144. 0144specialize beta_at_unique sc
  145. 0145specialize beta_at_unique i
  146. 0146specialize beta_at_unique s
  147. 0147specialize beta_at_unique x6
  148. 0148apply beta_at_unique
  149. 0149exact hs
  150. 0150exact hsigneddata_witness_witness_witness_right_right_left
  151. 0151rewrite hxeq
  152. 0152rewrite hqeq
  153. 0153rewrite hmeq
  154. 0154rewrite hseq
  155. 0155exact hlocal